Research

Order-enriched categorical models of the classical sequent calculus


Reference:

Fuhrmann, C. and Pym, D., 2006. Order-enriched categorical models of the classical sequent calculus. Journal of Pure and Applied Algebra, 204 (1), pp. 21-78.

Related documents:

This repository does not currently have the full-text of this item.
You may be able to access a copy if URLs are provided below.

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.

Details

Item Type Articles
CreatorsFuhrmann, C.and Pym, D.
DOI10.1016/j.jpaa.2005.03.016
DepartmentsFaculty of Science > Computer Science
RefereedYes
StatusPublished
ID Code5349
Additional InformationID number: ISI:000233951800003

Export

Actions (login required)

View Item