[Logiweb] Re: Quantifier elimination leads to variable clash

[Anders B0ggild-Povlsen]

If I remenber correctly, Klaus suggested that you prove the lemma with any 
free meta variables and use that lemma to prove the same thing using the 
meta variables you wanted to use in the first place.

In your case you could begin by proving (D=>E) => (D=>F=>E) and use that 
lemma to prove (A => B) => (A => C => B). That should avoid variable clash.

Anders Bøggild

On Mon, 20 Jun 2005, Ole Hyldahl Hansen wrote:

>
>> 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
>
-------------- next part --------------
_______________________________________________
Logiweb mailing list
Logiweb at diku.dk
http://miming.diku.dk/mailman/listinfo/logiweb
(Web access from inside DIKUs LAN only)