Modular approach clarifies logic systems with sequent proofs
A generalised and modular proof-theoretic semantics for sequent systems
Logic in Computer Science
Summary
Logic helps us decide what conclusions follow from given statements, but different logics have diverse rules that make understanding them tricky. The authors created a way to break down and organize these logic systems using a simple kind of proof structure called sequents. Their method clearly separates different parts of the logic and tracks how rules combine, making it easier to see how various logics relate and work. They showed this method works well for common logical systems and some more complex ones, helping unify how we understand logical reasoning.
What this means in practice
- •For programming language designers: Design and verify type systems by using the modular framework to model complex logical rules clearly and ensure sound reasoning.
- •For formal verification engineers: Implement precise verification tools for software correctness that integrate multiple logics using the modular sequent-based semantics framework.
A theory result. No direct application yet.
Authors
Victor Barroso-Nascimento, Arghya Chakrabarty, Elaine Pimentel
Abstract
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.