Sciweavers

Share
MSCS
2007

On categorical models of classical logic and the Geometry of Interaction

8 years 10 months ago
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...
Carsten Führmann, David J. Pym
Added 27 Dec 2010
Updated 27 Dec 2010
Type Journal
Year 2007
Where MSCS
Authors Carsten Führmann, David J. Pym
Comments (0)
books