标题： 直觉主义模态逻辑的基域扩展语义学 显示英文标题

标题： Base-extension Semantics for Intuitionistic Modal Logics

摘要： 直觉主义模态逻辑的证明论和语义学由辛普森通过Prawitz风格的标记自然演绎系统和克里普克模型进行研究。 模型论语义学的一种替代方法是证明论语义学，这是一种推理主义的逻辑实现，在这种实现中，构造的意义是通过其使用来理解的。 证明论语义学的关键思想是原子规则的基，所有这些规则仅涉及命题原子，且不涉及任何逻辑连接词。 一种特定形式的证明论语义学，称为基扩展语义学（B-eS），关注公式的有效性，并提供了一个与克里普克模型直接对应的语义学，该语义学以基中原子公式的可证性为基础。 我们系统地建立了辛普森的直觉主义模态逻辑的B-eS，并且系统地获得了相对于辛普森自然演绎系统的可靠性和完全性定理。 显示英文摘要

摘要： 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.