Paper Announcement: On the Geometry of Interaction for Classical Logic
The following may be of interest to readers of this list: Carsten F=FChrmann and David Pym, ''On the Geometry of Interaction for Classical Logic''. Abstract. It is well-known that weakening and contraction cause na=EFve 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=FChrmann and David Pym, "Order-enriched Categorical Models of the Classical Sequent Calculus". Abstract. It is well-known that weakening and contraction cause na=EFve 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 --=20 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@bath.ac.uk Bath BA2 7AY, England, U.K. Web: http://www.bath.ac.uk/~cssdjp
participants (1)
-
David J. Pym