Re: Splitting, cut elimination and classical logic

On Thu, 21 Oct 2004, Alessio Guglielmi wrote:

> 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.

The basic idea is that splitting gives me for a proof

          _
          |
      [(P,Q),R]

three pieces:

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

which I can put together to get

          _
          |
     ([P,U],[Q,V])
 s,s -------------
      [(P,Q),U,V]
          |
      [(P,Q),R]

I want that this is "the same" proof as I started with. This is what my 
method gives me (if "the same" means the same proof net---Just give us 
another week to finish the proof net paper)

> 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.

from the point of view of proof nets, the two proofs are identical. If you 
apply splitting to one of them and then put the pieces together, you 
should end up with the other.
 
> Clearly, this example is the simplest manifestation of this 
> phenomenon, which can occur in arbitrarily complex situations. Does 
> your technique capture this migration?

Well, yes, in the way as I said above.

> 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.

The two proof are different (again, from the point of view of proof nets), 
and therefore, applying splitting to it must yield different results.
 
> Do we agree that this is the essence of the problem, together with 
> the fact that we don't want to generate complexity?

I did not get what you mean by "the problem". I just explained what my 
technique does. And I need exactly that to establish the relation between 
proof nets and the CoS, in the sense that cut elimination does the same 
thing on both sides. And I am confident that, in case we want, we will 
get some "computational meaning" out of it.

-Lutz