You try it

................................................................

1. Open the ¬le Universal 1. This ¬le contains the argument proven above.

We™ll show you how to construct this proof in Fitch.

2. Start a new subproof immediately after the premises. Before typing any-

thing in, notice that there is a blue, downward pointing triangle to the left

of the blinking cursor. It looks just like the focus slider, but sort of stand-

ing on its head. Use your mouse to click down on this triangle. A menu

will pop up, allowing you to choose the constant(s) you want “boxed” in

this subproof. Choose d from the menu. (If you choose the wrong one, say

c, then choose it again to “unbox” it.)

3. After you have d in the constant box, enter the sentence P(d) as your

assumption. Then add a step and continue the subproof.

Chapter 13

Universal quantifier rules / 345

4. You should now be able to complete the proof on your own. When you™re

done, save it as Proof Universal 1.

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Congratulations

Default and generous uses of the ∀ rules

Both of the universal quanti¬er rules have default uses. If you cite a universal default uses of ∀ rules

sentence and apply ∀ Elim without entering a sentence, Fitch will replace the

universally quanti¬ed variable with its best guess of the name you intended. It

will either choose the alphabetically ¬rst name that does not already appear

in the sentence, or the ¬rst name that appears as a boxed constant in the

current subproof. For example, in steps 4 and 6 of the above proof, the default

mechanism would choose d, and so generate the correct instances.

If you know you want a di¬erent name substituted for the universally

quanti¬ed variable, you can indicate this by typing a colon (:), followed by indicating substitutions

the variable, followed by the greater-than sign (>), followed by the name

you want. In other words, if instead of a sentence you enter “: x > c”, Fitch

will instantiate ∀x P(x) as P(c), rather than picking its own default instance.

(Think of “: x > c” as saying “substitute c for x.”)

If you apply ∀ Intro to a subproof that starts with a boxed constant on its

own, without entering a sentence, Fitch will take the last sentence in the cited

subproof and universally quantify the name introduced at the beginning of the

subproof. If the cited subproof starts with a boxed constant and a sentence,

then Fitch will write the corresponding universal conditional, using the ¬rst

sentence and the last sentence of the proof to create the conditional.

You try it

................................................................

1. Open the ¬le Universal 2. Look at the goal to see what sentence we are

trying to prove. Then focus on each step in succession and check the step.

Before moving to the next step, make sure you understand why the step

checks out and, more important, why we are doing what we are doing at

that step. At the empty steps, try to predict which sentence Fitch will

provide as a default before you check the step.

2. When you are done, make sure you understand the completed proof. Save

the ¬le as Proof Universal 2.

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Congratulations

Section 13.1

346 / Formal Proofs and Quantifiers

Fitch has generous uses of both ∀ rules. ∀ Elim will allow you to remove

several universal quanti¬ers from the front a sentence simultaneously. For

example, if you have proven ∀x ∀y SameCol(x, y) you could infer SameCol(f, c)

in one step in Fitch. If you want to use the default mechanism to generate this

step, you can enter the substitutions “: x > f : y > c” before checking the step.

In a like manner, you can often prove a sentence starting with more than

one universal quanti¬er by means of a single application of ∀ Intro. You do

this by starting a subproof with the appropriate number of boxed constants.

If you then prove a sentence containing these constants you may end the

subproof and infer the result of universally quantifying each of these constants

using ∀ Intro. The default mechanism allows you to specify the variables to

be used in the generated sentence by indicating the desired substitutions, for

example “: a > z : b > w” will generate ∀z ∀w R(w, z) when applied to R(b, a).

Notice the order used to specify substitutions: for ∀ Elim it will always be

“: variable > name,” while for ∀ Intro it must be “: name > variable.”

Remember

The formal rule of ∀ Intro corresponds to the informal method of general

conditional proof, including the special case of universal generalization.

Exercises

13.1 If you skipped the You try it sections, go back and do them now. Submit the ¬les Proof

‚ Universal 1 and Proof Universal 2.

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. In this chapter you are free to use Taut

Con to justify proof steps involving only propositional connectives.

13.2 13.3

∀x (Cube(x) ” Small(x)) ∀x Cube(x)

‚ ‚

∀x Cube(x) ∀x Small(x)

∀x Small(x) ∀x (Cube(x) § Small(x))

13.4 13.5

¬∀x Cube(x) ∀x ∀y ((Cube(x) § Dodec(y))

‚ ‚ ’ Larger(y, x))

¬∀x (Cube(x) § Small(x))

∀x ∀y (Larger(x, y) ” LeftOf(x, y))

∀x ∀y ((Cube(x) § Dodec(y))

’ LeftOf(y, x))

Chapter 13

Existential quantifier rules / 347

13.6 13.7

∀x ((Cube(x) § Large(x)) ∀x ∀y ((Cube(x) § Dodec(y))

‚ ‚

∨ (Tet(x) § Small(x))) ’ FrontOf(x, y)))

∀x (Tet(x) ’ BackOf(x, c))

