[Logiweb] Naming variables in proofs

[Frederik Eriksen]

Hi logiweb at diku.dk

It seems to me that sometimes it makes a difference how you name the 
variables of your proof. For instance, I have tried to prove the 
following lemma in the theory "system prime s" from the "peano axioms" page:

For all X, A and B:  X -> A -> B    |-     X -> A     |-     X->B

(Here "->" is "peano imply", while "|-" is "infer"). The proof is just 
eight lines, all included: Use"Arbitrary" three times, state the two 
premises, instantiate axiom schema A2' appropriately, and use MP' twice. 
However, pyk doesn't accept this proof. The diagnosis page says 
"Quantifier elimination leads to variable clash" (and some more things 
that I don't understand).

The point is that all goes well if I substitute "D" for "X", "E" for "A" 
and "F" for "B" in the lemma and the proof, so that I end up proving:

For all D, E and F:  D -> E -> F    |-     D -> E     |-     D->F

Is there a way to get around this problem?

Best Regards
Frederik.