On categorical models of classical logic and the Geometry of Interaction

C Fuhrmann, D Pym

Research output: Contribution to journalArticle

7 Citations (Scopus)

Abstract

It is well known that weakening and contraction cause naive categorical models of the classical sequent calculus to collapse to Boolean lattices. In previous work, summarised briefly herein, we have provided a class of models called classical categories that 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 axiomatisation 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 of these include, besides the classical categories mentioned above, the category of sets and relations, where both conjunction and disjunction are modelled by the disjoint union. We prove that Durnmett categories are MIX, and that the partial order can be derived from hom-semilattices, which have a straightforward proof-theoretic definition. Moreover, we show that the Geometry-of-Interaction construction can be extended from multiplicative linear logic to classical logic by applying it to obtain a classical category from a Dummett category. Along the way, we gain detailed insights into the changes that proofs undergo during cut elimination in the presence of weakening and contraction.
Original languageEnglish
Pages (from-to)957-1027
Number of pages71
JournalMathematical Structures in Computer Science
Volume17
Issue number5
DOIs
Publication statusPublished - 2007

Fingerprint Dive into the research topics of 'On categorical models of classical logic and the Geometry of Interaction'. Together they form a unique fingerprint.

  • Cite this