Base-extension Semantics for Modal Logic

In proof-theoretic semantics, meaning is based on inference. It may seen as the mathematical expression of the inferentialist interpretation of logic. Much recent work has focused on base-extension semantics, in which the validity of formulas is given by an inductive definition generated by provability in a `base' of atomic rules. Base-extension semantics for classical and intuitionistic propositional logic have been explored by several authors. In this paper, we develop base-extension semantics for the classical propositional modal systems K, KT , K4, and S4, with $\square$ as the primary modal operator. We establish appropriate soundness and completeness theorems and establish the duality between $\square$ and a natural presentation of $\lozenge$. We also show that our semantics is in its current form not complete with respect to euclidean modal logics. Our formulation makes essential use of relational structures on bases.