[FOM] Paper announcement: On the Geometry of Interaction for Classical Logic

David J. Pym d.j.pym at bath.ac.uk
Sat Nov 1 11:50:26 EST 2003


The following may be of interest to readers of this list:

Carsten Führmann and David Pym,
''On the Geometry of Interaction for Classical Logic''.

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 a previous paper, summarized herein, we provided 
sound and complete models that avoid this collapse by interpreting 
cut-reduction by a partial order between morphisms. In this article, we 
provide concrete examples of such models, based on geometry of 
interaction and data-flow. Our models provide detailed analyses of the 
relationships between negation, weakening, and contraction under 
cut-reduction.

Manuscript available at http://www.cs.bath.ac.uk/~pym/classical-GoI.pdf

We'd be very pleased to receive comments. This paper follows on from

Carsten Führmann and David Pym,
"Order-enriched Categorical Models of the Classical Sequent Calculus".

Abstract. It is well-known that weakening and contraction cause naïve 
categorical models of the classical sequent calculus to collapse to 
Boolean lattices. Starting from a convenient formulation of the 
well-known categorical semantics of linear classical sequent proofs, we 
give models of weakening and contraction that do not collapse. 
Cut-reduction is interpreted by a partial order between morphisms. Our 
models make no commitment to any translation of classical logic into 
intuitionistic logic and distinguish non-deterministic choices of 
cut-elimination. We show soundness and completeness via initial models 
built from proof nets, and describe models built from sets and relations.

This paper is in submission. Manscript available at 
http://www.cs.bath.ac.uk/~pym/oecm.pdf

Again, we'd be very pleased to receive comments.

Regards,

   David

-- 
Prof. David J. Pym                Telephone: +44 (0)1 225 38 3246
Professor of Logic & Computation  Facsimile: +44 (0)1 225 38 3493
University of Bath                Email: d.j.pym at bath.ac.uk
Bath BA2 7AY, England, U.K.       Web: http://www.bath.ac.uk/~cssdjp






More information about the FOM mailing list