A Category of Classical Proofs

May 19, 2017

Abstract: I show that the cut-free proof terms defined in my paper “Proof Terms for Classical Derivations” form a well-behaved category. The talk is intended to be accessible enough for those who don’t know any category theory to follow along. I show that the category is not Cartesian – and that we’d be wrong to expect to be. It has no products or coproducts, nor any initial or final objects. Nonetheless, it is quite well behaved.

I show that the term category is star autonomous (so it fits well within the family of categories for multiplicative linear logic), with internal monoids and comonoids taking care of weakening and contraction. The category is enriched in the category of semilattices, as proofs are closed under the blend rule (also called “mix” in the literature).

This is a talk presented at the Melbourne Logic Seminar.

• The slides are available here.