3/31/06
There is a rule for adding a Existential Quantifier. This permits the step illustrated by the following proof fragments.
5 Fa 6 (∃x)Fx 5 EG
5 Fb 6 (∃x)Fx 5 EG
5 Fb 6 (∃z)Fz 5 EG
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 respectively, then substitute a term for free occurrences of the variable of quantification-- you should be able to get line 5, and indeed you can.
Sad to say, like Universal Instantiation and Generalization, there is a rather sophisticated restriction on this rule-- we will come to this in Tutorial 23.
If a derivation contains a line of the form
n. <formula>[<term>/<variable>]> <any justification>
then a line of the form
(∃<variable>)<formula> 'n EG'
may be added to the derivation, provided that <variable> is new to <formula>.
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