<<

. 63
( 107 .)



>>


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

<<

. 63
( 107 .)



>>