On categorical models of classical logic and the Geometry of Interaction

It is well-known that weakening and contraction cause na¨ıve categorical models of the classical sequent calculus to collapse to Boolean lattices. In previous work, summarized briefly herein, we have provided a class of models called classical categories which is sound and complete and avoids this collapse by interpreting cut-reduction by a poset-enrichment. Examples of classical categories include boolean lattices and the category of sets and relations, where both conjunction and disjunction are modelled by the set-theoretic product. In this article, which is self-contained, we present an improved axiomatization of classical categories, together with a deep exploration of their structural theory. Observing that the collapse already happens in the absence of negation, we start with negation-free models called Dummett categories. Examples include, besides the classical categories above, the category of sets and relations, where both conjunction and disjunction are modelled by the di...

• Type: Journal
• Year: 2007
• Where: MSCS
• Authors: Carsten Führmann, David J. Pym
• Keywords: Classical Categories, Classical Sequent Calculus, Dummett Categories, MSCS 2007