[PT] 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.