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

it.

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

contradiction.

We now begin the process of turning our informal proof into a formal

proof.

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

proof.

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

Exercises

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)

‚ ‚