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

Sequent Calculus
Categorical
Contraction
Proof Nets
Boolean Lattice
Cut-elimination
Model
Intuitionistic Logic
Classical Logic
Soundness
Morphisms
Partial Order
Completeness
Formulation

Cite this

Order-enriched categorical models of the classical sequent calculus. / Fuhrmann, C; Pym, D.

In: Journal of Pure and Applied Algebra, Vol. 204, No. 1, 2006, p. 21-78.

Research output: Contribution to journalArticle

@article{30e2ec1a943f42b5a665a3b3864aedf5,
title = "Order-enriched categorical models of the classical sequent calculus",
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.",
author = "C Fuhrmann and D Pym",
note = "ID number: ISI:000233951800003",
year = "2006",
doi = "10.1016/j.jpaa.2005.03.016",
language = "English",
volume = "204",
pages = "21--78",
journal = "Journal of Pure and Applied Algebra",
issn = "0022-4049",
publisher = "Elsevier",
number = "1",

}

TY - JOUR

T1 - Order-enriched categorical models of the classical sequent calculus

AU - Fuhrmann, C

AU - Pym, D

N1 - ID number: ISI:000233951800003

PY - 2006

Y1 - 2006

N2 - 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.

AB - 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.

U2 - 10.1016/j.jpaa.2005.03.016

DO - 10.1016/j.jpaa.2005.03.016

M3 - Article

VL - 204

SP - 21

EP - 78

JO - Journal of Pure and Applied Algebra

JF - Journal of Pure and Applied Algebra

SN - 0022-4049

IS - 1

ER -