Subject: Proof Nets, Boolean Categories, and Medial
Newsgroups: gmane.science.mathematics.frogs
Date: 2005-12-22 14:52:41 GMT (2 years, 20 weeks, 20 hours and 49 minutes ago)
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