A generalised and modular proof-theoretic semantics for sequent systems
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.
Related
- Modular Properties of W3 Generalised Gibbs Ensembles
- The parameterised complexity of generalised temporal domination on temporal graphs with modular structure
- Modular Properties of Generalised Gibbs Ensembles: The Deformed KdV Hierarchy
- K-theoretic invariants of four three-dimensional operator systems
- K-theoretic invariants of the Toeplitz operator system and its dual, and of all graph operator systems
BibTeX
@misc{barrosonascimento2026generalised,
title = {{A generalised and modular proof-theoretic semantics for sequent systems}},
author = {Victor Barroso-Nascimento and Arghya Chakrabarty and Elaine Pimentel},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.23822},
eprint = {2610.23822},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.23822},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - A generalised and modular proof-theoretic semantics for sequent systems
AU - Victor Barroso-Nascimento
AU - Arghya Chakrabarty
AU - Elaine Pimentel
PY - 2026
DA - 2026/10/16
PB - arXiv
DO - 10.48550/arxiv.2610.23822
UR - https://arxiv.org/abs/2610.23822
AB - 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.
ER -