Order-enriched categorical models of the classical sequent calculus

12Citations
Citations of this article
9Readers
Mendeley users who have this article in their library.

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. © 2005 Elsevier B.V. All rights reserved.

Cite

CITATION STYLE

APA

Führmann, C., & Pym, D. (2006). Order-enriched categorical models of the classical sequent calculus. Journal of Pure and Applied Algebra, 204(1), 21–78. https://doi.org/10.1016/j.jpaa.2005.03.016

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free