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


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