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

[Klaus Ebbe Grue]

Hi Frederik

> 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"?

I don't know of a neat way if neat means 'expressed the usual way'. 
The proof I give uses the raw sequent operators. A^I is the identitity 
sequent operator applied to A which yields A|-A. The Pi operator expresses 
meta-generalization and changes A|-A to Pi A:A|-A which is the repetition 
lemma.

> 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?

Yes. Use repetition! As an example:

L01: Premise >> A ^ B;
L02: Repetition |> L01 >> ~(A=>~B);
...

Proofs are checked *after* macro expansion, and after macro expansion, L01 
and L02 above are identical, so the latter follows from the former by 
repetition.

> 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").

The lemma and proof read:

Lemma Technicality: Pi A,B: A => B |- ~ ~ A => B

Proof of Techincality:
L01: Arbitrary >> A,B;
L02: Premise >> A => B;
L03: Block >> Begin;
L04: Arbitrary >> A,B;
L05: Premise >> ~ ~ A;
L06: RemoveDoubleNeg |> L05 >> A;
L07: MP |> L02 |> L06 >> B;
L08: Block >> End;
L09: Ded |> L08 >> ~ ~ A => B

The problem is in L04. 'Arbitrary A,B' is a meta-generalization over A and 
B. But A and B occur free in the premise in L02. That is what the system 
complains about.

At the semantic level, the proof says:

L01: Let A and B be arbitrary terms;
L02: Assume A => B;
L04: Now let A and B be two arbitrary terms that have no connection with 
the ones called A and B in L01;
L05: Assume ~ ~ A;
L06: Remove double negation: A;
L07: From L02 and L06 we have B;

At the semantic level it would be more reasonable to say that the error 
is in line L07 where A => B from L02 is combined with A from L06 even 
though the two A's are unrelated.

Finally, how to correct the proof? Try removing L04! Then the A in L05-L07 
is the same as the one in L01-L02. And similarly for B. I hope it works. 
Otherwise I have to correct Ded.

-Klaus