Gheorghiu, Alexander V; Pym, David J; (2023) Defining Logical Systems via Algebraic Constraints on Proofs. Journal of Logic and Computation , Article exad065. 10.1093/logcom/exad065. (In press).

Preview

Text Pym_exad065.pdf Download (4MB) | Preview

Abstract

We present a comprehensive programme analysing the decomposition of proof systems for non-classical logics into proof systems for other logics, especially classical logic, using an algebra of constraints. That is, one recovers a proof system for a target logic by enriching a proof system for another, typically simpler, logic with an algebra of constraints that act as correctness conditions on the latter to capture the former; e.g. one may use Boolean algebra to give constraints in a sequent calculus for classical propositional logic to produce a sequent calculus for intuitionistic propositional logic. The idea behind such forms of decomposition is to obtain a tool for uniform and modular treatment of proof theory and to provide a bridge between semantics logics and their proof theory. The paper discusses the theoretical background of the project and provides several illustrations of its work in the field of intuitionistic and modal logics: including, a uniform treatment of modular and cut-free proof systems for a large class of propositional logics; a general criterion for a novel approach to soundness and completeness of a logic with respect to a model-theoretic semantics; and a case study deriving a model-theoretic semantics from a proof-theoretic specification of a logic.

Download activity - last month

Export as JSONCSVXML

Download activity - last 12 months

Export as XMLCSVJSON

Downloads by country - last 12 months

Export as JSONXMLCSV

Archive Staff Only

View Item