Re: Two more FAQ entries

Lutz:
 
> 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)

General graph-shaped objects, and even DAGs, are more complex to formalise 
and reason about than tree-shaped objects.  If you formalise the usual 
notion of proof net using graph theoretic machinery, then of course there
is little difference in complexity.

I think your notion of proof net is fundamentally more complex than
mine.

Charles