Re: Splitting, cut elimination and classical logic

On Thu, 7 Oct 2004, Alessio Guglielmi wrote:
> Hi,
> 
> answers to Kai and Lutz:
> 
> Are you sure that what you're doing is correct? 
> The fact that you get splitting for {ai_, s, m} 
> looks very suspicious to me. Consider P = [a,c], 
> Q = [b,-a], R = [-c,-b] (see a splitting 
> statement below) and the proof
> 
>                  t
>            ai_ ------
>                [b,-b]
>        ai_ ---------------
>            [([a,-a],b),-b]
>          s ---------------
>             [(a,b),-a,-b]
>     ai_ ----------------------
>         [(a,b),([c,-c],-a),-b]
>       s ----------------------
>          [(a,b),(c,-a),-c,-b]
>       m ---------------------- .
>         [([a,c],[b,-a]),-c,-b]
> 
> I don't see how you can get rid of a and -a in 
> the `split' proofs, without weakening.

OK. Sorry. We have to reformulate the statement a bit.
 
> *** 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]

If we replace KS by {ai_, s, m}, we have to add:
"provided that P and Q do not contain complementary atoms that kill each 
other in an instance of ai_ ."
(Alternatively we could also allow weakening.)
I forgot to mention that because I was already thinking in terms of 
"derivation nets".

Best,
Lutz