Empirical Support for Our Response

One of us (S. Bringsjord) hypothesized that the training provided, because it is confined to merely brisk coverage of certain purely syntactic rules of inference, fails to give students/subjects the formal tools required for solving (P1)-(P4), and other problems from the same general class. What might be missing, S.B. specifically hypothesized, is (among other things)

H1

teaching of disproofs;

H2

teaching of diagrammatic techniques;

H3

and teaching of rigorous and general-purpose procedures for formalizing natural language logic problems in first-order logic so that they can then be solved by proof.

In order to test these hypotheses, S.B. has repeatedly taught students how to use certain theorem-proving technologies in order to produce proofs that constitute solutions to problems at the level of our quartet, and well beyond. These technologies allow for both the construction of disproofs (so-called ``proofs of non-consequence") and for diagrammatic reasoning; and the use of these systems to generate proofs absolutely requires that students be able to formalize natural language logic problems in first-order logic so that such problems can be mechanically solved by proof.

In three separate pre-test/post-test designs, using the system HYPERPROOF [Barwise and Etchemendy, 1994] (and to some degree the system OTTER; both are treated by S. Bringsjord in class as theorem-provers, though the former is designed mostly for pedagogical purposes while the latter is used by professional mathematicians), this is precisely what was found. For example, in the first experiment, while 20% of students at the start of a HYPERPROOF-based first course in mathematical logic solved the selection task, P1, over 80% solved a formal analogue at the end of the course. Similarly dramatic improvement was obtained for P2-P4. More importantly, at the conclusion of the course students were able to routinely solve logic problems much more difficult than P1-P4. This level of performance was replicated twice in the two other experiments. Of course, Piaget predicted that deductive operations would be something a young person would master (with suitable interchange with the environment). We see no reason to think that, say, sixth graders couldn't routinely learn to do what my college students routinely learn to do; and we're planning experiments at this grade level to see if we're correct.

Let us conclude by briefly diagnosing the two members of the quartet P1-P4 in the context of my hypotheses and the pedagogy with which they are associated. (More details can be found by looking at the courses on S. Bringsjord's web site.)

Consider first the selection task in connection with H3. Students were told that they had to cast the selection task in a form that would allow the automated theorem prover OTTER to solve it. Here is a sample input file:

% Wason's Selection Task
% This is an input file for the 
% proof that if card
% 4 (which shows a 7), when flipped, 
% reveals a vowel,
% then a contradiction results.

set(auto).

formula_list(usable).
% The rule:
all x (Vowel(x) -> Even(x)).
% What we observe facing us 
% before flipping:
Vowel(c1).
Consonant(c2).
Even(c3).
Odd(c4).
% The fact that even and odd 
% numbers are distinct:
all x (Even(x) <-> -Odd(x)).
% The possibility that card 
% 4 bears a vowel:
Vowel(c4).
end_of_list.

And here is the proof from a sample output file ($F indicates that a contradiction has been found):

---------------- PROOF ----------------
1 [] -Vowel(x)|Even(x).
2 [] -Even(x)| -Odd(x).
6 [] Odd(c4).
8 [] Vowel(c4).
10 [hyper,8,1] Even(c4).
11 [hyper,10,2,6] $F.
------------ end of proof -------------

Students get so good at this process that even logic problems much harder than P1 can be formalized and sent to OTTER to be solved by proof. For example, they are soon able to solve a problem like the Dreadsbury Mansion Mystery:

Someone Who lives in Dreadsbury Mansion killed Aunt Agatha. Agatha, the butler, and Charles live in Dreadsbury Mansion, and are the only people who live therein. A killer always hates his victim, and is never richer than his victim. Charles hates no one that Aunt Agatha hates. Agatha hates everyone except the butler. The butler hates everyone not richer than Aunt Agatha. The butler hates everyone Agatha hates. No one hates everyone. Agatha is not the butler.

Now, given the above clues, there is a bit of a disagreement between three (incompetent?) Norwegian detectives: Inspector Bjorn is sure that Charles didn't do it. Is he right? Inspector Reidar is sure that it was a suicide. Is he right? Inspector Olaf is sure that the butler, despite conventional wisdom, is innocent. Is he right?

Let's consider now the teaching of disproofs, and let's anchor the discussion to P4: We noted above that in P4 (3) doesn't follow from (1) and (2). This sequence -- (3) from (1) and (2) -- is one of 256 syllogisms studied by Aristotle (out of this space, 15 are valid). It's form is

In order to conform to the geometric predicates built into the HYPERPROOF system [Barwise and Etchemendy, 1994], let's recast this inference in first-order logic as follows.

Now, it is possible to prove in Hyperproof that this inference is invalid. The finished proof is shown in Figure 1. You will notice that the first two lines of symbolic text match the premises; this is the ``given" information. You will then see what is called a ``sub-proof" under these lines; the sub-proof is composed of three lines. In the first line of the sub-proof (an assumption) a visual situation is constructed in which two dodecs (frenchmen) are happy (wine-drinkers), and some happy things (wine-drinkers) are large (gourmets). In the second line of the sub-proof, a check is done to make sure that this visual situation is consistent with the given information (a indicates that we have consistency). Finally, in the last line, we simply observe that the conclusion in question is false in the visual situation. This constitutes a disproof of the syllogism.

 
Figure:  The ``Frenchmen" Syllogism Disproved in Hyperproof

In conclusion and in short, Piaget is right: humans can rather easily reach the level of formal deductive operations if they are educated in logic as they are in areas like reading and arithmetic.