🔢 mathematics

Propositional Dynamic Logic has Craig Interpolation: a tableau-based proof

本文通过采用一种带有加载机制的循环表式系统（cyclic tableau system）以及一种用于计算插值式的改进型 Maehara 方法，为命题动态逻辑（PDL）具有克雷格插值性质（Craig Interpolation Property）提供了构造性证明，从而在之前的尝试被撤回或受到批评之后，解决了这一长期存在的开放问题。

原作者： Manfred Borzechowski, Malvin Gattinger, Helle Hvid Hansen, Revantha Ramanayake, Francisco Trucco Dalmas, Yde Venema

发布于 2026-08-12

📖 1 分钟阅读🧠 深度阅读

CC BY 4.0

原作者： Manfred Borzechowski, Malvin Gattinger, Helle Hvid Hansen, Revantha Ramanayake, Francisco Trucco Dalmas, Yde Venema

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下你是一名试图破解谜团的侦探，但你只能使用一组特定的线索。你有一份来自一名证人（我们称之为“控诉者”）的长篇且复杂的报告，以及另一份来自另一名证人（“辩护者”）的反驳报告。你的任务是找到一个简短的句子，来解释他们之间的冲突。这个句子必须是“中间地带”：如果控诉者是对的，这个句子必须为真；如果辩护者是对的，这个句子必须为假。至关重要的是，这个句子只能使用同时出现在两份报告中的单词。如果控诉者谈论“猫”和“老鼠”，而辩护者谈论“狗”和“骨头”，那么你的中间句子不能提到“猫”或“骨头”；它只能使用像“动物”或“追逐”这样在两个故事中都出现的单词。在计算机科学领域，这个侦探游戏被称为克雷格插值属性（Craig Interpolation Property）。这是一种超级力量，能帮助计算机理解系统的不同部分是如何相互关联的，而不会被无关细节所困扰。

这个特定的侦探游戏处理的是命题动态逻辑（Propositional Dynamic Logic，简称 PDL）。把 PDL 想象成一种描述计算机程序行为的语言。它就像是一个视频游戏的规则手册，规定了诸如“如果你按下‘A’，那么‘B’，你就会跳跃”或者“如果你持续按下‘X’，你最终会飞行”之类的内容。棘手的部分在于“最终”或“持续做这件事直到永远”的部分，这使得这种逻辑变得非常强大，但也非常难以解决。几十年来，数学家和计算机科学家一直试图证明这种特定的规则手册（PDL）是否拥有插值这一超级力量。过去有三个不同的团队尝试解决这个谜题，但他们的解决方案被发现存在漏洞，使得这个问题悬而未决并令人沮丧。

这篇论文终于解开了这个谜团。作者们——一个来自德国和荷兰的研究小组——构建了一个全新的、严谨的证明，证明了命题动态逻辑确实具有克雷格插值属性。他们不仅仅是在猜测；他们构建了一个名为“循环表过程系统（cyclic tableau system）”的特定工具。想象一下这个系统是一个巨大的、分支的树状结构，你试图将一个复杂的逻辑谜题分解成越来越小的碎片。通常，这些树会无限生长，但作者添加了一个特殊的“加载机制”，它起到了安全网的作用。如果这棵树开始循环回到自身（这发生在程序重复动作时），该机制会识别出这个循环并停止生长，从而确保证明过程保持有限且可控。

利用这个新的树状构建工具，作者展示了对于 PDL 中的任何有效的逻辑语句，你总能找到那个完美的“中间句子”（即插值项），它使用双方共有的词汇来连接论证的两侧。他们不仅证明了它的存在，还展示了如何精确地计算它。他们甚至用一种名为 Haskell 的编程语言写了一个程序，可以为你进行这种计算；目前，他们正在编写第二个证明层，利用一个名为“Lean”的数字助手来验证他们的数学推导是否 100% 正确。虽然他们解决了主要谜题，但他们承认一些较小的相关问题——例如，在不含“测试（test）”命令的简化版本逻辑中是否仍然适用——仍留给未来的侦探们去解决。但就目前而言，大问题已经有了答案：PDL 拥有插值的超级力量，而且我们现在确切知道如何使用它。

技术摘要：命题动态逻辑具有克雷格插值性质

1. 问题描述

本文解决了关于命题动态逻辑（PDL）是否具有克雷格插值性质（Craig Interpolation Property, CIP）这一长期悬而未决的问题。CIP 指的是：对于任何有效的蕴含式 $\phi \to \psi$ ，存在一个插值式 $\theta$ ，使得 $\phi \to \theta$ 和 $\theta \to \psi$ 均有效，且 $\theta$ 仅包含 $\phi$ 与 $\psi$ 共有的命题字母和原子程序。

尽管 PDL 作为一种研究深入、具有成熟判定性和完备性结果的模态逻辑，其插值状态在过去几十年中一直不明朗。文献中存在三次关于证明插值的尝试：

Leivant (1981)： 声称给出了证明，后被 Kracht (1999) 指出其理由错误，尽管 Leivant 的证明中确实存在实质性的漏洞。
Borzechowski (1988)： 一篇声称证明了插值的硕士论文（Diplomarbeit），该文受到的关注较少，并被一些人认为难以验证。
Kowalski (2002)： 声称给出了证明，但该证明被驳回并在 2004 年正式撤回。

难点在于 PDL 是一种模态不动点逻辑（由于迭代算子 $*$ 的存在）。虽然插值性质已在通过循环证明系统实现的完整模态 $\mu$ -演算及其无交替片段中得到确立，但 PDL 特有的约束使得确保表征插值式的不动点方程解能够表达在 PDL 自身内部（而非需要完整的 $\mu$ -演算表达能力）变得极具挑战性。

2. 方法论

