Order-enriched categorical models of the classical sequent calculus |
| |
Authors: | Carsten Führmann |
| |
Institution: | University of Bath, England, UK |
| |
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. |
| |
Keywords: | 03B05 03F03 03G30 03F05 03G05 03F52 |
本文献已被 ScienceDirect 等数据库收录! |