Defining Logical Systems via Algebraic Constraints on Proofs

TL;DR

This paper introduces a unified algebraic framework for decomposing and constructing proof systems for non-classical logics, enabling modular, sound, and complete proof-theoretic and semantic analysis.

Contribution

It develops a general algebraic approach to derive proof systems for various logics from simpler ones, enhancing modularity and semantic correspondence.

Findings

Uniform treatment of propositional logics proof systems

A criterion for soundness and completeness via algebraic constraints

Derivation of model-theoretic semantics from proof systems

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; for example, 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 reduction is to obtain a tool for uniform and modular treatment of proof theory and provide a bridge between semantics logics and their proof theory. The article discusses the theoretical background of the project and provides several illustrations of its work in the field of intuitionistic and modal logics. The results include the following: 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.