Re: Two more FAQ entries

Greg,

On Tuesday 31 August 2004 01:20, Greg Restall wrote:
> On proofnets and duals of proofs:
>
> I think that this feature of traditional proofnets is an inessential
> feature.  

I agree.

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

If the logic has a deMorgan duality, one can even do without duplication of 
rules (by consequently using the deMorgan duality, as it happens in one-sided 
sequent systems)

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

I'll have a look at it.

-Lutz