. 22
( 107 .)


conclusion, A ∨ C, is also true. The conclusion is true in other rows as well, but
we don™t care about that. This inference, from A ∨ ¬B and B ∨ C to A ∨ C, is
logically valid, and is an instance of an important pattern known in computer
science as resolution.
We should look at an example where the truth table method reveals that
the conclusion is not a tautological consequence of the premises. Actually, the
last truth table will serve this purpose. For this table also shows that the
sentence A ∨ ¬B is not a tautological consequence of the two premises B ∨ C
and A ∨ C. Can you ¬nd the row that shows this? (Hint: It™s got to be the
¬rst, second, third, ¬fth, or seventh, since these are the rows in which B ∨ C
and A ∨ C are both true.)

Chapter 4
Logical and tautological consequence / 113


Let P1 , . . . , Pn and Q be sentences of fol built up from atomic sentences
by means of truth functional connectives alone. Construct a joint truth
table for all of these sentences.

1. Q is a tautological consequence of P1 , . . . , Pn if and only if every row
that assigns T to each of P1, . . . , Pn also assigns T to Q.

2. If Q is a tautological consequence of P1 , . . . , Pn , then Q is also a logical
consequence of P1, . . . , Pn .

3. Some logical consequences are not tautological consequences.


For each of the arguments below, use the truth table method to determine whether the conclusion is a
tautological consequence of the premises. Your truth table for Exercise 4.24 will be fairly large. It™s good
for the soul to build a large truth table every once in a while. Be thankful you have Boole to help you.
(But make sure you build your own reference columns!)

4.20 4.21
(Tet(a) § Small(a)) ∨ Small(b) Taller(claire, max) ∨ Taller(max, claire)
‚ ‚ Taller(claire, max)
Small(a) ∨ Small(b)
¬Taller(max, claire)

4.22 Large(a)
‚ Cube(a) ∨ Dodec(a)
(Cube(a) § Large(a)) ∨ (Dodec(a) § Large(a))

4.23 4.24
A ∨ ¬B ¬A ∨ B ∨ C
‚ ‚
B∨C ¬C ∨ D
C∨D ¬(B § ¬E)
A ∨ ¬D D ∨ ¬A ∨ E

4.25 Give an example of two di¬erent sentences A and B in the blocks language such that A § B is
 a logical consequence of A ∨ B. [Hint: Note that A § A is a logical consequence of A ∨ A, but
here we insist that A and B be distinct sentences.]

Section 4.3
114 / The Logic of Boolean Connectives

Section 4.4
Tautological consequence in Fitch
We hope you solved Exercise 4.24, because the solution gives you a sense
of both the power and the drawbacks of the truth table method. We were
tempted to ask you to construct a table requiring 64 rows, but thought better
of it. Constructing large truth tables may build character, but like most things
that build character, it™s a drag.
Checking to see if Q is a tautological consequence of P1 , . . . , Pn is a me-
chanical procedure. If the sentences are long it may require a lot of tedious
work, but it doesn™t take any originality. This is just the sort of thing that
computers are good at. Because of this, we have built a mechanism into Fitch,
called Taut Con, that is similar to Ana Con but checks to see whether a
Taut Con mechanism
sentence is a tautological consequence of the sentences cited in support. Like
Ana Con, Taut Con is not really an inference rule (we will introduce infer-
ence rules for the Boolean connectives in Chapter 6), but is useful for quickly
testing whether one sentence follows tautologically from others.

You try it
1. Launch Fitch and open the ¬le Taut Con 1. In this ¬le you will ¬nd an
argument that has the same form as the argument in Exercise 4.23. (Ignore
the two goal sentences. We™ll get to them later.) Move the focus slider to
the last step of the proof. From the Rule? menu, go down to the Con
submenu and choose Taut Con.

2. Now cite the three premises as support for this sentence and check the
step. The step will not check out since this sentence is not a tautological
consequence of the premises, as you discovered if you did Exercise 4.23,
which has the same form as this inference.

3. Edit the step that did not check out to read:

Home(max) ∨ Hungry(carl)

This sentence is a tautological consequence of two of the premises. Figure
out which two and cite just them. If you cited the right two, the step
should check out. Try it.

4. Add another step to the proof and enter the sentence:

Hungry(carl) ∨ (Home(max) § Hungry(pris))

Chapter 4
Tautological consequence in Fitch / 115

Use Taut Con to see if this sentence follows tautologically from the three
premises. Choose Verify Proof from the Proof menu. You will ¬nd that
although the step checks out, the goal does not. This is because we have
put a special constraint on your use of Taut Con in this exercise.

5. Choose See Goal Constraints from the Goal menu. You will ¬nd that
in this proof, you are allowed to use Taut Con, but can only cite two
or fewer support sentences when you use it. Close the goal window to get
back to the proof.

