6/19/07 10Software
Reading
Bergmann[2004] The Logic Book Section 10.1.
The Tutorial
There is a rule for adding a Existential Quantifier, Existential Introduction (also commonly known as 'Existential Generalization'). This permits the step illustrated by the following proof fragments.
5 Fa 6 (∃x)Fx 5 ∃I
5 Fb 6 (∃x)Fx 5 ∃I
5 (Fb&Gb) 6 (∃z)(Fz&Gb) 5 ∃I
To understand what this rule permits, it helps to think about it as though you were going backwards from line 6 to line 5. Take the scope of line 6, which is Fx, Fx, and (Fz&Gb) respectively, then substitute a constant for free occurrences of the variable of quantification-- you should be able to get line 5, and indeed you can.
The Rule of Existential Introduction ∃I
If a derivation contains a line of the form
n. <formula>[<constant>/<variable>] <any justification>
then a line of the form
(∃<variable>)<formula> 'n ∃I'
may be added to the derivation.
Notice that, in a sense, you are generalizing on occurrences of the constant in the first formula. Now, you do not have to generalize on all of them; you can generalize on 0, 1, or many, depending on what is there and what you want to do.
Exercise to accompany Predicate Tutorial 10
Exercise 1 (of 1)
Proofs
Derive the following
a) Fb∴(∃x)Fx
b) Fa∴(∃y)Fy
c) Fa∴(∃x)Fa
d) Fa,Ga∴(∃x)(Fx&Gx)
e) Fa,Ga∴(∃x)(Fx&Ga)
f) Fa,Ga∴(∃x)(Fa&Gx)
g) Fa,Ga∴(∃x)(Fx)&Ga