Preprint: semantics of classical proofs

Preprint: semantics of classical proofs

[David J. Pym]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain; charset=3DISO-8859-1; format=3Dflowed, Size: 1360 bytes --]

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