Subject: Re:Proof Nets, Boolean Categories, and Medial
Newsgroups: gmane.science.mathematics.frogs
Date: 2005-12-22 21:26:48 GMT (2 years, 20 weeks, 17 hours and 13 minutes ago)
At 14:57 +0100 22/12/05, lutz@... 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