论文标题
与交集的模态逻辑的简单完整性证明
Simpler completeness proofs for modal logics with intersection
论文作者
论文摘要
人们对扩展各种模态逻辑与交集有很大的兴趣，最突出的例子是具有分布式知识的认识和毒逻辑。此类逻辑的完整性证明往往很复杂，尤其是在标准认知逻辑中的S5等模型类中，这主要是由于标准模态逻辑中模态交集的不确定性。 [8]中概述了S5情况的标准证明方法，然后在[13]中更详细地进行了详细阐述，使用“解开折叠方法”案例，以实现Treelike模型来处理不确定性的问题。但是，由于细节和对S5的依赖水平，此方法不容易适应其他逻辑。在本文中，我们通过直接构建Treelike规范模型来提出一种更简单的证明技术，从而避免了拆卸和折叠过程中的并发症。我们通过显示正常模态逻辑K，D，T，B，S4和S5的完整性来证明技术。此外，这些Treelike典型模型与Fischer-Ladner风格的封闭兼容，我们结合了显示上述逻辑的完整性的方法，进一步扩展了PDL或认知逻辑已知的联合模态的延伸。其中一些完整的结果是新的。
There has been a significant interest in extending various modal logics with intersection, the most prominent examples being epistemic and doxastic logics with distributed knowledge. Completeness proofs for such logics tend to be complicated, in particular on model classes such as S5 like in standard epistemic logic, mainly due to the undefinability of intersection of modalities in standard modal logics. A standard proof method for the S5 case was outlined in [8] and later explicated in more detail in [13], using an "unraveling-folding method" case to achieve a treelike model to deal with the problem of undefinability. This method, however, is not easily adapted to other logics, due to the level of detail and reliance on S5. In this paper we propose a simpler proof technique by building a treelike canonical model directly, which avoids the complications in the processes of unraveling and folding. We demonstrate the technique by showing completeness of the normal modal logics K, D, T, B, S4 and S5 extended with intersection modalities. Furthermore, these treelike canonical models are compatible with Fischer-Ladner-style closures, and we combine the methods to show the completeness of the mentioned logics further extended with transitive closure of union modalities known from PDL or epistemic logic. Some of these completeness results are new.
