Order-enriched categorical models of the classical sequent calculus
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.
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.
|Creators||Fuhrmann, C.and Pym, D.|
|Departments||Faculty of Science > Computer Science|
|Additional Information||ID number: ISI:000233951800003|
Actions (login required)