[Logiweb] Re: Quantifier elimination leads to variable clash

[Ole Hyldahl Hansen]

> Hi logiweb at diku.dk
>
> Just for the record: Frederiks guess below is correct. More on that in the 
> lecture today.

Sorry, I must have forgotten what was said about this topic at the lecture 
:-(.

I would like to prove this lemma:
(A=>B) => (A=>C=>B)

In the proof I need this instance of axiom A1: B=>C=>B. However, that 
causes the "Quantifier elimination leads to variable clash". I can easily 
prove this lemma instead: (D=>E) => (D=>F=>E) using another instance of 
A1: E=>F=>E.

But I cannot keep using fresh meta variables for all lemmas (right?). Is 
there a good solution or just a recommended "best practice" for avoiding 
this problem?

Using the at @-operator does not seem to help any.

What should I do?

Thanks in advance
Ole Hyldahl Hansen



>
> Klaus
>
> On Thu, 9 Jun 2005, Frederik Eriksen wrote:
>> Kasper H0st Frederiksen wrote:
>> ... "Quantifier elimination leads to variable clash ...."
>> 
>> My guess is that the proof will go through if you just use another
>> variable name than "meta b" - for instance, "meta a".
>> 
>> Here's an explanation why this might work: When you use axioms and rules,
>> you have to avoid conflicts between your own variable names, and the
>> variable names contained in the quantifiers of the axioms/rules you are
>> using. For example, let's say you try to prove the lemma:
>> 
>> BBB: B -> B -> B,
>> 
>> using the axiom:
>> 
>> A1': For all A : for all B :  A -> B -> A.
>> 
>> (The "->" stands for "peano imply". I've put the "B" from BBB in
>> boldface, to make the contrast with the "B" from A1' clearer.) The first
>> thing Logiweb does is to replace the "A" in A1' with the "B" from BBB.
>> This gives us:
>> 
>> (§):  for all B :  B -> B -> B.
>> 
>> But now there is a clash between the B from the quantifier of (§), and
>> the new "B" from BBB. In Mendelson's parlance, B is not free for A in
>> A1'. This gives the error message: "Quantifier elimination leads to
>> variable clash". However, you can easily prove:
>> 
>> AAA: A -> A -> A
>> 
>> using axiom A1'.
>
>



===================================
 	unzip;strip;touch;finger;mount;fsck;more;yes;unmount;sleep