Re: Splitting, cut elimination and classical logic

At 15:07 +0200 8.10.04, Lutz Strassburger wrote:
> On Thu, 7 Oct 2004, Alessio Guglielmi wrote:
>  > Are you sure that what you're doing is correct?
>
> 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.)

Ah, OK, now it makes sense: medial doesn't work without weakening!

It's just an observation: all instances of medial apply to a logical 
relation for which weakening applies. This is true for all of linear 
logic and also for the unary instances of medial: see page 146 of 
Lutz's thesis, rules m, m1_, m2_, l1_ and l2_. It's probably not by 
chance!

<http://www.ki.inf.tu-dresden.de/%7elutz/dissvonlutz.pdf>

Anyway, you said that your technique has strict bounds on the size of 
generated proofs. Which bounds? Unfortunately, I recall nothing of 
your method, it would help if you could post some details.

Anyway, it's not enough (for my purposes) to have good bounds. Let's 
see whether we agree on what is the fundamental problem with medial.

Take

   S = [ ([a,b],[c,d]) , ([-a,-c],[-b,-d]) ] .

S is provable by a proof of the shape

                   _
                   | {s,ai_}
                   |
     [ (a,c),(b,d) ,([-a,-c],[-b,-d])]
   m --------------------------------- .
     [([a,b],[c,d]),([-a,-c],[-b,-d])]

However, it is also possible to prove it by a proof of this shape

                   _
                   | {s,ai_}
                   |
     [([a,b],[c,d]), (-a,-b),(-c,-d) ]
   m --------------------------------- .
     [([a,b],[c,d]),([-a,-c],[-b,-d])]

If P = [a,b] and Q = [c,d] and R = ([-a,-c],[-b,-d]), the splitting 
theorem should capture the `migration' of medial from the proof above 
(P,Q) to the generated proof above R.

Clearly, this example is the simplest manifestation of this 
phenomenon, which can occur in arbitrarily complex situations. Does 
your technique capture this migration?

Since I am at it, let me also show why medial and weakening behave in 
a complementary way, in the intuition I have about this subject. 
Consider a situation in which P and Q participate in a medial and 
then the generated pieces interact for getting a proof, like when P = 
[U,-V] and Q = [V,W] in

                  _
                  |
                  |
              [(U,W),R]
   s;s;i_ ------------------
          [ (U,V),(-V,W) ,R]
        m ------------------ .
          [([U,-V],[V,W]),R]

In this case, weakening can reduce the problem to

                 _
                 |
                 |
             [(U,W),R]
   w_;w_ ------------------ ,
         [([U,-V],[V,W]),R]

where, of course, the point is that P and Q *need not* communicate, 
and can then be separated into the two proofs generated by a 
splitting.

Do we agree that this is the essence of the problem, together with 
the fact that we don't want to generate complexity?

-Alessio