Tutorial 21 Existential Instantiation.

The Tutorial

Existential Instantiation permits you to remove an existential quantifier from a formula which has an existential quantifier as its main connective. It is one of those rules which involves the adoption and dropping of an extra assumption (like ∼I,⊃I,∨E, and ≡I).

The circumstance that Existential Instantiation gets invoked looks like this.

	(∃x)<scope>			?
	?			? <<
	<target>			?

That is, a formula you have has an existential quantifier as its main connective-- and you are trying to obtain some formula which we will call <target>.

For example,

	(∃x)(Fx)			?
	?			? <<
	(∃y)(Fy)			?

invites the use of EI. In this case (∃x)(Fx) is the existential formula, (Fx) is its scope, and (∃y)(Fy) is the target.

To use EI you follow a three stage process. First you assume the <scope>. The illustrated fragment will then become

	(∃x)<scope>			?
			<scope>	Ass
	?			? <<
	<target>			?

Second you continue deriving in this new context until you manage to derive <target> thus

	(∃x)<scope>			?
			<scope>	Ass
			<proof fragment in here >	?
			<target>	?
	?			? <<
	<target>			?

Finally you select <target> at the end of the sub-proof, select the existential formula, and click EI to complete the existential instantiation.

n	(∃x)<scope>			?
			<scope>	Ass
			<proof fragment in here >	?
k			<target>	?
	<target>			n,k EI

In the example, the derivation would look like

1	(∃x)Fx			Ass
2			Fx	Ass
3			(∃y)Fy	2 EG
4	(∃y)Fy			1,3 EI

There are restrictions on EI. The variable of quantification must not be free either

• a) in the <target> ,
• or b) in the assumptions of the final <target> line,
• or c) in the assumptions of the existential formula that EI is used on.

More about these later.

Exercise to accompany Predicate Tutorial 11.

Exercise 1 (of 3)

Proofs

Your browser is not displaying the Deriver applet. Try downloading Deriver itself by clicking on the link elsewhere on the page.

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)

Exercise 2 (of 3)

Proofs

Your browser is not displaying the Deriver applet. Try downloading Deriver itself by clicking on the link elsewhere on the page.

Repeat the derivations of Exercise 1 without using Tactics.

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)

Exercise 3 (of 3)

Proofs

Your browser is not displaying the Deriver applet. Try downloading Deriver itself by clicking on the link elsewhere on the page.

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

Easy Deriver Documentation ©1991-2008 Martin Frické, SoftOption™ Ltd (NZ). Easy Deriver is formed out of Deriver(Generic) Program Units. Deriver(Generic) Program Units ©1987-2008 Martin Frické, SoftOption™ Ltd (NZ). Licenced to SoftOption™ Ltd (NZ).

Should you find any bugs in Easy Deriver, please tell us about them.  (Try to reproduce them, then note their exact symptoms. Send the information to support(at)SoftOption.Us)

NO WARRANTY OR REPRESENTATION IS MADE, EITHER EXPRESSED OR IMPLIED, WITH RESPECT TO THIS SOFTWARE AND DOCUMENTATION, THEIR QUALITY, THEIR PERFORMANCE, THEIR MERCHANTABILITY, OR THEIR FITNESS FOR A PARTICULAR PURPOSE, AS A RESULT, THIS SOFTWARE IS SOLD OR OFFERED 'AS IS' AND YOU THE PURCHASER OR USER ARE ASSUMING THE ENTIRE RISK AS TO THEIR QUALITY AND TO THE SOFTWARE'S PERFORMANCE.