作者基于一个循环表（cyclic tableau）系统以及对 Maehara 证明论方法的改进，提供了一个构造性证明。

2.1. PDL 的循环表系统

作者定义了一个作用于分裂序列（split sequents，即公式对）的新 PDL 表系统。其核心特征包括：

局部与模态推理： 该系统区分了局部规则（单个状态内的命题推理和程序的展开）与模态规则（在 Kripke 模型中跨越状态）。
展开机制： 系统并未针对每个程序构造器使用标准的归约规则，而是使用了一种“加载”（loading）机制。形式为 $[\alpha]\psi$ （其中 $\alpha$ 为非原子程序）的公式会被展开为一组有限的序列，该集合被称为“测试剖面”（test profiles）。该集合 $\text{unfold}_\square(\alpha, \psi)$ 代表了 $\alpha$ 所有可能的执行路径的析取，其中特定的测试成功或失败。
处理迭代： 为了防止对形如 $[\alpha^*]\psi$ 的公式进行无限的局部展开，系统在展开过程中会消除重新生成的公式出现。这依赖于 $[\alpha^*]\psi$ 是一个最大不动点的观察结果。
循环证明： 系统允许“重复”（即标签与祖先相同的节点）。
- 加载路径重复（Loaded-path repeats）： 指从祖先（伴随节点）到当前节点的路径完全由加载节点组成的重复。这些被视为“成功的”叶节点（表明满足公式的循环）。
- 自由重复（Free repeats）： 指路径中包含未加载节点的重复。这些被视为“不成功的”叶节点，指示潜在的反例模型。
终止性： 系统通过强制要求所有自由重复和加载路径重复均为叶节点，并利用 Fischer-Ladner 闭包来限制公式集合，从而确保了系统的有限性。

2.2. 通过拟表（Quasi-tableaux）与不动点方程实现插值

作者将 Maehara 的方法适配到循环设置中以构造插值式：

簇（Clusters）： 表被视为一个带有从重复节点指向伴随节点的回边（back edges）的有向图。该图的强连通分量（SCC）被称为“簇”。
拟表： 对于一个正规簇（非单元素 SCC），作者定义了一个“拟表”。该结构用于建立表征插值式的方程组。
前插值式（Pre-interpolants）： 该方法通过从叶向根的归纳法定义拟表节点的“前插值式”。
- 在退出节点（不属于簇的叶节点）处，前插值式是该退出节点的插值式（假设根据归纳法已存在）。
- 在重复叶节点处，前插值式是一个内部命题变量 $q_x$ 。
- 在伴随节点处，前插值式被定义为不动点方程的解。具体而言，如果伴随节点 $x$ 有一个子节点 $y$ ，其前插值式为 $\iota_y \equiv \bigwedge_i [\alpha_i]q_x \wedge \bigwedge_j [\beta_j]q_{z_j} \wedge \psi$ ，则 $x$ 的前插值式定义为 $\iota_x := [(\bigcup_i \alpha_i)^*](\bigwedge_j [\beta_j]q_{z_j} \wedge \psi)$ 。
在 PDL 中求解： 关键的洞察在于，这种特定的构造确保了不动点方程的解仍然保持在 PDL 的语言范围内。在 $\iota_x$ 的定义中使用迭代算子 $*$ 有效地在 PDL 内部解决了方程 $\iota_x \equiv \iota_y\langle q_x \mapsto \iota_x \rangle$ 。
最终插值式： 簇根节点的插值式是通过将根节点前插值式中的内部变量替换为相应的区域公式（即分裂序列左侧的析取）来获得的。

3. 主要贡献与结果

证明了 PDL 的 CIP： 本文确立了 PDL 具有克雷格插值性质。
Beth 可定义性： 作为推论，本文证明了 PDL 具有 Beth 可定义性（因为在存在演绎定理的情况下，CIP 蕴含 Beth 可定义性）。
构造性算法： 证明是构造性的。作者提供了一个清晰的算法，用于从闭合表（closed tableau）中计算插值式。
形式化验证： 作者已在交互式定理证明器 Lean 4 中部分形式化了该证明。截至论文撰写时，其可靠性（Soundness）和完备性（Completeness）定理以及若干支持性引理已通过验证。
实现： 提供了一个用 Haskell 实现的表系统及插值式构造程序，可通过 Web 界面访问。

4. 意义与主张

本文声称解决了关于 PDL 插值状态的文献谜题，提供了第一个克服了以往尝试中缺陷的经过验证的证明。

解决历史问题： 作者明确回应了插值尝试失败的历史，指出其方法虽然借鉴了 Borzechowski (1988) 的核心思想，但在处理循环证明和在 PDL 语言内构造插值式方面进行了严格的形式化。
方法论创新： 论文强调，虽然 Maehara 的方法对于非循环证明是标准的，但将其应用于循环证明（不动点逻辑）需要求解不动点方程。作者展示了对于 PDL，这些解可以使用逻辑自身的迭代算子来表达，这是一个非平凡的结果，将其与那些可能需要完整 $\mu$ -演算才能获得解的其它片段区分开来。
开放问题： 作者谦逊地指出，其方法依赖于测试程序（ $\tau?$ ）的存在。因此，PDL 的无测试片段是否具有插值性质仍是一个开放问题，因为即使输入是无测试的，其构造出的插值式通常仍会包含测试。此外，作者也留下了将该方法扩展到其他 PDL 变体（例如带有逆运算或交集运算的 PDL）以及对带测试的克莱尼代数（KAT）之影响等开放课题。

总而言之，本文通过一种新颖的循环表系统和专门的插值式不动点求解技术，为 PDL 提供了确定性的、构造性的克雷格插值证明，并辅以 Haskell 实现和部分 Lean 形式化验证。