Hypersequent Calculi Have Ackermannian Complexity

这是一篇关于超序演算（Hypersequent Calculi）在子结构逻辑中证明搜索复杂度的学术论文。文章主要解决了关于具有收缩（Contraction）或弱化（Weakening）规则的子结构逻辑扩展系统的复杂度上界问题。

以下是该论文的详细技术总结：

1. 研究问题 (Problem)

• 背景：子结构逻辑（如线性逻辑、相关逻辑、模糊逻辑等）通过省略或修改经典逻辑中的结构规则（收缩、弱化、交换、结合律）来构建。其中，具有收缩规则的系统（如 $FL_{ec}$）和具有弱化规则的系统（如 $FL_{ew}$）是核心研究对象。
• 现状与困境：
  • 对于基本的 $FL_{ec}$（具有收缩的 Full Lambek 演算），其证明搜索空间可以通过 Dickson 引理（基于 $\mathbb{N}^d$ 上的良拟序 wqo）进行分析，证明了其判定问题是 Ackermannian 复杂度（即属于 $F_\omega$ 类）。
  • 然而，许多 $FL_{ec}$ 和 $FL_{ew}$ 的扩展系统（如模糊逻辑 MTL）无法在标准的序演算（Sequent Calculi）中拥有无割（cut-free）证明系统，必须使用更通用的超序演算（Hypersequent Calculi）。
  • 超序演算将“多重集”提升为“多重集的多重集”（即超序是序的多重集）。之前的研究（如 Balasubramanian et al.）尝试将 wqo 从序（Sequents）提升到超序的幂集（Powerset）上。由于幂集上的良拟序长度定理对应的是 Hyper-Ackermannian 复杂度（即 $F_{\omega^\omega}$ 类），这导致人们推测：使用超序演算的系统其复杂度必然从 Ackermannian 跳跃到 Hyper-Ackermannian。
• 核心问题：这种从序到超序的转换是否必然导致复杂度从 Ackermannian 跳跃到 Hyper-Ackermannian？是否存在一种方法，使得超序演算的判定问题仍然保持在 Ackermannian 复杂度？

2. 方法论 (Methodology)

作者提出了一种新的证明搜索策略，避免了将良拟序（wqo）直接提升到幂集上，而是利用超序内部组件之间的新型依赖关系。

A. 针对收缩逻辑 ($FL_{ec}$) 的方法

1. 可逆化与细化演算：
   • 将超序演算转换为可逆形式（Invertible form），允许结论中的组件在前提中保留。
   • 引入细化收缩演算（Refined contraction calculus），通过限制收缩规则的应用次数（基于公式多重性和活跃组件数量），确保结构规则的高度保持可容许性（hp-admissible）。
2. 坏序列分析（Bad Sequence Analysis）：
   • 关键洞察：在向后证明搜索中，将超序视为按添加顺序排列的序序列。
   • 利用 Dickson 引理在序（Sequents）上的 wqo 性质，证明超序的线性化序列本身就是一个受控的坏序列（Controlled Bad Sequence）。
   • 通过控制函数（Control Function）限制序列中元素的增长，证明了搜索树的深度受限于 Ackermannian 函数，从而避免了幂集带来的复杂度爆炸。

B. 针对弱化逻辑 ($FL_{ew}$) 的方法

弱化情况更为复杂，因为简单的向后搜索可能无法终止（由于弱化规则可以无限增加公式）。作者引入了类似 Karp-Miller 算法的加速机制：

1. $\omega$-公式与 $\omega$-序：
   • 扩展语言，引入 $\omega$-公式（$\varphi^\omega$），表示某公式的计数可以无限增长。
   • 定义 $\omega$-序（$\omega$-sequent），包含一个有限多重集向量（表示有限计数）和一个 $\omega$-集合（表示无限计数的公式）。
2. 加速机制（Acceleration）：
   • 在证明搜索树中，如果某个组件的有限计数严格大于之前出现过的某个组件，则触发“加速”：将该公式标记为 $\omega$-公式（即放入 $\omega$-集合，并将有限计数归零）。
   • 这模拟了 Karp-Miller 算法中覆盖集（Coverability Set）的构建，防止了无限增长的计数导致搜索树无限延伸。
