Decomposition for classical logic

Dear Frogs,

Let us consider the symmetric version of the nonlocal system for classical 
logic in the CoS, consisting of the rules ai_, ai^, s, c_, c^, w_, w^, i.e., 
atomic identity and cut, switch, and (general) contraction and weakening (up 
and down). The details can be found in Kai's thesis (BUY IT!)

In the thesis Kai states the conjecture that every derivation in that system 
can be decomposed into

  P
  | c^
  P1
  | w^
  P2
  | ai_
  P3 
  | s
  Q3
  | ai^
  Q2
  | w_
  Q1
  | c_
  Q

separating core and non-core.

It should be mentioned here (because it is nowhere published) that we 
actually KNOW that this is true, i.e., it should be stated as theorem. 
The rather simple proof uses however cut elimination within the sequent 
calculus. The problem is, of course, finding a proof that is 
1. independent from the sequent calculus and 
2. independent from cut elimination.  
Recent investigations by Kai and myself show that 1. is easy to reach. 
(However, 2. remains difficult)

We plan to write a paper about this, including also the following observation:
From the decomposition above, we can easily get interpolation as a 
decomposition of the form 

  P
  | c^
  P1
  | w^
  P2
  | s
  P4
  | ai^
  I 
  | ai_
  Q4
  | s
  Q3
  | w_
  Q1
  | c_
  Q

using the techniques I developped for linear logic in my thesis. As it has 
been observed much earlier on this list, cut elimination is an immediate 
consequence of this form of interpolation.

Thus, we have that in the CoS, cut elimination, decomposition and 
interpolation are immediate consequences of each other. There is no need of 
doing an induction on the cut-free sequent proof. It is just obvious from the 
way proofs are written in the CoS. In Alessio's "Formalism A", we could make 
it probably even more obvious.

The nice thing about all these proof transformations is that they get well 
along with my proof nets. This means that they do not change the underlying 
net of the derivation.

Best wishes,
Lutz