David,
The existential rule most closely analogous to universal instantiation
is existential introduction.
The ∃_elim rule is more complex, and the name perhaps misleading.
The conclusion is always exactly the conclusion of the second premise.
The existential "eliminated" is the conclusion of the first premise.
But its probably clearer to think of the first premise being used to
eliminate an assumption in the second premise which is a witness to the
existential in the first premise.
In your proof, the effect realised is to introduce an existential in the
assumptions (in both cases).
Roger
On 31/03/2020 17:10, David Topham wrote:
I was restudying this proof suggested by Rob a few years ago and still
have a nagging question I am trying to resolve:
Here is the complete proof
with the output you should see in the comments.
val L1 = asm_rule ⌜p(x,y):BOOL⌝;
(* val L1 = p (x, y) ⊢ p (x, y): THM *)
val L2 = ⌜∃x:'a⦁p(x,y)⌝;
(* val L2 = ⌜∃ x⦁ p (x, y)⌝: TERM *)
val L3 = ∃_intro L2 L1;
(* val L3 = p (x, y) ⊢ ∃ x⦁ p (x, y): THM *)
val L4 = ⌜∃y:'b⦁∃x:'a⦁p(x,y)⌝;
(* val L4 = ⌜∃ y x⦁ p (x, y)⌝: TERM *)
val L5 = ∃_intro L4 L3;
(* val L5 = p (x, y) ⊢ ∃ y x⦁ p (x, y): THM *)
val L6 = asm_rule ⌜∃y:'b⦁p(x,y)⌝;
(* val L6 = ∃ y⦁ p (x, y) ⊢ ∃ y⦁ p (x, y): THM *)
val L7 = ∃_elim ⌜y:'b⌝ L6 L5;
(* val L7 = ∃ y⦁ p (x, y) ⊢ ∃ y x⦁ p (x, y): THM *)
val L8 = asm_rule ⌜∃x:'a⦁ ∃y:'b⦁p(x,y)⌝;
(* val L8 = ∃ x y⦁ p (x, y) ⊢ ∃ x y⦁ p (x, y): THM *)
val L9 = ∃_elim ⌜x:'a⌝ L8 L7;
(* val L9 = ∃ x y⦁ p (x, y) ⊢ ∃ y x⦁ p (x, y): THM *)
val L10 = ⇒_intro ⌜∃x:'a⦁ ∃y:'b⦁p(x,y)⌝ L9;
(* val L10 = ⊢ (∃ x y⦁ p (x, y)) ⇒ (∃ y x⦁ p (x, y)): THM *)
I know when we do Universal elimination the quantifier is no longer
there, but here for Existential elimination the quantifier remains.
Is there a reason for that?
e.g.
Why is
val L7 = ∃_elim ⌜y:'b⌝ L6 L5;
(* val L7 = ∃ y⦁ p (x, y) ⊢ ∃ y x⦁ p (x, y): THM *)
not
val L7 = ∃_elim ⌜y:'b⌝ L6 L5;
(* val L7 = ∃ y⦁ p (x, y) ⊢ p (x, y): THM *)
Aren't we selecting y to be witness or example of a y that satisfies p?
Like
(∃y)Py Py ∃_elimNeed to make assumption based on the existentially quantified
proposition
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
