Syntax Independence?

Could you say something a little more exoteric about syntax independence,
what it means in general terms?

JA

--
=C2=A0
inquiry list: http://stderr.org/pipermail/inquiry/
mwb: http://www.mywikibiz.com/Directory:Jon_Awbrey
knol: http://knol.google.com/k/-/-/3fkwvf69kridz/1
oeiswiki: http://www.oeis.org/wiki/User:Jon_Awbrey
=C2=A0
=20=20
-------------- Original message ----------------------
From: Alessio Guglielmi <[email protected]>
>
> Hello,
>=20
> The discussion with Lutz is becoming technical and somewhat=20
> repetitive, and I'm reluctant to continue sending messages to more=20
> than 100 people. On the other hand, I think that this exchange is=20
> interesting because it touches some nontrivial issues.
>=20
> Perhaps somebody is interested in continuing the discussion in a more=20
> private form. So, whoever is interested, please tell me and I'll make=20
> a private list for the rest of this exchange. I'll wait until=20
> tomorrow before replying to the last post by Lutz.
>=20
> Since the issues at stakes are now clear, I summarise here my=20
> position on the subject and then I'll stay quiet (on Frogs; I'll keep=20
> jerking privately):
>=20
> 1) I don't attack Lutz's technical results (some of which are nice=20
> and important, like the balanced tautologies).
>=20
> 2) However, I take issue with a) the claim that adding his extension=20
> to (one or two) cut-free systems has the same universal value as=20
> adding Tseitin's extension to Frege or Gentzen formalisms; and I take=20
> issue with b) the methodology used, especially because units play a=20
> role. I think that this is a serious mistake.
>=20
> 3) The universal value of separating extension and cut can only come=20
> 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.,=20
> syntax-independent, notion of cut-free *formalism* (so, not just one=20
> or two systems, but an entire class of systems). The same happens for=20
> robustness of Gentzen, Frege, their dag/tree variants and the=20
> extension/substitution variants of Frege. Right now we are starting=20
> to have such a syntax-independent notion of cut-freeness, thanks to=20
> atomic flows, but much more experience with them is needed before=20
> making any bold claims. Moreover, other characterisations might well=20
> be possible. (Lutz does not even take into consideration the need for=20
> such a syntax-independent view of cut-free formalisms.)
>=20
> 5) The units are a fixed part of proofs: semantically, they belong to=20
> the logical structure that keeps atoms together. In fact, what varies=20
> in the models is the truth value of atoms, and this is the only thing=20
> that should matter. Using units or not in proofs is and should be=20
> just a matter of convenience.
>=20
> 6) Consequently, as soon as I see that units discriminate between=20
> separation and nonseparation of extension and cut, and especially if=20
> this depends on a very delicate choice of unit equations, a big RED=20
> 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=20
> separate extension and cut, because the paper does the trick for one=20
> system, while all the papers and textbooks on the subject of=20
> 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
>=20