[Logiweb] * proof of * reads *

[Ole Hyldahl Hansen]

On Sun, 26 Jun 2005, Martin Røpcke wrote:

> Hi,
> I'm trying to use the construct
>
> * proof of * reads *
>
> and constantly get a NO INTERPRETATIONS error. The construct is defined on 
> check page, and it is used on peano page, which does not refer to check. 
> Nevertheless, the construct is used on peano page. How is that possible? I'm 
> obviously missing something.

How the peano page can get away with using the construct without referring 
to the defining page I do not know. Maybe it is defined (also) on the base 
page?

>
> I get the error when including this:
>
> "[ math
> system prime s proof of mendelson lemma one eight reads
> arbitrary meta b end line end math ]"
>
> If I include "PREASSOCIATIVE check: * proof of * reads *" in my page, I get 
> as far as end line, which then has no interpretation. Is there something I 
> should read (or reread) in some page? Any advice will be much appreciated.

Try to add another line to the proof like this
"[ math
 	system prime s proof of mendelson lemma one eight reads

 	arbitrary meta b end line

 	because axiom prime a one indeed
 	meta b peano imply meta b peano imply meta b

 	qed
end math ]"

You should get a lemma/proof mismatch with this one. The syntactic rules 
for proofs are not always obvious.

Regards,
Ole Hyldahl Hansen