∀x (Cube(x) ’ ∀y (Dodec(y)

∀x ¬(Small(x) § Large(x))

’ FrontOf(x, y))

∀x (Small(x) ’ BackOf(x, c))

(See Exercise 12.9. Notice that we have

included a logical truth as an additional

premise here.)

13.8 13.9

∀x (Cube(x) ’ ∀y (Dodec(y) ∀x ∀y ((Cube(x) § Dodec(y))

‚ ‚

’ FrontOf(x, y)) ’ Larger(x, y))

∀x ∀y ((Dodec(x) § Tet(y))

∀x ∀y ((Cube(x) § Dodec(y))

’ Larger(x, y))

’ FrontOf(x, y))

∀x ∀y ((Cube(x) § Tet(y))

’ Larger(x, y))

Section 13.2

Existential quanti¬er rules

Recall that in our discussion of informal proofs, existential introduction was a

simple proof step, whereas the elimination of ∃ was a subtle method of proof.

Thus, in presenting our formal system, we begin with the introduction rule.

Existential Introduction (∃ Intro):

S(c)

.

.

.

∃x S(x)

Here too x stands for any variable, c stands for any individual constant, and

S(c) stands for the result of replacing free occurrences of x in S(x) with c.

Note that there may be other occurrences of c in S(x) as well.

When we turn to the rule of existential elimination, we employ the same,

“boxed constant” device as with universal introduction. If we have proven

∃x S(x), then we introduce a new constant symbol, say c, along with the as-

sumption that the object denoted by c satis¬es the formula S(x). If, from this

Section 13.2

348 / Formal Proofs and Quantifiers

assumption, we can derive some sentence Q not containing the constant c,

then we can conclude that Q follows from the original premises.

Existential Elimination (∃ Elim):

∃x S(x)

.

.

.

c S(c)

Where c does not occur out-

.

.

. side the subproof where it is

introduced.

Q

Q

Again we think of the notation at the beginning of the subproof as the formal

counterpart of the English “Let c be an arbitrary individual such that S(c).”

The rule of existential elimination is quite analogous to the rule of disjunc-

tion elimination, both formally and intuitively. With disjunction elimination,

comparison with

∨ Elim we have a disjunction and break into cases, one for each disjunct, and estab-

lish the same result in each case. With existential elimination, we can think

of having one case for each object in the domain of discourse. We are required

to show that, whichever object it is that satis¬es the condition S(x), the same

result Q can be obtained. If we can do this, we may conclude Q.

To illustrate the two existential rules, we will give a formal counterpart to

the proof given on page 323.

1. ∀x [Cube(x) ’ Large(x)]

2. ∀x [Large(x) ’ LeftOf(x, b)]

3. ∃x Cube(x)

4. e Cube(e)

5. Cube(e) ’ Large(e) ∀ Elim: 1

6. Large(e) ’ Elim: 5, 4

7. Large(e) ’ LeftOf(e, c) ∀ Elim: 2

8. LeftOf(e, c) ’ Elim: 7, 6

9. Large(e) § LeftOf(e, c) § Intro: 6, 8

10. ∃x (Large(x) § LeftOf(x, b)) ∃ Intro: 9

11. ∃x (Large(x) § LeftOf(x, b)) ∃ Elim: 3, 4-10

Chapter 13

Existential quantifier rules / 349

Default and generous uses of the ∃ rules

Defaults for the existential quanti¬er rules work similarly to those for the

universal quanti¬er. If you cite a sentence and apply ∃ Intro without typing default uses of ∃ rules

a sentence, Fitch will supply a sentence that existentially quanti¬es the al-

phabetically ¬rst name appearing in the cited sentence. When replacing the

name with a variable, Fitch will choose the ¬rst variable in the list of variables

that does not already appear in the cited sentence. If this isn™t the name or

variable you want used, you can specify the substitution yourself; for example

“: max > z” will replace max with z and add ∃z to the front of the result.

In a default application of ∃ Elim, Fitch will supply the last sentence in

the cited subproof, providing that sentence does not contain the temporary

name introduced at the beginning of the subproof.

You try it

................................................................

1. Open the ¬le Existential 1. Look at the goal to see the sentence we are

trying to prove. Then focus on each step in succession and check the step.

Before moving to the next step, make sure you understand why the step

checks out and, more important, why we are doing what we are doing at

that step.

2. At any empty steps, you should try to predict which sentence Fitch will

provide as a default before you check the step. Notice in particular step

eight, the one that contains “: a > y”. Can you guess what sentence would

have been supplied by Fitch had we not speci¬ed this substitution? You

could try it if you like.

3. When you are done, make sure you understand the completed proof. Save

the ¬le as Proof Existential 1.

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Congratulations

As with ∀, Fitch has generous uses of both ∃ rules. ∃ Intro will allow

you to add several existential quanti¬ers to the front a sentence. For example,

if you have proved SameCol(b, a) you could infer ∃y ∃z SameCol(y, z) in one

step in Fitch. In a like manner, you can use a sentence beginning with more

than one existential quanti¬er in a single application of ∃ Elim. You do this

by starting a subproof with the appropriate number of boxed constants. If