Re: GoI/Semantics of Classical Proofs

Apologies: related papers are actually at

http://www.cs.bath.ac.uk/~pym/semclasspro.html


David J. Pym wrote:

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