You should now Launch Deriver and do the 3 exercises of Predicate Exercise 11 (Predex11).
It is probably easier to learn EI using Tactics. After you start each derivation,switch Tactics on, select the existentially quantified formula, and click EI.
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)
Repeat the derivations of Exercise 1 without using Tactics.
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