A Concrete Category of Classical Proofs

June 28, 2017

Abstract: I show that the cut-free proof terms defined in my paper “Proof Terms for Classical Derivations” form a well-behaved category. I show that the category is not Cartesian—and that we’d be wrong to expect it 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 an invited address, for TACL 2017, in Prague.

• The slides are available here.