Splitting for classical logic

Hello,

as I said, there have been discussions about splitting for classical 
logic at the workshop. My impression is that some of the points that 
I was considering `obvious' might not have gone through. In 
particular, I don't want anybody to have the impression that 
splitting for classical logic is not proved, albeit it's true that it 
doesn't appear in any paper (yet). So, let's put the record straight.

First of all, let's consider a plain vanilla splitting statement like 
the one I posted before:


*** Theorem 1 (Shallow Splitting)    In KS, for every P, Q, R and for 
every proof

        _
        |
    [(P,Q),R]

there exist U, V and derivations such that

                _             _
    [U,V]       |             |
      |   ,     |     and     |   .
      R       [P,U]         [Q,V]


This theorem can be restated as


*** Theorem 2 (Shallow Splitting)    In KS, for every P, Q, R and for 
every proof

        _
        |
    [(P,Q),R]

there exist derivations such that

                _             _
    [R,R]       |             |
      |   ,     |     and     |   .
      R       [P,R]         [Q,R]


Proving this theorem is a *complete triviality* after simply 
observing that KS is complete for classical logic, and then [P,R] and 
[Q,R] must be provable if [(P,Q),R] is. The problem with this proof 
is that it's not constructive!

Of course, we can further specialise the theorem as in


*** Theorem 3 (Shallow Splitting)    In KS, for every a, -a, R and 
for every proof

        _
        |
    [(a,-a),R]

there exist derivations such that

                _              _
    [R,R]       |              |
      |   ,     |     and      |   .
      R       [a,R]         [-a,R]


This is exactly what Kai uses in his proof, in disguised form. Of 
course, he proves this constructively.

If constructiveness is all one wants, then it is possible to prove 
Theorem 2 constructively with the same technique that Kai uses for 
Theorem 3. For example, take

        _
        |
    [(P,Q),R]

and replace atoms in Q one by one by t, follow up their occurrences 
and turn broken atomic identities into weakenings, and finally get

      _
      |
      |   .
    [P,R]

So, constructive shallow splitting for propositional classical logic 
*exists* and it's a triviality! (If I'm not terribly mistaken: I 
confess that I never took pencil and paper and carefully checked 
this...) At least now it's written somewhere.

By the way, this is enough to say that proof search nondeterminism in 
KS is not worse than that in the sequent calculus.

OK, so, what's the problem? The main one is the size of the proofs so 
produced. The two proofs produced by the theorem are involved in the 
substitution mechanism, where their sizes basically multiply. This is 
then repeated for as many times as there are cuts, with bigger 
proofs, and this produces the final exponential size. This is by no 
means bad, but we can do better!

One can note that by replacing atoms by t, a few inference rules 
might become trivial and safely removed, but in general the size of 
the proof so produced remains the same. It's also true that some 
identities become weakenings, so they contribute less to the final 
combinatorial explosion, but still...

The point is that we can hope for much more. Consider Theorem 1, in 
the special case in which P = a and Q = -a. What is a minimal U we 
can hope of generating? It can be something like

    U = (-a,...,-a) ,

meaning that the proof of [a,U] is made by as many atomic 
contractions (minus one) and atomic identities as there are atoms in 
U, *and nothing else*. In other words, it should be possible to 
filter down all unnecessary stuff for cut elimination in the 
derivation that `produces' U and V from R, and that part is *not* 
involved in the substitution mechanism.

This is the quantitative part of the business, the qualitative one 
being the fact that it's not at all satisfactory, in my mind, to 
duplicate entire proofs without being able to get inside and 
rearrange the stuff according to finer criteria. I guess doing this 
is the qualifying aspect of deep inference, after all. I should add 
that, for all the reasons explained above, I consider splitting 
theorems as one of the main guides we have along the road for 
deductive proof nets.

This is why I'm insisting so much into splitting statements which 
contain bounds on the size of proofs generated. Am I missing 
anything? Apart from all I said now, there is this business of being 
able to understand the general pattern of why and how cut elimination 
works and discover criteria for that, which is of course not revealed 
by resorting to substitution/weakening as in the tricks above for 
classical logic.

BY THE WAY: Since a couple of years there is a splitting `proof' of 
mine for classical logic which circulates in the form of handwritten 
notes. Roy Dyckhoff found a mistake in that proof. The statement 
about classical logic without medial (KS1) still looks correct after 
Roy's and others' scrutiny (and makes precisely the point I think 
splitting theorems should make). However, the statement about the 
whole system is wrong: it uses the statement for KS1 as a lemma, but 
this is incorrect (can you spot the problem, Charles?).

I'm working to this theorem myself, but of course everybody is 
welcome to try and find a satisfying solution along the lines I 
explained above.

Speaking of which: there wasn't much time to discuss because Lutz had 
to leave, so perhaps we can do so on the list. Lutz has a splitting 
proof for classical logic, but for a different system than KS (no 
medial, in particular). I don't think this solves the problem as I 
stated it, because if we have to look for general criteria, we 
probably want to deal with medial, since this rule pops up so often, 
also in completely unrelated systems and in different shapes, like 
unary versions for classical logic. But let's discuss the pros and 
cons.

Enough for today. Buonanotte.

-Alessio