3. 依赖关系与 $\omega$-精炼：
   • 定义索引超序（Indexed Hypersequents）和关系索引超序（Relational Indexed Hypersequents），记录组件生成的顺序和依赖关系（Key Ancestor）。
   • 引入 $\omega$-精炼（$\omega$-refinement）：当检测到严格递增时，利用 $\omega$-函数将组件替换为其 $\omega$-扩展版本。
   • 证明了在这种机制下，搜索树的分支是受控的坏序列，且长度受限于 $F_\omega$ 类函数。

3. 主要贡献 (Key Contributions)

1. 推翻直觉：证明了具有无割超序演算的 $FL_{ec}$ 和 $FL_{ew}$ 的扩展系统，其判定问题并非必然具有 Hyper-Ackermannian 复杂度，而是可以保持在 Ackermannian 复杂度（$F_\omega$）。
2. 优化 $FL_{ec}$ 上界：对于收缩情况，证明了其复杂度上界是最优的（因为 $FL_{ec}$ 本身就已经达到了 Ackermannian 复杂度）。
3. 解决 $FL_{ew}$ 及 MTL 的长期开放问题：
   • 首次为基本模糊逻辑 MTL（由 $FL_{ew}$ 加前线性公理 $(p \to q) \lor (q \to p)$ 定义）提供了 Ackermannian 复杂度上界。
   • 此前 MTL 的复杂度上界未知，之前的超序分析暗示可能是 Hyper-Ackermannian。
   • 该结果同样适用于其他标准完备的模糊逻辑（如 $n$-contractive 扩展和 $wmn$-扩展）。
4. 技术突破：
   • 提出了一种避免幂集提升（Powerset lifting）的新方法，通过利用超序组件间的依赖关系，直接在序的 wqo 上进行分析。
   • 将 Karp-Miller 加速思想创造性地应用于证明论中的超序搜索，设计了复杂的 $\omega$-精炼机制。

4. 结果 (Results)

• 定理 3.14 (Main Theorem I)：任何通过有限个无环 $P'_3$-公理扩展的 $FL_{ec}$（即 $HFL_{ec}$ 的任何解析结构扩展），其可判定性具有 Ackermannian 复杂度。
• 定理 6.4 (Main Theorem II)：任何通过有限个 $P_3$-公理扩展的 $FL_{ew}$（即 $HFL_{ew}$ 的任何解析结构扩展），其可判定性具有 Ackermannian 复杂度。
• 推论 6.5：模糊逻辑 MTL 具有 Ackermannian 复杂度。
• 算法复杂度：提出的证明搜索算法（$Wkn$）在$F^\star_\omega$ 时间内终止。

5. 意义 (Significance)

1. 理论突破：打破了“超序演算必然导致复杂度从 $F_\omega$ 跳跃到 $F_{\omega^\omega}$"的固有认知。这表明，只要仔细分析证明结构中的依赖关系，即使是在更复杂的超序框架下，也能保持较低的复杂度上界。
2. 解决开放问题：彻底解决了 MTL 及其相关模糊逻辑的复杂度上界这一长期悬而未决的问题，将其从“未知/推测为极高”明确为 Ackermannian。
3. 方法论价值：
   • 为无限状态系统（Infinite-state systems）社区提供了新的视角：通过更精细地分析坏序列（Bad Sequences）和证明演算的结构，可以改进基于良拟序（wqo）的复杂度分析。
   • 展示了如何将自动机理论中的加速技术（如 Karp-Miller）与证明论（Proof Theory）相结合，处理具有弱化规则的逻辑系统。
4. 实际应用：为模糊逻辑、多值逻辑等子结构逻辑系统的自动推理工具（定理证明器、模型检查器）提供了坚实的理论基础，表明这些系统的判定问题在理论上是可处理的（尽管复杂度很高，但并非不可控的 Hyper-Ackermannian）。

总结：该论文通过创新的证明搜索策略和良拟序分析技术，成功地将子结构逻辑超序演算的复杂度上界从推测的 Hyper-Ackermannian 降低到了 Ackermannian，不仅解决了 MTL 等核心逻辑的复杂度问题，也为子结构逻辑的证明论研究开辟了新方向。