Defining Logical Systems via Algebraic Constraints on Proofs

We provide a comprehensive presentation of a program of uniform decomposition of proof systems for non-classical logics into other logics, especially classical logic, by means of an algebra of constraints. That is, one recovers a proof system for a target logic by enriching a proof system for a simpler logic with an algebra of constraints that act as correctness conditions on the latter to capture the former; for example, one may use Boolean constraints in the consequent in a sequent calculus for classical logic to produce a sequent calculus for intuitionistic logic. The idea behind such forms of reduction it to obtain a tool for uniform and modular treatment of proof theory, and provide a bridge between semantics of more complex logics and their proof theory. The article discusses the theoretic background of the project and provides several illustrations of its work in the field of intuitionistic and modal logics. Some results include 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.