团簇展开与 boxdot 猜想

boxdot 猜想断言，每一个通过著名的 boxdot 翻译忠实解释 T 的正规模态逻辑，实际上都包含于 T 中。我们证实该猜想是正确的。更一般地，我们提出了一个关于模态逻辑 $L_0$ 的简单语义条件，该条件确保通过 boxdot 翻译忠实嵌入 $L_0$ 的最大逻辑就是 $L_0$ 本身。特别地，这一 boxdot 猜想的自然推广对于用 S4、S5 和 KTB 替代 T 的情形也成立。