A non-uniform view of Craig interpolation in modal logics with linear frames

技术摘要：关于线性框架下模态逻辑中克雷格插值（Craig Interpolation）的非一致性视角

问题陈述
克雷格插值属性（CIP）是逻辑学中的一个基本属性，它指出对于任何有效的蕴含式 $\phi \to \psi$，都存在一个仅使用 $\phi$ 与 $\psi$ 共享词汇的插值式 $\iota$，使得 $\phi \to \iota$ 且 $\iota \to \psi$ 同样有效。在许多扩展了 K4.3（线性传递框架的逻辑）的正则模态逻辑中，缺乏 CIP 已成为一个公认的“否定性”事实，特别是对于那些具有无界深度的逻辑。传统上，CIP 的缺失意味着对给定逻辑的插值式研究的终止。

本文通过研究插值式存在问题（IEP），将 CIP 的缺失重新定义为一个研究课题：给定两个公式 $\phi$ 和 $\psi$，若 $\phi \to \psi$ 在某种逻辑 $L$ 中有效，那么是否存在 $L$ 中的克雷格插值式？与一致性的 CIP 不同，IEP 并不简单地还原为有效性检查，因为蕴含式的有效性并不保证插值式的存在。本文探讨的核心问题是：IEP 在这些逻辑中的计算复杂度是否比有效性问题（蕴含问题）更高。以往在其他逻辑（例如带有标名的模态逻辑、一阶逻辑的分片）中的研究结果表明，IEP 可能显著更难（例如 3ExpTime）。本文调查了对于包含 K4.3 的命题模态逻辑，是否也存在这种情况。

方法论
作者采用了一种基于**双模拟（bisimulations）和描述性框架（descriptive frames）**的非一致、模型论方法。

1. 双模拟特征化： 本文利用了一个已知的判别准则（定理 3.2）：$\phi \to \psi$ 在 $L$ 中缺乏插值式，当且仅当存在两个基于 $L$ 的描述性框架的模型 $M_1$ 和 $M_2$，使得 $M_1$ 满足 $\phi$，$M_2$ 满足 $\neg\psi$，且这两个模型的根点是 $\sigma$-双模拟的（其中 $\sigma$ 是共享签名）。
2. 描述性框架： 分析高度依赖于描述性框架的结构（配备了满足微分性、紧密性和紧凑性条件的特定内部集合代数的框架）。这至关重要，因为对于像 GL.3 和 Log{(N, <)} 这样的逻辑，反例无法通过标准的 Kripke 框架来体现，而必须需要无限的描述性框架。
3. 结构分解： 核心技术创新在于分析这些双模拟模型的结构。作者将模型划分为 $\sigma$-块（具有特定双模拟性质的点区间），并证明任何见证插值式缺失的双模拟模型对都可以转化为一对“拟有限（quasi-finite）”模型。这些模型是通过基于特定原子框架（有限链、有限簇或如 $C(\bigcirc_k, \bullet)$ 的“蝌蚪型”结构）的简单模型的有序和构造而成的。
4. 拟多项式规模属性： 对于有限可公理化的逻辑，作者证明了这些见证模型的大小可以由输入公式的大小和逻辑公理的大小的多项式进行界定。这被称为拟多项式规模双模拟模型属性。

主要贡献与结果

• 可判定性与复杂度： 本文证明了对于所有包含 K4.3 的有限可公理化正则模态逻辑，IEP 是可判定的且属于 coNP-完全类。

  • 这一结果具有重要意义，因为它表明 IEP 并不比有效性问题（该类逻辑的有效性问题同样属于 coNP）更难。这与近期在其他逻辑框架中观察到的非一致插值结果形成了鲜明对比，后者显示 IEP 往往严格更难。
  • 证明过程涉及一个非确定性算法，该算法猜测满足双模拟准则的多项式规模模型，并验证逻辑公理。

• 拟多项式规模双模拟模型属性： 作者确立了所有包含 K4.3 的有限可公理化扩展都具有“拟多项式规模双模拟模型属性”。这意味着，如果插值式不存在，则存在一对见证这一事实的双模拟模型，其中模型是基于多项式数量的简单模型以及多项式大小的原子框架构成的有序和。

  • 对于 d-持久共尾子框架逻辑（一类子类），该属性更强：它们具有多项式规模双模拟模型属性，即模型是多项式规模的标准 Kripke 框架。

• 向普里奥尔（Priorean）时间逻辑的扩展： 该方法被扩展到了在标准时间流（同时包含未来和过去模态）上的普里奥尔时间逻辑：

  • Lin（所有线性框架）、LinQ（有理数）和 LinR（实数）：这些逻辑被证明具有多项式规模双模拟模型属性，且其 IEP 为 coNP-完全。
  • Lin<ω（有限严格线性序）和 LinZ（整数）：这些逻辑不具备多项式规模属性，但具有拟多项式规模双模拟模型属性。其 IEP 也被证明是 coNP-完全的。
  • 针对时间逻辑的证明需要处理双向链和两端的极限簇，因此需要新的框架构造（例如对称的“蝌蚪型”框架 $C(\bullet, \bigcirc_k, \bullet)$）。

意义与主张
本文声称提供了第一个涵盖大规模逻辑族（K4.3 的扩展）的关于克雷格插值式存在性的通用结果，这些逻辑本身并不具备 CIP。通过证明 IEP 对于这些逻辑是 coNP-完全的，作者挑战了以下直觉：即 CIP 的缺失必然会导致存在问题的复杂度等级更高。

这项工作表明，IEP 的复杂度本质上并不取决于 CIP 的失效，而是取决于见证失效所需的模型的结构属性。作者将此定位为根据 IEP 复杂度对模态逻辑进行分类的一步。

论文明确指出，其证明关于计算插值式本身是非构造性的；它提供了一个关于存在性的判定程序，但并未产生高效计算插值式本身或其大小上界的算法。作者还强调，描述性框架对于其证明是必不可少的，这提出了一个开放性问题：对于不是 d-持久但具有强 Kripke 完全性的逻辑（如 LinR），Kripke 框架是否足以处理 IEP 问题。