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.