[FOM] Paper announcement: Categorical Models of Classical Logic and GoI

[David Pym]

Readers of these lists may be interested to hear that the following paper
has appeared:

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

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