一句话：确定一阶模态逻辑中插值式与定义存在性在若干片段上的可判定性与复杂度。
常域语义下，K 与 S5 之间的一阶模态逻辑即使限制为单个体变元也不具备 Craig 插值或投影 Beth 可定义性，故插值式/定义存在性不能归约为有效性。本文研究这些存在性问题的可判定性与复杂度：在 S5 的可判定片段 Q^1S5 及 S5 与带 universal role 的 ALC 结合片段 S5_ALC^u 中，插值式和定义存在性为 coN2ExpTime 可判定、2ExpTime-hard，uniform interpolant existence 不可判定，并迁移到无等词 FO^2；在 K 的一变量片段 Q^1K 中为非初等可判定，uniform interpolant existence 仍不可判定。
None of the first-order modal logics between $\mathsf{K}$ and $\mathsf{S5}$ under the constant domain semantics enjoys Craig interpolation or projective Beth definability, even in the language restricted to a single individual variable. It follows that the existence of a Craig interpolant for a given implication or of an explicit definition for a given predicate cannot be directly reduced to validity as in classical first-order and many other logics. Our concern here is the decidability and computational complexity of the interpolant and definition existence problems. We first consider two decidable fragments of first-order modal logic $\mathsf{S5}$: the one-variable fragment $\mathsf{Q^1S5}$ and its extension $\mathsf{S5}_{\mathcal{ALC}^u}$ that combines $\mathsf{S5}$ and the description logic$\mathcal{ALC}$ with the universal role. We prove that interpolant and definition existence in $\mathsf{Q^1S5}$ and $\mathsf{S5}_{\mathcal{ALC}^u}$ is decidable in coN2ExpTime, being 2ExpTime-hard, while uniform interpolant existence is undecidable. These results transfer to the two-variable fragment $\mathsf{FO^2}$ of classical first-order logic without equality. We also show that interpolant and definition existence in the one-variable fragment $\mathsf{Q^1K}$ of first-order modal logic $\mathsf{K}$ is non-elementary decidable, while uniform interpolant existence is again undecidable.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{KuruczWZ25,
title = {Deciding the Existence of Interpolants and Definitions in First-Order Modal Logic},
author = {Agi Kurucz and Frank Wolter and Michael Zakharyaschev},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 4},
year = {2025},
doi = {10.46298/lmcs-21(4:6)2025}
}