We prove that the constructive and intuitionistic variants of the modal logic $\mathsf{KB}$ coincide. This result contrasts with a recent result by Das and Marin, who showed that the constructive and intuitionistic variants of $\mathsf{K}$ do not prove the same diamond-free formulas.
翻译:我们证明了模态逻辑$\mathsf{KB}$的构造性变体与直觉主义变体是等价的。这一结果与Das和Marin最近的研究结论形成了对比,他们证明了$\mathsf{K}$的构造性变体与直觉主义变体在菱形算子自由的公式上并不具有相同的可证性。