arXiv · 2507.06834
Base-extension Semantics for Intuitionistic Modal Logics
Abstract
The proof theory and semantics of intuitionistic modal logics have been studied by Simpson in terms of Prawitz-style labelled natural deduction systems and Kripke models. An alternative to model-theoretic semantics is provided by proof-theoretic semantics, which is a logical realization of inferentialism, in which the meaning of constructs is understood through their use. The key idea in proof-theoretic semantics is that of a base of atomic rules, all of which refer only to propositional atoms and involve no logical connectives. A specific form of proof-theoretic semantics, known as base-extension semantics (B-eS), is concerned with the validity of formulae and provides a direct counterpart to Kripke models that is grounded in the provability of atomic formulae in a base. We establish, systematically, B-eS for Simpson's intuitionistic modal logics and, also systematically, obtain soundness and completeness theorems with respect to Simpson's natural deduction systems.
Explore related subjects
Keep this discovery
Explore connections, maps & timelines
Yll Buzoku, David. J. Pym. 2025-07-09. Base-extension Semantics for Intuitionistic Modal Logics. https://arxiv.org/abs/2507.06834
Cite the original work for its findings. Save a collection to share your selection of sources.