Re: Re: Re: Extension

Hello,

The discussion with Lutz is becoming technical and somewhat 
repetitive, and I'm reluctant to continue sending messages to more 
than 100 people. On the other hand, I think that this exchange is 
interesting because it touches some nontrivial issues.

Perhaps somebody is interested in continuing the discussion in a more 
private form. So, whoever is interested, please tell me and I'll make 
a private list for the rest of this exchange. I'll wait until 
tomorrow before replying to the last post by Lutz.

Since the issues at stakes are now clear, I summarise here my 
position on the subject and then I'll stay quiet (on Frogs; I'll keep 
jerking privately):

1) I don't attack Lutz's technical results (some of which are nice 
and important, like the balanced tautologies).

2) However, I take issue with a) the claim that adding his extension 
to (one or two) cut-free systems has the same universal value as 
adding Tseitin's extension to Frege or Gentzen formalisms; and I take 
issue with b) the methodology used, especially because units play a 
role. I think that this is a serious mistake.

3) The universal value of separating extension and cut can only come 
from a robustness theorem (Lutz seems to agree on this).

4) In order to prove a robustness theorem, one needs a robust, i.e., 
syntax-independent, notion of cut-free *formalism* (so, not just one 
or two systems, but an entire class of systems). The same happens for 
robustness of Gentzen, Frege, their dag/tree variants and the 
extension/substitution variants of Frege. Right now we are starting 
to have such a syntax-independent notion of cut-freeness, thanks to 
atomic flows, but much more experience with them is needed before 
making any bold claims. Moreover, other characterisations might well 
be possible. (Lutz does not even take into consideration the need for 
such a syntax-independent view of cut-free formalisms.)

5) The units are a fixed part of proofs: semantically, they belong to 
the logical structure that keeps atoms together. In fact, what varies 
in the models is the truth value of atoms, and this is the only thing 
that should matter. Using units or not in proofs is and should be 
just a matter of convenience.

6) Consequently, as soon as I see that units discriminate between 
separation and nonseparation of extension and cut, and especially if 
this depends on a very delicate choice of unit equations, a big RED 
ALERT flashes in my mind and I launch the interceptors.

7) This issues should at least be mentioned in a paper that claims to 
separate extension and cut, because the paper does the trick for one 
system, while all the papers and textbooks on the subject of 
extending formalisms do so for formalisms, not just single systems.

My 7 cents. More details privately for the masochist (let me know who you are).

-Alessio