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