Re: Re: Re: Re: Extension

On Mar 3, 2010, at 6:03 AM, Alessio Guglielmi wrote:

> Hello,
>=20
> 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.
>=20
> 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.
>=20
> 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):
>=20
> 1) I don't attack Lutz's technical results (some of which are nice and =
important, like the balanced tautologies).
>=20
> 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.
>=20
> 3) The universal value of separating extension and cut can only come =
from a robustness theorem (Lutz seems to agree on this).
>=20
> 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.)
>=20
> 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.
>=20
> 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.
>=20
> 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.
>=20
> My 7 cents. More details privately for the masochist (let me know who =
you are).
>=20
> -Alessio