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.
Keywords
Cite
@article{arxiv.2507.06834,
title = {Base-extension Semantics for Intuitionistic Modal Logics},
author = {Yll Buzoku and David. J. Pym},
journal= {arXiv preprint arXiv:2507.06834},
year = {2025}
}
Comments
21 pages