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.

Abstract This work is the first exploration of proof-theoretic semantics for a substructural logic. It focuses on the base-extension semantics (B-eS) for intuitionistic multiplicative linear logic ( $$\mathrm IMLL$$ ). The starting point is a review of Sandqvist’s B-eS for intuitionistic propositional logic (IPL), for which we propose an alternative treatment of conjunction that takes the form of thegeneralizedelimination rule for the connective. The resulting semantics is shown to be sound and complete. This motivates our main contribution, a B-eS for $$\mathrm IMLL$$ , in which the definitions of the logical constants all take the form of their elimination rule and for which soundness and completeness are established.

Abstract The logic of Bunched Implications (BI) freely combines additive and multiplicative connectives, including implications; however, despite its well-studied proof theory, proof-search in BI has always been a difficult problem. The focusing principle is a restriction of the proof-search space that can capture various goal-directed proof-search procedures. In this paper we show that focused proof-search is complete for BI by first reformulating the traditional bunched sequent calculus using the simpler data-structure of nested sequents, following with a polarised and focused variant that we show is sound and complete via a cut-elimination argument. This establishes an operational semantics for focused proof-search in the logic of Bunched Implications.