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

Classical Logic
Categorical
Boolean algebra
Geometry
Interaction
Boolean Lattice
Acoustic waves
Model
Contraction
Cut-elimination
Sequent Calculus
Linear Logic
Semilattice
Axiomatization
Partial Order
Poset
Multiplicative
Disjoint
Union

Cite this

On categorical models of classical logic and the Geometry of Interaction. / Fuhrmann, C; Pym, D.

In: Mathematical Structures in Computer Science, Vol. 17, No. 5, 2007, p. 957-1027.

Research output: Contribution to journalArticle

@article{4810e879496447859a0f84ac7807ec84,
title = "On categorical models of classical logic and the Geometry of Interaction",
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.",
author = "C Fuhrmann and D Pym",
note = "ID number: ISI:000251864200003",
year = "2007",
doi = "10.1017/s0960129507006287",
language = "English",
volume = "17",
pages = "957--1027",
journal = "Mathematical Structures in Computer Science",
issn = "0960-1295",
publisher = "Cambridge University Press",
number = "5",

}

TY - JOUR

T1 - On categorical models of classical logic and the Geometry of Interaction

AU - Fuhrmann, C

AU - Pym, D

N1 - ID number: ISI:000251864200003

PY - 2007

Y1 - 2007

N2 - 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.

AB - 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.

U2 - 10.1017/s0960129507006287

DO - 10.1017/s0960129507006287

M3 - Article

VL - 17

SP - 957

EP - 1027

JO - Mathematical Structures in Computer Science

JF - Mathematical Structures in Computer Science

SN - 0960-1295

IS - 5

ER -