[Logiweb] Re: Quantifier elimination leads to variable clash

[Klaus Ebbe Grue]

Hi logiweb at diku.dk

Just for the record: Frederiks guess below is correct. More on that in the 
lecture today.

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