[Logiweb] Re: Quantifier elimination leads to variable clash

[Kasper H0st Frederiksen]

Than you for you help.

> My guess is that the proof will go through if you just use another
> variable name than "meta b" - for instance, "meta a".

Your guess truns out to be partially correct. If I replace all "meta b" in 
the proof with "meta a" I get the same error, _but_ if i replace all "meta 
b" in BOTH proof and the lemma statement with "meta k" the proof checks as 
correct.

There still seems to be a deeper problem though. If the proof uses only 
"meta k" and the lemma statement uses only "meta j" then I get a 
Lemma/Proof mismatch.

The folowing proof works:
---------------
"[ intro lemma one point eight
    index "L1.8"
    pyk   "lemma one point eight"
    tex   "L1.8"
    end intro ]"

"[ math
   in theory system prime s
    lemma
        lemma one point eight
    says
        all meta k indeed parenthesis meta k peano imply meta k end 
parenthesis
    end lemma
    end math ]"

"[ math
      system prime s
    proof of
      lemma one point eight
    reads
      arbitrary meta k end line
      line ell a because axiom prime a two indeed
        parenthesis meta k peano imply parenthesis parenthesis meta k peano 
imply meta k end parenthesis peano imply meta k end parenthesis end 
parenthesis
          peano imply
        parenthesis parenthesis meta k peano imply parenthesis meta k peano 
imply meta k end parenthesis end parenthesis peano imply parenthesis meta 
k peano imply meta k end parenthesis end parenthesis
      end line
      line ell b because axiom prime a one indeed
        meta k peano imply parenthesis parenthesis meta k peano imply meta 
k end parenthesis peano imply meta k end parenthesis
      end line
      line ell c because rule prime mp modus ponens ell a modus ponens ell 
b indeed
        parenthesis meta k peano imply parenthesis meta k peano imply meta 
k end parenthesis end parenthesis
          peano imply
        parenthesis meta k peano imply meta k end parenthesis
      end line
      line ell d because axiom prime a one indeed
        meta k peano imply parenthesis meta k peano imply meta k end 
parenthesis
      end line
      because rule prime mp modus ponens ell c modus ponens ell d indeed
        meta k peano imply meta k
      qed
    end math ]"
-------------------

But this proof gives a Lemma/Proof mismatch:
-------------------
"[ intro lemma one point eight
    index "L1.8"
    pyk   "lemma one point eight"
    tex   "L1.8"
    end intro ]"

"[ math
   in theory system prime s
    lemma
        lemma one point eight
    says
        all meta j indeed parenthesis meta j peano imply meta j end 
parenthesis
    end lemma
    end math ]"

"[ math
      system prime s
    proof of
      lemma one point eight
    reads
      arbitrary meta k end line
      line ell a because axiom prime a two indeed
        parenthesis meta k peano imply parenthesis parenthesis meta k peano 
imply meta k end parenthesis peano imply meta k end parenthesis end 
parenthesis
          peano imply
        parenthesis parenthesis meta k peano imply parenthesis meta k peano 
imply meta k end parenthesis end parenthesis peano imply parenthesis meta 
k peano imply meta k end parenthesis end parenthesis
      end line
      line ell b because axiom prime a one indeed
        meta k peano imply parenthesis parenthesis meta k peano imply meta 
k end parenthesis peano imply meta k end parenthesis
      end line
      line ell c because rule prime mp modus ponens ell a modus ponens ell 
b indeed
        parenthesis meta k peano imply parenthesis meta k peano imply meta 
k end parenthesis end parenthesis
          peano imply
        parenthesis meta k peano imply meta k end parenthesis
      end line
      line ell d because axiom prime a one indeed
        meta k peano imply parenthesis meta k peano imply meta k end 
parenthesis
      end line
      because rule prime mp modus ponens ell c modus ponens ell d indeed
        meta k peano imply meta k
      qed
    end math ]"
-----------------------


-Kasper Frederiksen