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 Coq Proof Assistant.

翻译：在构造性K（CK）与直觉主义K（IK）之间考察的直觉主义模态逻辑，在其对可能性（菱形）联结词的处理上存在差异。近期研究发现，某些介于CK与IK之间的逻辑在其无菱形片段上也存在分歧，其中仅部分逻辑对仅含必然性（方框）的直觉主义模态逻辑标准公理化系统保持保守性。我们证明，CK的关系克里普克语义可通过添加框架条件进行扩展，这些条件覆盖IK标准公理化中的所有公理以及先前研究过的其他公理。这使我们能够回答关于此类逻辑相对于无菱形直觉主义模态逻辑的（非）保守性的开放问题。本研究结果已通过Coq证明辅助工具进行形式化验证。