Order-enriched categorical models of the classical sequent calculus

C Fuhrmann, D Pym

Research output: Contribution to journalArticle

12 Citations (Scopus)

Abstract

It is well-known that weakening and contraction cause naive 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. (c) 2005 Elsevier B.V. All rights reserved.
Original languageEnglish
Pages (from-to)21-78
Number of pages58
JournalJournal of Pure and Applied Algebra
Volume204
Issue number1
DOIs
Publication statusPublished - 2006

Fingerprint Dive into the research topics of 'Order-enriched categorical models of the classical sequent calculus'. Together they form a unique fingerprint.

Cite this