Re:Syntax Independence?

Hello,

At 14:14 +0000 3/3/10, Jon Awbrey wrote:
>Could you say something a little more exoteric about syntax independence,
>what it means in general terms?

More or less, a robustness theorem establishes the polynomial 
equivalence of all proof systems belonging to a certain formalism, 
independently of two syntactic factors:

1) the language of the formulae;
2) the axioms and inference rules adopted.

In this sense, we have syntax independence.

Of course, we require some conditions: concerning (1), we ask for the 
chosen set of connectives to be adequate (i.e., every boolean 
function is representable); concerning (2), we ask for the axioms and 
rules to form an implicationally complete system, (i.e., if A1,...,An 
|= B, then there is a proof of B from hypotheses A1, ..., An). Note 
that these conditions are only based on semantics.

For example, let's take the formalism of Frege proof systems, i.e., 
the usual Hilbert proof systems restricted to propositional logic. By 
definition, Frege systems are implicationally complete, and we want 
to prove a robustness theorem. So, we want to prove that each Frege 
system is able to simulate any other Frege system in polynomial time.

We address the language (1) and the axioms and rules (2) separately.

For the language part, we choose a canonical base of connectives, and 
we show that any formula in any language can be reduced to a 
canonical one in polynomial time. This requires a rather 
simple-minded and straightforward analysis of the formula tree, and 
is an argument that can be performed in every formalism, provided 
that they use formulae. This argument is due to Reckhow.

Let us now suppose that we want to polynomially simulate a proof 
system P by using another proof system Q.

For the axioms, we observe that every axiom scheme in P must be 
provable in Q by some proof (because Q is complete). Each instance of 
the axiom in P will then be simulated by an instance of the 
corresponding proof in Q, and the size of this instance depends 
linearly on the size of the formulae used to instantiate P and Q. 
This is so, because the size of the proof in Q simulating the axiom 
scheme in P is fixed.

For the rules, implicational completeness comes into play. Any rule scheme

    A1   ...   An
    -------------
          B

in P can be simulated by a proof scheme in Q of fixed size (this 
exists because Q is implicationally complete). Analogously to the 
case of axioms, the instances of these schemes only depend linearly 
on the size of formulae used to instantiate.

 From all this, the robustness theorem follows (Cook & Reckhow). Note 
that the argument is straightforward and simple, thanks to the rather 
strong requirement of implicational completeness.

Now, if we move to Gentzen formalisms or deep inference, we 
immediately see that implicational completeness is given (or taken 
away) by the presence (or absence) of the cut rule.

In fact, if A1,...,An |= B, completeness ensures that we can prove 
(A1 ^ ... ^ An) -> B, but only a cut rule (or something morally 
equivalent) can guarantee a proof of B from hypotheses A1, ..., An. 
For example, in the case of one hypothesis, we can build

              __
              ||
        A   A -> B
    cut ---------- .
            B

So, robustness can be immediately proved for Gentzen formalisms as it 
has been done for Frege. If we extend Frege or deep inference with 
substitution or Tseitin's extension, for example, again we can prove 
robustness, because we don't touch implicational completeness.

However, what happens when we remove the cut, and so we lose 
implicational completeness? We lose, at the same time, a way to 
define the *formalism* of cut-free systems, and a way to prove 
robustness for it. In other words, we lose syntax-independence. This 
is the problem that I have with Lutz: he shot his foot without even 
noticing it. Insensitive (we're friends, eh?).

I believe that, actually, syntax-independence, and so, robustness, 
can be obtained even for cut-free systems, but this requires: (1) a 
syntax-independent way to characterise cut-free systems, and (2) a 
technique to prove their polynomial equivalence.

As I said, a starting point might be the atomic flows, but there are 
other ways that come to mind. In any case, much has to be done before 
we can claim to deal with robustness for cut-free systems in the same 
sense as we do for Frege, and Gentzen and deep-inference systems with 
cut. BTW, this is a nice research subject, I think.

All we can do for now, which is what Lutz really is doing, is 
reasoning on single proof systems. This is, of course, interesting, 
but not syntax-independent and not robust.

Ciao,

-Alessio