Re: Two more FAQ entries

On Tuesday 31 August 2004 12:01, Charles Stewart wrote:
> (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

I disagree on that. The definition is as simple as the definition of ordinary 
proof nets, simply because from a graph theoretical point of view it is the 
same thing. There is nothing mysterious or complex here. It is a triviality. 
All you have to do is to make sure that all cuts and identities are atomic 
(you can do without that restriction, but then it is a little more 
complicated).
Now you have a formula forest on the top, a formula forest on the bottom, and 
a bunch of wires connecting dual atoms.
(For MLL this is enough, for classical logic it is a little more complicated, 
but essentially the same idea)

-Lutz