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 ∃_elim
Need 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
