Splitting and cut elimination

Hello,

there has been a lot of discussion at and after the workshop about 
splitting and cut elimination. Not everybody was present in the days 
after the workshop and those that were there were very tired. I 
thought then to make a little exposition of the `state of the art', 
to fix ideas in writing, and also to collect suggestions from the 
absent.

As I argued in my talk, my ambition is to obtain a very general and 
natural methodology for cut elimination in a broad range of 
(propositional?) logics. The outcome could be something similar to 
the cut elimination criteria for the display formalism, but much 
simpler and more natural.

I think the main ideas are all already out, and what is needed in 
order to claim the result is some work to polish off the details and 
overcome the last obstacles. Nothing of what I say below is 
technically challenging or especially new, but I think it is 
important to start paying attention to the big picture and the 
possible outcomes.

In this email I'll talk prevalently of shallow splitting. Deep 
splitting is analogous and might be necessary for certain modal 
logics. The only difference is that the statement is more powerful, 
and so it's more difficult to prove (but not to state!). Besides cut 
elimination, other applications of splitting are, of course, in the 
reduction of proof search nondeterminism, but I won't talk about that 
here.

The general idea is exploiting Kai's cut elimination proof for other 
logics. In case you don't know Kai's technique, this email provides 
for all the necessary explanations. In a separate email I will make 
the point about the special case of splitting for classical logic.


KAI'S CUT ELIMINATION
=====================

The main ingredient for Kai's proof is being able to perform a 
substitution operation of one proof into another. Given the two proofs

       _               _
   Pi1 |     and   Pi2 |
       |               |
     S{a}            [R,-a]

one wants, in Pi1, to substitute R for all instances of atom a 
generated (going up in the proof) by the instance of the atom a 
shown. The only inference rules that are `broken' by this operation 
are atomic identities. For example, in Pi1, an atomic identity

        S'{t}
   ai_ --------
       S'[a,-a]

might become

      S'{t}
   ? -------- ;
     S'[R,-a]

this is not a valid inference and cannot be fixed by routine methods, 
since it is not even sound. However, given Pi2, we can fix the 
inference by simply replacing it by Pi2, in the context S'{ }.

In other cases the fix might be done simply by resorting to the rules 
of the system. For example, an atomic contraction

       S'[a,a]
   ac_ -------
        S'[a]

remains sound, by becoming

   S'[R,R]
   ------- ;
    S'[R]

this can be simply obtained in the system by atomic contraction and 
medial instances.

This mechanism is wonderfully simple and eliminates cuts the same way 
one does normalisation in natural deduction: by plugging proofs of 
lemmas into proofs that use them as axioms. This is *the* way it 
should be morally done and, of course, one wonders whether this can 
*always* be done for every logic for which cut is admissible. It's 
now clear that it can be done! (Continue reading...)

In the mechanism I've shown above there is nothing which is peculiar 
to classical logic. Moreover, it is very simple to check whether a 
formal system is suitable for it to work. The following definition is 
all one needs:

*** Definition   A deductive system is *Kai-esque* if every inference 
rule, apart from identity and cut, is such that all its instances in 
which an atom is substituted by a generic structure are derivable in 
the same system.

Checking this condition is trivial and, as far as I know, this holds 
for all the systems we've designed so far in the calculus of 
structures (which means tens). In general, there is no reason why a 
system should not be Kai-esque, because the only reasonable cause for 
breaking the property is dealing with negation, which is precisely 
the business of identity and cut, taken care of by the definition.

