Re:Proof Nets, Boolean Categories, and Medial

At 14:57 +0100 22/12/05, lutz-TgEOGOHWQm0czSlqHMVBIP3zm4ADWneb@xxxxxxxxxxxxxxxx 
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