. 65
( 107 .)


2. A good strategy is to ¬nd an informal proof and then try to formalize

3. Working backwards can be very useful in proving universal claims,
especially those of the form ∀x (P(x) ’ Q(x)).

4. Working backwards is not useful in proving an existential claim ∃x S(x)
unless you can think of a particular instance S(c) of the claim that
follows from the premises.

5. If you get stuck, consider using proof by contradiction.

A worked example
We are going to work through a moderately di¬cult proof, step by step, using
what we have learned in this section. Consider the the following argument:

¬∀x P(x)
∃x ¬P(x)

This is one of four such inferences associated with the DeMorgan rules relating
quanti¬ers and negation. The fact that this inference can be validated in F
is one we will need in our proof of the Completeness Theorem for the system
F in the ¬nal chapter. (The other three DeMorgan rules will be given in the
review exercises at the end of this chapter. Understanding this example will
be a big help in doing those exercises.)
Before embarking on the proof, we mention that this inference is one of the
hallmarks of ¬rst-order logic. Notice that it allows us to assert the existence
of something having a property from a negative fact: that not everything has
the opposite property.
In the late nineteenth and early twentieth century, the validity of this sort
of inference was hotly debated in mathematical circles. While it seems obvious
to us now, it is because we have come to understand existence claims in a
somewhat di¬erent way than some (the so-called “intuitionists”) understood intuitionists

Section 13.3
356 / Formal Proofs and Quantifiers

them. While the ¬rst-order understanding of ∃x Q(x) is as asserting that some
Q exists, the intuitionist took it as asserting something far stronger: that the
asserter had actually found a Q and proven it to be a Q. Under this stronger
reading, the DeMorgan principle under discussion would not be valid. This
point will be relevant to our proof.
Let us now turn to the proof. Following our strategy, we begin with an
informal proof, and then formalize it.
Proof: Since we are trying to prove an existential sentence, our ¬rst
thought would be to use existential introduction, say by proving
¬P(c) for some c. But if we think a bit about what our premise
means, we see there is no hope of proving of any particular thing
that it satis¬es ¬P(x). From the fact that not everything satis¬es
P(x), we aren™t going to prove of some speci¬c c that ¬P(c). So this
is surely a dead end. (It is also why the intuitionist would not accept
the argument as valid, given his or her understanding of ∃.)
This leaves only one possible route to our desired conclusion: proof by
contradiction. Thus we will negation our desired conclusion and try
to obtain a contradiction. Thus, we assume ¬∃x ¬P(x). How can we
hope to obtain a contradiction? Since our only premise is ¬∀x P(x),
the most promising line of attack would be to try for a proof of
∀x P(x) using universal generalization. Thus, let c be an arbitrary
individual in our domain of discourse. Our goal is to prove P(c).
How can we do this? Another proof by contradiction, for if P(c)
were not the case, then we would have ¬P(c), and hence ∃x ¬P(x).
But this contradicts our assumption. Hence P(c) is the case. Since
c was arbitrary, we get ∀x P(x). But this contradicts our premise.
Hence, we get our desired conclusion using the method of proof by
We now begin the process of turning our informal proof into a formal

You try it
1. Open Quanti¬er Strategy 1. This contains the skeleton of our proof:
1. ¬∀x P(x)
2. ∃x ¬P(x)

Chapter 13
Strategy and tactics / 357

2. The ¬rst step in our informal proof was to decide to try to give a proof by
contradiction. Formalize this idea by ¬lling in the following:
1. ¬∀x P(x)

2. ¬∃x ¬P(x)
4. ⊥ ⊥ Intro: ?, ?
5. ∃x ¬P(x) ¬ Intro: 2“4

This step will check out because of the generous nature of Fitch™s ¬ Intro
rule, which lets us either strip o¬ as well as add a negation.

3. We next decided to try to contradict ¬∀x P(x) by proving ∀x P(x) using
universal generalization. Formalize this as follows:
1. ¬∀x P(x)

2. ¬∃x ¬P(x)

3. c

5. P(c) ?
6. ∀x P(x) ∀ Intro: 3“5
7. ⊥ ⊥ Intro: 6, 1
8. ∃x ¬P(x) ¬ Intro: 2“7
4. Recall how we proved P(c). We said that if P(c) were not the case, then
we would have ¬P(c), and hence ∃x ¬P(x). But this contradicted the as-
sumption at step 2. Formalize this reasoning by ¬lling in the rest of the

Section 13.3
358 / Formal Proofs and Quantifiers

1. ¬∀x P(x)

2. ¬∃x ¬P(x)

3. c

4. ¬P(c)
5. ∃x ¬P(x) ∃ Intro: 3
6. ⊥ ⊥ Intro: 5, 2
7. ¬¬P(c) ¬ Intro: 4“6
8. P(c) ¬ Elim: 7
9. ∀x P(x) ∀ Intro: 3“8
10. ⊥ ⊥ Intro: 9, 1
11. ∃x ¬P(x) ¬ Intro: 2“10
5. This completes our formal proof of ∃x ¬P(x) from the premise ¬∀x P(x).
Verify your proof and save it as Proof Quanti¬er Strategy 1.
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Congratulations


13.19 If you skipped the You try it section, go back and do it now. Submit the ¬le Proof Quanti¬er
‚ Strategy 1.

