. 64
( 107 .)


you then prove a sentence not containing these constants, you may end the
subproof and infer the result using ∃ Elim.

Section 13.2
350 / Formal Proofs and Quantifiers


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


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

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
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.


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


. 64
( 107 .)