Re: Bureaucracy and identity

Hi Frogs,

Since we had recently this interesting dicussion on bureaucracy and 
identity of proofs on this list, I'd like to announce the paper "From Deep 
Inference to Proof Nets" which I wrote more or less at the same time when 
the discussion was going on. It can be found here:

http://www.ps.uni-sb.de/~lutz/papers/deepnet.ps

I have kept the paper rather informal, explaining the basic idea how to 
translate deep inference derivations into proof nets. Interestingly, on 
the way, we meet nets for Formalism A.

In order to capture Formalism B, we would need Alessio's "pipes". It would 
be interesting to see how these gadgets can be incorporated into proof 
nets.

An interesting observation is that we obtain nets, which form a "Boolean 
category" which is not idempotent. The homsets are equipped with a 
semigroup structure (the usual sum of proofs) and a partial order 
structure (cut elimination).
BUT: the two structures are NOT RELATED via f<=g iff f+g=g.

cheers,
Lutz