[PT] GoI/Semantics of Classical Proofs

The draft below, now submitted to a journal, may be of interest to
readers of this list. It contains
a non-trivial categorical analysis of classical proofs and their theory
of cut-reduction, together
with a deep study of the structural theory,  and non-trivial examples.


On Categorical Models of  Classical Logic and the Geometry of Interaction,
Carsten F¸hrmann and David Pym.

http://www.cs.bath.ac.uk/~pym/dj.pdf  or
http://www.cs.bath.ac.uk/~pym/dj.ps
(Related papers at http://www.cs.bath.ac.uk/~pym/semclassproofs.html)

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