[Logiweb] PS: New peano page

[Klaus Ebbe Grue]

Hi Logiweb at diku.dk,

As a PS to the previous posting: The new peano page contains a comment 
right after Lemma M3.2(f) which is wrong. It says:

The proof below uses local definitions. Use only  raw  variables [a], [b], 
and so on for local definitions. Never use peano variables or 
meta-variables...

That is confusing since the proof right after uses local definitions of 
the meta-variables z and h. I wrote the comment before I realized that 
local definitions of peano variables and meta-variables works fine.

Actually, it is the raw variables that one should be a little bit cautious 
about using. This is so because, behind the scene, a meta-z is just the 
raw variable z with a 'meta-mark' on it (look up the macro aspect of 
meta-z to see how this is done). A local macro definition of the raw 
variable z could very well expand instanses of the raw variable z with a 
meta-mark on it so that a local definition of raw z may affect meta-z with 
incomprehensible results.

Klaus