Re: Two more FAQ entries

Lutz,

I don't understand your remark. Take

    +----+   +----+
    |    |   |    |
    a   -a   a   -a
     \   |   |   /
      \  +---+  / .
       \       /
        \     /
         \   /
         a P -a

How am I supposed to turn around this? Same problem if I remove the 
bottom par, what do I do with the cut link? What do I do if I have 
three conclusions?

The problem addressed by the FAQ is that some people consider proof 
nets top-down symmetric because the identity and cut links look so, 
contrary to the sequent calculus. The point I'm trying to make is 
that this only a very partial symmetry, it's still not perfect.

I also don't understand your final remark. In CoS, you can flip 
around the vertical axis any derivation, not just proofs, while proof 
nets are just proofs, and this is an inherent reason for them to be 
asymmetric.

How can it be that the dual of a proof yields the same proof net? The 
dual of a proof is not even a proof!! You clearly have something else 
in mind than ordinary proof nets.

-Alessio


At 12:09 +0200 30.8.04, Lutz Strassburger wrote:
>On Saturday 28 August 2004 19:53, Alessio Guglielmi wrote:
>>  Hi,
>>
>>  it's me again. Two more entries for the FAQ, please comment. In
>>  general, do you have any complaint or suggestion for the FAQ page?
>>
>>  -Alessio
>>
>>
>>  *** Question   Aren't proof nets top-down symmetric objects, not
>>  differently than proofs in the calculus of structures?
>>
>>  *** Answer   No, proof nets are top-down asymmetric: they consist of
>>  trees with some links on top (in the simplest case of multiplicative
>>  linear logic). If you flip a proof net upside-down, you don't get a
>>  dual proof net, just an upside-down one.
>
>Alessio,
>
>I do not (entirely) agree on this point. The problem is that proof nets are
>usually drawn the wrong way (ie assymmetric). But actually, they are
>symmetric: If you take for example a PN (say for MLL) with two conclusions A
>and B, then you can draw that object with the two conclusions down and the
>links above (the usual way), or you can draw it with A on top and B at the
>bottom and the links in between, or the other way arround, or both formulas
>at the top, and all the links at the bottom.
>The only important point is that we do not get a "dual proof net", but the
>same proof net. Maybe that is the real difference: if you take a CoS
>derivation an its dual, they yield the same proof net.
>
>-Lutz