subproof and infer the result using ∃ Elim.

Section 13.2

350 / Formal Proofs and Quantifiers

Remember

The formal rule of ∃ Elim corresponds to the informal method of exis-

tential instantiation.

Exercises

13.10 If you skipped the You try it section, go back and do it now. Submit the ¬le Proof Existential 1.

‚

For each of the following arguments, decide whether or not it is valid. If it is, use Fitch to give a formal

proof. If it isn™t, use Tarski™s World to give a counterexample. Remember that in this chapter you are

free to use Taut Con to justify proof steps involving only propositional connectives.

13.11 13.12

∀x (Cube(x) ∨ Tet(x)) ∀x (Cube(x) ∨ Tet(x))

‚ ‚

∃x ¬Cube(x) ∃x ¬Cube(x)

∃x ¬Tet(x) ∃x Tet(x)

13.13 13.14

∀y [Cube(y) ∨ Dodec(y)] ∀x (Cube(x) ” Small(x))

‚ ‚

∀x [Cube(x) ’ Large(x)] ∃x ¬Cube(x)

∃x ¬Large(x)

∃x ¬Small(x)

∃x Dodec(x)

13.15 13.16

∃x (Cube(x) ’ Small(x)) ∃x ∃y Adjoins(x, y)

‚ ‚

∀x Cube(x) ∀x ∀y (Adjoins(x, y)

’ ¬SameSize(x, y))

∃x Small(x)

∃x ∃y ¬SameSize(y, x)

In our discussion of the informal methods, we observed that the method that introduces new constants

can interact to give defective proofs, if not used with care. The formal system F automatically prevents

these misapplications of the quanti¬er rules. The next two exercises are designed to show you how the

formal rules prevent these invalid steps by formalizing one of the fallacious informal proofs we gave

earlier.

Chapter 13

Existential quantifier rules / 351

13.17 Here is a formalization of the pseudo-proof given on page 331:

‚

1. ∀x ∃y SameCol(x, y)

2. c

3. ∃y SameCol(c, y) ∀ Elim: 1

4. d SameCol(c, d)

5. SameCol(c, d) Reit: 4

6. SameCol(c, d) ∃ Elim: 3, 4“5

7. ∀x SameCol(x, d) ∀ Intro: 2“6

8. ∃y ∀x SameCol(x, y) ∃ Intro: 7

1. Write this “proof ” in a ¬le using Fitch and check it out. You will discover that step

6 is incorrect; it violates the restriction on existential elimination that requires the

constant d to appear only in the subproof where it is introduced. Notice that the other

steps all check out, so if we could make that move, then the rest of the proof would be

¬ne.

2. Construct a counterexample to the argument to show that no proof is possible.

Submit both ¬les.

13.18 Let™s contrast the faulty proof from the preceding exercise with a genuine proof that ∀x ∃y R(x, y)

‚ follows from ∃y ∀x R(x, y). Use Fitch to create the following proof.

1. ∃y ∀x SameCol(x, y)

2. d ∀x SameCol(x, d)

3. c

4. SameCol(c, d) ∀ Elim: 2

5. ∃y SameCol(c, y) ∃ Intro: 4

6. ∀x ∃y SameCol(x, y) ∀ Intro: 3“5

7. ∀x ∃y SameCol(x, y) ∃ Elim: 1, 2“6

Notice that in this proof, unlike the one in the previous exercise, both constant symbols c

and d are properly sequestered within the subproofs where they are introduced. Therefore the

quanti¬er rules have been applied properly. Submit your proof.

Section 13.2

352 / Formal Proofs and Quantifiers

Section 13.3

Strategy and tactics

We have seen some rather simple examples of proofs using the new rules. In

more interesting examples, however, the job of ¬nding a proof can get pretty

challenging. So a few words on how to approach these proofs will be helpful.

We have given you a general maxim and two strategies for ¬nding sen-

tential proofs. The maxim”to consider what the various sentences mean”is

consider meaning

even more important with the quanti¬ers. Only if you remember what they

mean and how the formal methods mirror common-sense informal methods

will you be able to do any but the most boring of exercises.

Our ¬rst strategy was to try to come up with an informal proof of the

informal proof as guide

goal sentence from the premises, and use it to try to ¬gure out how your

formal proof will proceed. This strategy, too, is even more important in proofs

involving quanti¬ers, but it is a bit harder to apply. The key skill in applying

the strategy is the ability to identify the formal rules implicit in your informal

reasoning. This takes a bit of practice. Let™s work through an example, to see

some of the things you should be looking out for.

Suppose we want to prove that the following argument is valid:

∃x (Tet(x) § Small(x))

∀x (Small(x) ’ LeftOf(x, b))

∃x LeftOf(x, b)

Obviously, the conclusion follows from the given sentences. But ask yourself

how you would prove it, say, to your stubborn roommate, the one who likes

to play devil™s advocate. You might argue as follows:

