一句话：为 CK 与 IK 之间的直觉主义模态逻辑给出 Kripke 语义与框架条件，解答其相对无 diamond 逻辑的保守性问题。
本文研究 Constructive K (CK) 与 Intuitionistic K (IK) 之间的直觉主义模态逻辑。这些逻辑对可能性（diamond）联结词的处理不同，近期发现其中部分逻辑在无 diamond 片段上也不一致，只有部分逻辑对仅含必然性（box）的标准直觉主义模态逻辑公理化保持保守。作者将 CK 的关系 Kripke 语义扩展，为 IK 标准公理化及此前研究的其他公理给出对应框架条件，从而回答这些逻辑关于无 diamond 直觉主义模态逻辑的（非）保守性开放问题。所有结果均在 Rocq Prover 中形式化验证。
The intuitionistic modal logics considered between Constructive K (CK) and Intuitionistic K (IK) differ in their treatment of the possibility (diamond) connective. It was recently rediscovered that some logics between CK and IK also disagree on their diamond-free fragments, with only some remaining conservative over the standard axiomatisation of intuitionistic modal logic with necessity (box) alone. We show that relational Kripke semantics for CK can be extended with frame conditions for all axioms in the standard axiomatisation of IK, as well as other axioms previously studied. This allows us to answer open questions about the (non-)conservativity of such logics over intuitionistic modal logic without diamond. Our results are formalised using the Rocq Prover.
DOI 原文 ·
@inproceedings{paperbot8667,
title = {Semantical Analysis of Intuitionistic Modal Logics between CK and IK},
author = {Jim De Groot and Ian Shillito and Ranald Clouston},
booktitle = {LICS},
year = {2025},
doi = {10.1109/lics65433.2025.00020}
}