Re: Two more FAQ entries

On Tue, 31 Aug 2004, Alessio Guglielmi wrote:

> Lutz,
> 
> I don't understand your remark. Take
> 
>     +----+   +----+
>     |    |   |    |
>     a   -a   a   -a
>      \   |   |   /
>       \  +---+  / .
>        \       /
>         \     /
>          \   /
>          a P -a
> 
> How am I supposed to turn around this? 

like this:

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


> Same problem if I remove the 
> bottom par, 

Yes, it is the same.

> what do I do with the cut link? 

it becomes an identity link.

> What do I do if I have 
> three conclusions?

you do the same thing.
 
> 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.

The reason is that people perceive proof nets in the wrong way, which makes 
the symmetry between cut and identity a partial symmetry.

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

OK. I did not make myself clear. In order to settle the terminology, let us 
forget about proofs, and only talk about derivations (this is what I had in 
mind). The example you gave represents a derivation from "1" to "a P -a". By 
turning the net arround (as shown above), you get something that represents a 
derivation from "a X -a" to "bot". In fact, it is the dual derivation to what 
we had before.
 
> 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!! 

Right. The dual of a proof is a refutation. But morally it is the same thing, 
and in terms of "proof nets" (maybe the name is misleading) it is represented 
by the same object (see above).
 
> You clearly have something else 
> in mind than ordinary proof nets.

This depends on the viewpoint. You can say that ordinary proof nets are 
morally different, but technically, we talk about the same objects.

-Lutz