Re: Two more FAQ entries

(Lutz ">", Alessio ">>")

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

I think that there is a serious problem with what Lutz is saying: it
is possible to give a simple, natural, inductive definition for proof
nets of the kind that Alessio is considering; to extend it to cover
flippings of the Lutz can be achieved in an unnatural way (by having
it be the disjoint union of two inductively defined classes of 
diagram) or in a natural but complex way (where arbitrary fragments
of proof nets can be defined, along the lines of Lafont's diagrams),
but I think there is nothing both natural that includes both the
regular proof nets and their flippings, and that is as simple to define
as the regular proof nets.

Charles