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.

翻译：在证明论语义学中，意义基于推理。这可以视为逻辑推理主义解释的数学表达。近期大量工作聚焦于基扩展语义学，其中公式的有效性由原子规则"基"中的可证性生成的归纳定义给出。多位学者已探索了经典和直觉主义命题逻辑的基扩展语义学。本文针对以$\square$为主要模态算子的经典命题模态系统K、KT、K4和S4，发展了基扩展语义学。我们建立了相应的可靠性和完全性定理，并确立了$\square$与$\lozenge$自然表述之间的对偶性。同时证明，该语义学目前形式对于欧几里得模态逻辑不具完全性。我们的表述本质性地运用了基上的关系结构。