David,
Something odd about your message which confuses my mail tool and doesn't
quote it properly, so this is hand cranked (your text in italics)
/
//What is confusing is the 3 parameters. e.g. In this partial proof,
there is only one premise, but you mention 2?
/I'm afraid I'm confused by your question.
When I talked of two premises I presume I was talking of the two
theorems which are required by ∃_elim, i.e. L1 and L2 in your simpler
example.
//
/val L1 = asm_rule ⌜∃x⦁W(x)⌝;/
/val L2 = asm_rule ⌜W(b):BOOL⌝;/
/val L3 = ∃_elim ⌜x⌝ L1 L2;/
Good idea to look at the reference manual entry for ∃_elim, which, in
the version I am looking at, is on page 333.
The first premise must have an existential conclusion.
The second premise must have an assumption which is obtained from that
conclusion by removing the existential quantifier, but the variable over
which is quantifies must not be present anywhere else in the second premise.
You can change the name (as you have done) but you must use a name which
has no other free occurrences in that premise.
In L2 W(b) appears with b free both in the assumptions and in the
conclusion, so the rule will fail to eliminate W(b) from the assumptions.
Apart from the one assumption matching the existential premise which is
supposed to be remove (but wasn't in this case), all the assumptions in
the two premises appear in the conclusion.
So that's why /∃x⦁W(x)⌝ /appears in the assumptions of your conclusion.
A better explanation of what /∃_elim/ is doing has now occurred to me.
The turnstile in HOL is purely truth functional,
so you may think of A1, A2..., An ⊢ C as being similar to A1 ∧ A2 ... An ⇒ C
and we know that P is provable iff ∀x⦁P x//is provable./
/So A1, P x..., An ⊢ C is provable iff ∀x⦁A1 ∧ P x ... An ⇒ C is provable
and if x appears free nowhere else we can push in the universal to:
A1 ∧ (∃x⦁P x) ... An ⇒ C
i.e. a conjecture with an assumption with a unique free variable is provable
iff the conjecture with that assumption existentially quantified is
provable.
This is reflected in the effect of stripping an existential into the
assumptions
in a goal oriented proof, which results in the existential being dropped.
I say all this just to explain the naming of /∃_elim//.
/The existential eliminated by the rule is not an explicit existential
but rather what we might call an implicit existential in the assumptions
of the second premise, which is eliminated using a theorem (the first
premise) which has that existential as its conclusion.
If that existential is proven using certain assumptions, then of course
those assumptions must appear on the resulting theorem.
If the existential in the first premise does not match an assumption
in the second in which the existentially quatified variable is replaced by
a unique free variable, then the rule will not fail, but it will not
eliminate
any assumption, and you will still get the extra assumptions added.
This is what happened in your simpler example.
good luck,
Roger
//
/
/
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