6. The sentence you entered also follows from the sentence immediately above
it plus just one of the three premises. Uncite the three premises and see
if you can get the step to check out citing just two sentences in support.
Once you succeed, verify the proof and save it as Proof Taut Con 1
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Congratulations
You are probably curious about the relationship between Taut Con and
Ana Con”and for that matter, what the other mysterious item on the Con
menu, FO Con, might do. These are in fact three increasingly strong methods Taut Con, FO Con,
and Ana Con
that Fitch uses to test for logical consequence. Taut Con is the weakest. It
checks to see whether the current step follows from the cited sentences in virtue
of the meanings of the truth-functional connectives. It ignores the meanings of
any predicates that appear in the sentence and, when we introduce quanti¬ers
into the language, it will ignore those as well.
FO Con, which stands for “¬rst-order consequence,” pays attention to the
truth-functional connectives, the quanti¬ers, and the identity predicate when
it checks for consequence. FO Con would, for example, identify a = c as a
consequence of a = b § b = c. It is stronger than Taut Con in the sense that
any consequence that Taut Con recognizes as valid will also be recognized
by FO Con. But it may take longer since it has to apply a more complex
procedure, thanks to identity and the quanti¬ers. After we get to quanti¬ers,
we™ll talk more about the procedure it is applying.
The strongest rule of the three is Ana Con, which tries to recognize con-
sequences due to truth-functional connectives, quanti¬ers, identity, and most
of the blocks language predicates. (Ana Con ignores Between and Adjoins,
simply for practical reasons.) Any inference that checks out using either Taut
Con or FO Con should, in principle, check out using Ana Con as well. In
practice, though, the procedure that Ana Con uses may bog down or run
out of memory in cases where the ¬rst two have no trouble.
As we said before, you should only use a procedure from the Con menu
when the exercise makes clear that the procedure is allowed in the solution.

Section 4.4
116 / The Logic of Boolean Connectives

Moreover if an exercise asks you to use Taut Con, don™t use FO Con or Ana
Con instead, even if these more powerful rules seem to work just as well. If
you are in doubt about which rules you are allowed to use, choose See Goal
Constraints from the Goal menu.

You try it
1. Open the ¬le Taut Con 2. You will ¬nd a proof containing ten steps whose
rules have not been speci¬ed.

2. Focus on each step in turn. You will ¬nd that the supporting steps have
already been cited. Convince yourself that the step follows from the cited
sentences. Is it a tautological consequence of the sentences cited? If so,
change the rule to Taut Con and see if you were right. If not, change it
to Ana Con and see if it checks out. (If Taut Con will work, make sure
you use it rather than the stronger Ana Con.)

3. When all of your steps check out using Taut Con or Ana Con, go back
and ¬nd the one step whose rule can be changed from Ana Con to the
weaker FO Con.

4. When each step checks out using the weakest Con rule possible, save your
proof as Proof Taut Con 2.
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Congratulations


4.26 If you skipped the You try it sections, go back and do them now. Submit the ¬les Proof Taut
‚ Con 1 and Proof Taut Con 2.
For each of the following arguments, decide whether the conclusion is a tautological consequence of the
premises. If it is, submit a proof that establishes the conclusion using one or more applications of Taut
Con. Do not cite more than two sentences at a time for any of your applications of Taut Con. If
the conclusion is not a consequence of the premises, submit a counterexample world showing that the
argument is not valid.

4.27 4.28
Cube(a) ∨ Cube(b) Large(a) ∨ Large(b)
‚ ‚
Dodec(c) ∨ Dodec(d) Large(a) ∨ Large(c)
¬Cube(a) ∨ ¬Dodec(c)
Large(a) § (Large(b) ∨ Large(c))
Cube(b) ∨ Dodec(d)

Chapter 4
Pushing negation around / 117

4.29 4.30
Small(a) ∨ Small(b) Tet(a) ∨ ¬(Tet(b) § Tet(c))
‚ ‚
Small(b) ∨ Small(c) ¬(¬Tet(b) ∨ ¬Tet(d))
Small(c) ∨ Small(d) (Tet(e) § Tet(c)) ∨ (Tet(c) § Tet(d))
Small(d) ∨ Small(e)
Small(a) ∨ Small(e)

Section 4.5
Pushing negation around
When two sentences are logically equivalent, each is a logical consequence of
the other. As a result, in giving an informal proof, you can always go from
an established sentence to one that is logically equivalent to it. This fact
makes observations like the DeMorgan laws and double negation quite useful
in giving informal proofs.
What makes these equivalences even more useful is the fact that logically
equivalent sentences can be substituted for one another in the context of a substitution of logical
larger sentence and the resulting sentences will also be logically equivalent.
An example will help illustrate what we mean. Suppose we start with the

¬(Cube(a) § ¬¬Small(a))

By the principle of double negation, we know that Small(a) is logically equiv-
alent to ¬¬Small(a). Since these have exactly the same truth conditions, we
can substitute Small(a) for ¬¬Small(a) in the context of the above sentence,
and the result,

¬(Cube(a) § Small(a))

will be logically equivalent to the original, a fact that you can check by con-
structing a joint truth table for the two sentences.
We can state this important fact in the following way. Let™s write S(P)
for an fol sentence that contains the (possibly complex) sentence P as a
component part, and S(Q) for the result of substituting Q for P in S(P). Then
if P and Q are logically equivalent:


it follows that S(P) and S(Q) are also logically equivalent:


. 22
( 107 .)