Re: Splitting, cut elimination and classical logic

At 18:05 +0200 21.10.04, Lutz Strassburger wrote:
>  > 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.

OK, I think it's finally clear what we are doing differently.

I want exactly the opposite of what you have: I don't want the two 
proofs to be identical. There is a phenomenon of migration of medial 
which I want to capture, because it is relevant from the deductive 
viewpoint (which is a different viewpoint than that of your proof 
nets).

In one proof you have medial on the left, in the other you have 
medial on the right, and of course you can embed those medials into 
very complex situations, which means that you can amplify the 
difference quite a bit, always from a deductive viewpoint.

This is why I think (my version of) splitting is very relevant for 
getting to deductive proof nets: we should be able to observe these 
phenomena, like medial migration.

Just not to be misunderstood: I very much like what you're doing, 
simply, it's not what I'm after. You're getting a very concrete 
semantics, I'm still after a very abstract syntax.

-Alessio