二阶命题模态逻辑的 Sahlqvist 对应理论
计算机科学中的逻辑
2021-10-19 v1
摘要
带命题量词的模态逻辑（即二阶命题模态逻辑（SOPML））自模态逻辑早期就已被研究。其表达力和复杂度都很高，其 van-Benthem-Rosen 定理和 Goldblatt-Thomason 定理已由 ten Cate（2006）证明。然而，SOPML 的 Sahlqvist 理论在文献中尚未被考虑。在本文中，我们填补了这一空白。我们发展了 SOPML 的 Sahlqvist 对应理论，其涵盖并恰当地扩展了基本模态逻辑中已有的 Sahlqvist 公式。我们以分层方式逐步定义 SOMPL 的 Sahlqvist 公式类，其中每个公式都被证明在 Kripke 框架上有一个可由算法 有效计算的一阶对应物。此外，我们表明某些 -规则对应于 SOMPL 中的 -Sahlqvist 公式，其进一步对应于一阶条件，并且即使对于非常简单的 SOMPL Sahlqvist 公式，它们也可能已经是非典范的。
引用
@article{arxiv.2110.08561,
title = {Sahlqvist Correspondence Theory for Second-Order Propositional Modal Logic},
author = {Zhiguang Zhao},
journal= {arXiv preprint arXiv:2110.08561},
year = {2021}
}