From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/2331 Path: news.gmane.org!not-for-mail From: "David J. Pym" Newsgroups: gmane.science.mathematics.categories Subject: Preprint: semantics of classical proofs Date: Thu, 05 Jun 2003 08:37:44 +0100 Message-ID: <3EDEF348.4010107__17943.086094647$1241018586$gmane$org@bath.ac.uk> NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=3DISO-8859-1; format=3Dflowed Content-Transfer-Encoding: 8bit X-Trace: ger.gmane.org 1241018585 3630 80.91.229.2 (29 Apr 2009 15:23:05 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:23:05 +0000 (UTC) To: categories@mta.ca, types@cis.upenn.edu Original-X-From: rrosebru@mta.ca Thu Jun 5 16:28:15 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 05 Jun 2003 16:28:15 -0300 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19O0M7-00017i-00 for categories-list@mta.ca; Thu, 05 Jun 2003 16:24:59 -0300 Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 22 Original-Lines: 38 Xref: news.gmane.org gmane.science.mathematics.categories:2331 Archived-At: Dear Colleagues, The paper, "Order-enriched categorical models of the classical sequent calculus", by Carsten F=FChrmann and David Pym, may be of interest to readers of the recipient lists. It is available at =09http://www.cs.bath.ac.uk/~pym/oecm.pdf 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. Please accept out apologies for the size (11.5 Mb) of the pdf file: the proof-net diagrams are rather complex. Kind regards, =09David Pym --=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