Roger, Thank for once again trying to clarify Existential Elimination. Sorry for being to thick-headed, but I still don't get it. What is confusing is the 3 parameters. e.g. In this partial proof, there is only one premise, but you mention 2?
> > Message: 2 > Date: Tue, 31 Mar 2020 21:35:59 +0100 > From: Roger Bishop Jones <r...@rbjones.com> > To: proofpower@lemma-one.com > Subject: Re: [ProofPower] ?_elim > > 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 > I think I need a simpler example perhaps. How about this one? Prove ∀x(W(x)⇒R(x)),∃xW(x) ⊢ ∃xR(x) Starting out like this: "Existential Elimination"; val L1 = asm_rule ⌜∃x⦁W(x)⌝; val L2 = asm_rule ⌜W(b):BOOL⌝; val L3 = ∃_elim ⌜x⌝ L1 L2; =GFT val it = "Existential Elimination": string :) val L1 = ∃ x⦁ W x ⊢ ∃ x⦁ W x: THM :) val L2 = W b ⊢ W b: THM :) val L3 = ∃ x⦁ W x, W b ⊢ W b: THM It does seem to be close, but it introduced a new premise W b It I don't do that, what is the third parameter to ∃_elim? It seems I need 2 THMs but only have 1! Thank you in advance for all your wonderful contributions to this software and explanations of how to use it! -Dave
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
