[Prev][Next][Index][Thread]
Paper announcement, semantics of classical proofs
Dear Colleagues,
The paper, "Order-enriched categorical models of the
classical sequent calculus", by Carsten Führmann and
David Pym, may be of interest to readers of the recipient
lists. It is available at
http://www.cs.bath.ac.uk/~pym/oecm.pdf
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.
Please accept out apologies for the size (11.5 Mb) of the pdf file: the
proof-net diagrams are rather complex.
Kind regards,
David Pym
--
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