Re:Proof Nets, Boolean Categories, and Medial

At 14:57 +0100 22/12/05, [email protected] wrote:
>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.

Lutz Skywalker!

>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



-Alessio