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.