That established, let's move on. There is indeed something peculiar 
to classical logic in Kai's original proof, and this is what 
splitting theorems should avoid, or, better, make `conceptual'. So, 
my proposal is to combine Kai's technique with splitting in order to 
have a general methodology.

How does Kai prove cut elimination by employing the mechanism shown 
above? His proof uses features of classical logic in two steps he 
needs: 1) in the production of the two initial proofs; 2) in how they 
are used to get a final cut-free proof. Let's revise these two steps, 
and let's make the position that we operate in system KS (plus cut, 
in case):

1 GENERATION OF THE TWO PROOFS
------------------------------

One starts with a proof Pi whose only atomic cut is at the bottom:

           _
        Pi'|
           |
       [R,(a,-a)]
   ai^ ---------- .
           R

In this proof, we can replace either a or -a, and all the atom 
instances they generate, by the unit t. Since KS is Kai-esque, we 
only break atomic identity rules, but they can be fixed, *in this 
special case*, by resorting to (atomic) weakening; example:

        S{t}                    S{t}
   ai_ -------   becomes   aw_ ------- .
       S[a,-a]                 S[t,-a]

So, from Pi' we can produce two proofs
       _               _
   Pi1 |     and   Pi2 |   ,
       |               |
     [R,a]           [R,-a]

but we can do so only because we have weakening.

2 CREATION OF THE CUT FREE PROOF
--------------------------------

We can now plug Pi2 into Pi1, after substituting R for a in Pi1, and 
so fixing a broken Pi1, according to the mechanism explained above. 
By doing so we get a proof

     _
     |  ,
     |
   [R,R]

which is cut free but not quite what we want. But then, it's easy to 
get a cut free proof of R: simply use contraction, which is derivable 
in KS by way of atomic contraction and medial; so we get

        _
        |
        |
      [R,R]
   c_ ----- .
        R

Clearly, we need contraction for this trick to work, and contraction 
is peculiar to classical logic.


SPLITTING
=========

A splitting methodology fixes the dependency on classical logic of 
the two steps above.

A splitting statement depends on a cut-free deductive system (in deep 
inference, but not necessarily in CoS) and a logical relation 
different from the one used for interaction (disjunction, normally). 
For example, splitting for KS (propositional classical logic in CoS) 
and conjunction is a statement of the following kind:

*** Theorem (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 is not the whole story about splitting. I would add two 
requirements for calling such a theorem `splitting': 1) a 
constructive proof, and 2) some strict bounds on the size of the 
derivations involved in the theorem. More on this in the next email.

A theorem like this immediately connects with the notion of Kai-esque 
system and produces a cut elimination proof.

In fact, suppose we start from

           _
        Pi |
           |
       [R,(a,-a)]
   ai^ ---------- ,
           R

as before. Splitting gives us

               _             _
   [U,V]       |             |
     |   ,     |     and     |    ;
     R       [a,U]         [-a,V]

We can combine the two proofs into a proof of [U,V] by using the 
mechanism explained above, and then we can paste the pieces together 
into

     _
     |
     |
   [U,V] ,
     |
     R

so avoiding the two problems peculiar to classical logic outlined above.

*Of course*, one could remark that we didn't do much more than 
rolling the two peculiarities into a special theorem, so what's the 
point? The point is that theorems of exactly this shape seem 
particularly common, albeit sometimes difficult to prove, at least if 
we insist on constructiveness and bounds. So far, there exist 
splitting theorems for classical logic and all fragments of linear 
logic and for BV and NEL.

One improvement over Kai's technique of a well-done splitting theorem 
with strict bounds should be in the size of the normalised proof. In 
fact, Kai duplicates everything, while a good splitting theorem 
should be able to generate two `initial' proofs which are reduced to 
the bare necessary for `killing' a and -a.

By looking at the proofs of these statements (in the papers, not in 
this email), one cannot fail to observe that splitting checks the 
internal symmetries of the given system in a similar way to a 
traditional cut elimination procedure in the sequent calculus.

Proving splitting for classical logic is particularly simple if one 
uses the peculiarities of the logic (see next email), but what is at 
stake here is trying to understand a *general* criterion, or 
understanding, which tells us *why* this theorem works so well and 
for so many logics.

After analysing many cases involved in the splitting statements, one 
notices regularities that should lead us to this kind of 
understanding. This is certainly true when no modalities and medial 
rules are involved.

This, basically, was the message of my talk at the workshop:

             cut elimination = Kai + splitting ,

   efficient cut elimination = Kai + splitting with strict bounds.


DEEP SPLITTING
==============

The methods above work for shallow, atomic cut rules like

       [R,(a,-a)]
   ai^ ---------- .
           R

In all deep inference systems cut is reducible to atomic form (which 
basically is why these methods cannot be used in the sequent 
calculus, if I'm not mistaken), so this is not a problem.

It might be a problem to reduce (trivially) the use of cut to its 
shallow version. This can be done trivially in systems without 
modalities, by simply using switches and alike. If this turned out to 
be impossible or inconvenient, then one can modify, in an obvious 
way, the technique for using a deep splitting theorem; example:

*** Theorem (Deep Splitting)    In KS, for every S{ }, P, Q and for every proof

     _
     |
   S(P,Q)

there exist U, V and derivations such that

                   _             _
   [{ },U,V]       |             |
       |     ,     |     and     |   .
     S{ }        [P,U]         [Q,V]

There are deep splitting statements in the papers about BV and NEL 
(and Lutz's thesis). I think so far we proved these theorems starting 
from shallow splitting ones and then lifting them up via so called 
context reduction theorems.

Please let me know if you disagree on any of the above. Could very 
well be that I'm missing something: I'm even more unreliable than 
usual because I've got some kind of cold/flu and profited of my 
diet's suspension (due to the workshop) for drinking a bit of beer.

-Alessio