[FOM] Paper announcement: Categorical Models of Classical Logic and GoI
d.j.pym at bath.ac.uk
Tue Nov 6 05:49:54 EST 2007
Readers of these lists may be interested to hear that the following paper
C. Führmann and D. Pym. On categorical models of classical logic and the
geometry of interaction.
Mathematical Structures in Computer Science 17(5), 2007, 957-1027.
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 Dummett 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
Prof. David J. Pym t: +44 (0) 117 312 8012
Principal Scientist f: +44 (0) 117 312 9250
HP Labs e: david.pym at hp.com
Bristol, UK w: http://www.hpl.hp.com/personal/davpym/
Professor of Logic & Computation, University of Bath, UK
Hewlett-Packard Limited Registered Office: Cain Road, Bracknell, Berks
RG12 1HN. Registered No: 690597 England.
The contents of this message, its subsequent correspondence, and any
attachments to it are confidential and may be legally privileged. If
you have received this message in error, you should delete it from
your system immediately and advise the sender.
Do not send, forward, or (b)cc replies to additional recipients
without my explicit consent.
To any recipient of this message within HP, unless otherwise stated you
should consider this message and attachments as "HP CONFIDENTIAL".
More information about the FOM