Existential Instantiation permits you to remove an existential quantifier from a formula which has an existential quantifier as its main connective.
The circumstance that Existential Instantiation gets invoked looks like this.
(∃x)<scope> ? ? ? <<
For example,
(∃x)Fx ? ? ? <<
It is easy to get a rough sense of what this should permit. (∃x)Fx says that 'something is F ' so what it should permit is an inference to, say, Fa ie 'a is F', where 'a' is the name of that thing which is F. Care has to be taken here because the constant 'a' may already be in the proof and, in fact, we may be able to prove Ga-- in which case we may be tempted to think that (∃x)Fx and Ga can give us (Fa and Ga) which it should not because there is no assurance that the thing which is F is the same thing as the thing which is G. What is needed here is that the 'a' or, to give it another description, the instantiating constant or term be new to the proof.
The resulting rule permits any of the following
n (∃x)Fx ? Fa n EI
n (∃x)Fx ? Fb n EI
provided 'a' and 'b' etc are new to the proof.
Proofs
Derive the following
a) (∃x)(Fa) ∴ Fa
b) (∃x) (Fx.Gx) ∴ (∃x)(Fx )
c) (∃x) (Fx.Gx) ∴ (∃y)(Gy)
d) (∃x)(Fx)∴ (∃y)(Fy)
e) (∃x)(Fx.Gx) ∴ (∃y)(Fy).(∃z)(Gz)
Proofs
Each of following derivations will use Existential Instantiation at some stage.
Derive
a) ∴ (∃x)Fx≡(∃y)Fy
b) (x)Fx,(∃x)~Fx∴G
c) ∴ (∃x) (Fx∨Gx) ≡ (∃y)Fy∨(∃z)Gz
d) (∃x)(Fx∨Gx),(x)(Fx⊃Hx),(x)(Gx⊃Hx)∴(∃x)Hx
e) ~(∃x)(Fx.~Gx),~(∃x)(Gx.~Hx)∴(x)(Fx⊃Hx)
f) ~(∃x)Gx,(x)(Fx⊃Gx)∴(x)(Fx⊃Hx)
g) (∃x)Fx∨(∃x)Gx,(x)((Fx∨Gx)⊃Hx)∴(∃x)Hx