Re: Two more FAQ entries

On proofnets and duals of proofs:

I think that this feature of traditional proofnets is an inessential 
feature.  You *could* define proofnet like structures as directed 
graphs, where the sequent X |- Y is given a proof with inputs X and 
ouptuts Y.  In this case, the dual of the proof (reversing arrows, and 
replacing connectives by their duals) would give you a proof of Y^d |- 
X^d rather trivially.  The cost of this is the duplication of rules 
(the &E is not the same rule as vI on this approach: the one is the 
mirror image of the other).  The virtue is the generality and the 
greater similarity to traditional natural deduction proofs.

This is the behaviour of the proofnet-like proof graphs for lattice 
logic discussed by me and Francesco Paoli in the paper I advertised a 
while ago (see http://consequently.org/writing/gndl/ ).

Greg


On 30/08/2004, at 8:09 PM, 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