一阶模态逻辑中插值符与定义存在性的判定
计算机科学中的逻辑
2025-10-15 v4
摘要
在常域语义下，介于K与S5之间的一阶模态逻辑，即便在限制为单个个体变量的语言中，也不具备Craig插值或投射Beth可定义性。由此可知，对于给定的蕴涵式给出Craig插值符、或对于给定的谓词给出显式定义，不能像经典一阶逻辑及许多其他逻辑那样直接归约为有效性。我们此处关注的是插值符与定义存在性问题的可判定性与计算复杂性。我们首先考虑一阶模态逻辑S5的两个可判定片段：单变量片段Q^1S5及其扩展S5_{ALC^u}（该扩展将S5与具有全角色的描述逻辑ALC相结合）。我们证明Q^1S5和S5_{ALC^u}中的插值符与定义存在性可在coN2ExpTime内判定，且为2ExpTime困难，而一致插值符存在性不可判定。这些结果转移到无等词的经典一阶逻辑双变量片段FO^2。我们还证明一阶模态逻辑K的单变量片段Q^1K中的插值符与定义存在性是非初等可判定的，而一致插值符存在性同样不可判定。
引用
@article{arxiv.2303.04598,
title = {Deciding the Existence of Interpolants and Definitions in First-Order Modal Logic},
author = {Agi Kurucz and Frank Wolter and Michael Zakharyaschev},
journal= {arXiv preprint arXiv:2303.04598},
year = {2025}
}