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.


I’m Greg Restall, and this is my personal website. I am the Shelby Cullom Davis Professor of Philosophy at the University of St Andrews, and the Director of the Arché Philosophical Research Centre for Logic, Language, Metaphysics and Epistemology I like thinking about – and helping other people think about – logic and philosophy and the many different ways they can inform each other.


To receive updates from this site, subscribe to the RSS feed in your feed reader. Alternatively, follow me at  @consequently@hcommons.social, where most updates are posted.


This site is powered by Netlify, GitHub, Hugo, Bootstrap, and coffee.   ¶   © 1992– Greg Restall.