Recall that in Exercises 1“3 on page 327, you were asked to give logical analyses of purported proofs of
some arguments involving nonsense predicates. In the following exercises, we return to these arguments.
If the argument is valid, submit a formal proof. If it is invalid, turn in an informal counterexample. If
you submit a formal proof, be sure to use the Exercise ¬le supplied with Fitch. In order to keep your
hand in at using the propositional rules, we ask you not to use Taut Con in these proofs.

13.20 ∀x [(Brillig(x) ∨ Tove(x)) ’ (Mimsy(x) § Gyre(x))]
‚| ∀y [(Slithy(y) ∨ Mimsy(y)) ’ Tove(y)]
∃x Slithy(x)
∃x [Slithy(x) § Mimsy(x)]
(See Exercise 12.1 on p. 327.)

Chapter 13
Strategy and tactics / 359

13.21 13.22
∀x [Brillig(x) ’ (Mimsy(x) § Slithy(x))] ∀x [(Brillig(x) § Tove(x)) ’ Mimsy(x)]
‚| ‚|
∀y [(Slithy(y) ∨ Mimsy(y)) ’ Tove(y)] ∀y [(Tove(y) ∨ Mimsy(y)) ’ Slithy(y)]
∀x [Tove(x) ’ (Outgrabe(x, b) § Brillig(x))] ∃x Brillig(x) § ∃x Tove(x)
∀z [Brillig(z) ” Mimsy(z)] ∃z Slithy(z)
(See Exercise 12.2 on p. 328.) (See Exercise 12.3, p. 328)

Some of the following arguments are valid, some are not. For each, either use Fitch to give a formal
proof or use Tarski™s World to construct a counterexample. In giving proofs, feel free to use Taut Con
if it helps.

13.23 13.24
∀y [Cube(y) ∨ Dodec(y)] ∃x (Cube(x) § Small(x))
‚ ‚
∀x [Cube(x) ’ Large(x)]
∃x Cube(x) § ∃x Small(x)
∃x ¬Large(x)
∃x Dodec(x)

13.25 13.26
∃x Cube(x) § ∃x Small(x) ∀x (Cube(x) ’ Small(x))
‚ ‚ ∀x (Adjoins(x, b) ’ Small(x))
∃x (Cube(x) § Small(x))
∀x ((Cube(x) ∨ Small(x))
’ Adjoins(x, b))

13.27 ∀x (Cube(x) ’ Small(x))
‚ ∀x (¬Adjoins(x, b) ’ ¬Small(x))
∀x ((Cube(x) ∨ Small(x)) ’ Adjoins(x, b))

For each of the following, use Fitch to give a formal proof of the argument. These look simple but some
of them are a bit tricky. Don™t forget to ¬rst ¬gure out an informal proof. Use Taut Con whenever it
is convenient but do not use FO Con.
13.28 13.29
∀x ∀y Likes(x, y) ∀x (Small(x) ’ Cube(x))
‚ ‚ ∃x ¬Cube(x) ’ ∃x Small(x)
∀x ∃y Likes(x, y)
∃x Cube(x)

13.30 13.31
Likes(carl, max) ∀x ∀y [Likes(x, y) ’ Likes(y, x)]
‚ ‚
∀x [∃y (Likes(y, x) ∨ Likes(x, y)) ∃x ∀y Likes(x, y)
’ Likes(x, x)]
∀x ∃y Likes(x, y)
∃x Likes(x, carl)

Section 13.3
360 / Formal Proofs and Quantifiers

The following valid arguments come in pairs. The validity of the ¬rst of the pair makes crucial use of the
meanings of the blocks language predicates, whereas the second adds one or more premises, making the
result a ¬rst-order valid argument. For the latter, give a proof that does not make use of Ana Con. For
the former, give a proof that uses Ana Con but only where the premises and conclusions of the citation
are literals (including ⊥). You may use Taut Con but do not use FO Con in any of the proofs.

13.32 13.33
¬∃x (Tet(x) § Small(x)) ¬∃x (Tet(x) § Small(x))
‚ ‚ ∀y (Small(y) ∨ Medium(y) ∨ Large(y))
∀x [Tet(x) ’ (Large(x) ∨ Medium(x))]
∀x [Tet(x) ’ (Large(x) ∨ Medium(x))]

13.34 13.35
∀x (Dodec(x) ’ SameCol(x, a)) ∀x (Dodec(x) ’ SameCol(x, a))
‚ ‚
SameCol(a, c) SameCol(a, c)
∀x ∀y ∀z ((SameCol(x, y) § SameCol(y, z))
∀x (Dodec(x) ’ SameCol(x, c))
’ SameCol(x, z))
∀x (Dodec(x) ’ SameCol(x, c))

13.36 13.37
∀x (Dodec(x) ’ LeftOf(x, a)) ∀x (Dodec(x) ’ LeftOf(x, a))
‚ ‚
∀x (Tet(x) ’ RightOf(x, a)) ∀x (Tet(x) ’ RightOf(x, a))
∀x ∀y (LeftOf(x, y) ’ ¬SameCol(x, y))
∀x (SameCol(x, a) ’ Cube(x))
∀x ∀y (RightOf(x, y) ’ ¬SameCol(x, y))
∀x (Cube(x) ∨ Dodec(x) ∨ Tet(x))
∀x (SameCol(x, a) ’ Cube(x))

13.38 13.39
∀x (Cube(x) ’ ∀y (Dodec(y) ∀x (Cube(x) ’ ∀y (Dodec(y)
‚ ‚


. 65
( 107 .)