A generalised and modular proof-theoretic semantics for sequent systems

Overview & Synopsis

Base-extension semantics explains logical consequence via derivability in atomic systems. Extending this approach across logics requires careful control of structural principles and contexts. We present a modular sequent-based framework in which support is indexed by multisets of atomic resources and the semantic clauses for connectives are guided by their left introduction rules. The framework separates additive from multiplicative behaviour and makes explicit the contributions of structural rules and restrictions on sequents. We establish soundness and completeness for classical and intuitionistic propositional logic and for multiplicative-additive fragments of classical and intuitionistic linear logic. We then investigate axiomatic extensions of intuitionistic logic through Jankov logic. Two classes of atomic bases yield sound and complete semantics. Completeness is proven using two novel and modular methods using simulation bases, one of which is constructive. These results provide a common semantic treatment of several logical systems while identifying the additional conditions needed to extend the framework beyond structural variations.