Look, Bozo, we™re told that there is a small tetrahedron. So we know

that it is small, right? But we™re also told that anything that™s small

is left of b. So if it™s small, it™s got to be left of b, too. So something™s

left of b, namely the small tetrahedron.

Now we don™t recommend calling your roommate “Bozo,” so ignore that bit.

The important thing to notice here is the implicit use of three of our quanti¬er

rules: ∃ Elim, ∀ Elim, and ∃ Intro. Do you see them?

What indicates the use of ∃ Elim is the “it” appearing in the second

sentence. What we are doing there is introducing a temporary name (in this

case, the pronoun “it”) and using it to refer to a small tetrahedron. That

corresponds to starting the subproof needed for an application of ∃ Elim.

Chapter 13

Strategy and tactics / 353

So after the second sentence of our informal proof, we can already see the

following steps in our reasoning (using “c” for “it”):

1. ∃x (Tet(x) § Small(x))

2. ∀x (Small(x) ’ LeftOf(x, b))

3. c Tet(c) § Small(c)

4. Small(c) § Elim: 3

.

.

.

5. ∃x LeftOf(x, b) ??

6. ∃x LeftOf(x, b) ∃ Elim: 3-5

In general, the key to recognizing ∃ Elim is to watch out for any reference to

an object whose existence is guaranteed by an existential claim. The reference

might use a pronoun (it, he, she), as in our example, or it might use a de¬nite

noun phrase (the small tetrahedron), or ¬nally it might use an actual name

(let n be a small tetrahedron). Any of these are signs that the reasoning is

proceeding via existential elimination.

The third and fourth sentences of our informal argument are where the

implicit use of ∀ Elim shows up. There we apply the claim about all small

things to the small tetrahedron we are calling “it.” This gives us a couple

more steps in our formal proof:

1. ∃x (Tet(x) § Small(x))

2. ∀x (Small(x) ’ LeftOf(x, b))

3. c Tet(c) § Small(c)

4. Small(c) § Elim: 3

5. Small(c) ’ LeftOf(c, b) ∀ Elim: 2

6. LeftOf(c, b) ’ Elim: 4, 5

.

.

.

8. ∃x LeftOf(x, b) ?

9. ∃x LeftOf(x, b) ∃ Elim: 3-8

The distinctive mark of universal elimination is just the application of a gen-

eral claim to a speci¬c individual. For example, we might also have said at

Section 13.3

354 / Formal Proofs and Quantifiers

this point: “So the small tetrahedron [there™s the speci¬c individual] must be

left of b.”

The implicit use of ∃ Intro appears in the last sentence of the informal

reasoning, where we conclude that something is left of b, based on the fact that

“it,” the small tetrahedron, is left of b. In our formal proof, this application

of ∃ Intro will be done within the subproof, giving us a sentence that we can

export out of the subproof since it doesn™t contain the temporary name c.

1. ∃x (Tet(x) § Small(x))

2. ∀x (Small(x) ’ LeftOf(x, b))

3. c Tet(c) § Small(c)

4. Small(c) § Elim: 3

5. Small(c) ’ LeftOf(c, b) ∀ Elim: 2

6. LeftOf(c, b) ’ Elim: 4, 5

7. ∃x LeftOf(x, b) ∃ Intro: 6

8. ∃x LeftOf(x, b) ∃ Elim: 1, 3-7

One thing that™s a bit tricky is that in informal reasoning we often leave out

simple steps like ∃ Intro, since they are so obvious. Thus in our example, we

might have left out the last sentence completely. After all, once we conclude

that the small tetrahedron is left of b, it hardly seems necessary to point out

that something is left of b. So you™ve got to watch out for these omitted steps.

This completes our formal proof. To a trained eye, the proof matches the

informal reasoning exactly. But you shouldn™t feel discouraged if you would

have missed it on your own. It takes a lot of practice to recognize the steps

implicit in our own reasoning, but it is practice that in the end makes us more

careful and able reasoners.

The second strategy that we stressed is that of working backwards: starting

working backward

from the goal sentence and inserting steps or subproofs that would enable us

to infer that goal. It turns out that of the four new quanti¬er rules, only ∀

Intro really lends itself to this technique.

Suppose your goal sentence is of the form ∀x (P(x) ’ Q(x)). After survey-

ing your given sentences to see whether there is any immediate way to infer

this conclusion, it is almost always a good idea to start a subproof in which

you introduce an arbitrary name, say c, and assume P(c). Then add a step to

the subproof and enter the sentence Q(c), leaving the rule unspeci¬ed. Next,

end the subproof and infer∀x (P(x) ’ Q(x)) by ∀ Intro, citing the subproof

in support. When you check this partial proof, an X will appear next to the

Chapter 13

Strategy and tactics / 355

sentence Q(c), indicating that your new goal is to prove this sentence.

Remember

1. Always be clear about the meaning of the sentences you are using.