[Logiweb] "Repetition" & Macro definitions & Error message

[Frederik Eriksen]

Hi logiweb at diku.dk,

I have three questions:

1. I'm currently working with an axiomatic system which looks a lot like 
system S from Klaus Grue's ijcar-article 
(http://www.diku.dk/~grue/logiweb/20060417/home/grue/ijcar). The only 
difference is that I've replaced the axiom called Neg with axiom A3 from 
Mendelson. In the article, Klaus proves the lemma "Repetition" (i.e. A 
|- A) using a low-level hack which I haven't quite understood (as yet). 
Is there another, more neat way to prove "Repetition"?

2. Suppose you have macro defined "A ^ B" as "~(A => ~B)". When you're 
writing a proof of, say, the lemma (A ^B |- A), you may want to write a 
proof line saying "A ^ B really means ~(A=>~B)" in order to make things 
clearer for the human reader. Is there a way to do this?

3. In one of my proofs I get the error message "Metageneralization over 
metavariable that occurs free in some premise". What does this mean? 
(I've made the faulty page accessible on "user eriksen"s home page under 
the name of "frozen").

Best Regards
Frederik Eriksen.