[Logiweb] Metavariables in side conditions ?

[Klaus Ebbe Grue]

Hi Allan

> I am trying to do something like this in a proof with the "peano 
> axioms"-page:
>
> line ell a because axiom prime a four at meta q indeed
> peano all peano w indeed peano w peano imply meta q end line
>
> But I get this error-message in the diagnose:
>  "The verify operation requires the side condition to contain no 
> metavariables."

In the following, small letters denote peano variables and capital 
letters denote meta-variables. Capital A, however, denotes universal 
quantification.

You try to prove Aw:w => Q for all terms Q, and the system protests 
because of Q (it could protest against other things also, but Q happens 
to be the first thing Logiweb deprecates).

Whenever you use an axiom that has a side condition, you have to 
instantiate it fully, e.g.

   A4 >> Av:v=v => w=w

If you say e.g. A4 >> Av:v=v => W=W then Logiweb would have to realize 
that W=W is an instance of v=v ***for all terms W***. Even though that is 
trivial to see for us, it is beyond the capabilities of Logiweb.

That motivates the rule: no meta-variables are allowed in side conditions 
after instantiation.

Due to this restriction, I suggest you prove t+r=r+t instead of T+R=R+T, 
i.e. that you prove commutativity of addition for two concrete variables t 
and r instead of two meta-variables T and R.

Klaus

PS. It is not completely true that meta-variables cannot occur in side 
conditions. It is possible to prove lemmas of type S ||- Q by assuming 
that the side condition S holds and then proving Q under that assumption.
In this case S is allowed to contain meta-variables. I will put an example 
of that on Logiweb later.