Proof Nets, Boolean Categories, and Medial

Hi Frogs,

Recently this list has seen some discussion on the identity of proofs. It
seems that for Boolean propositional logic there is no obvious canonical
way of providing a theory of proof identity. There are two extremes: on
one side the collapse to the Boolean algebra, i.e., all proofs of the same
formula are the same, and on the other side no identification at all, 
i.e., two proofs are the same if they are syntactically equal.

Between these two extremes there is a rich universe. I've put some 
effort in investigating this universe. A paper on this can be found 
here:

http://www.lix.polytechnique.fr/~lutz/papers/medial.pdf

I used category theory because it provides the right language for a
systematic treatment. Interestingly the medial map, which corresponds 
to the medial rule of system SKS, plays an important role.

In the end of the manuscript, I show that proof nets are a conrete example
obeying the category theoretical axiomatisations discussed before. This
last section might also be interesting for people who are not interested
in categories.

Happy Christmas holidays to everybody,
Lutz