2025-11-23T13:43:17.173951

Admissibility of Substitution Rule in Cyclic-Proof Systems

Saotome, Nakazawa
This paper investigates the admissibility of the substitution rule in cyclic-proof systems. The substitution rule complicates theoretical case analysis and increases computational cost in proof search since every sequent can be a conclusion of an instance of the substitution rule; hence, admissibility is desirable on both fronts. While admissibility is often shown by local proof transformations in non-cyclic systems, such transformations may disrupt cyclic structure and do not readily apply. Prior remarks suggested that the substitution rule is likely nonadmissible in the cyclic-proof system CLKID^omega for first-order logic with inductive predicates. In this paper, we prove admissibility in CLKID^omega, assuming the presence of the cut rule. Our approach unfolds a cyclic proof into an infinitary form, lifts the substitution rules, and places back edges to construct a cyclic proof without the substitution rule. If we restrict substitutions to exclude function symbols, the result extends to a broader class of systems, including cut-free CLKID^omega and cyclic-proof systems for the separation logic.
academic

Admissibility of Substitution Rule in Cyclic-Proof Systems

基本信息

  • 论文ID: 2510.14749
  • 标题: Admissibility of Substitution Rule in Cyclic-Proof Systems
  • 作者: Kenji Saotome, Koji Nakazawa (名古屋大学)
  • 分类: cs.LO (逻辑学)
  • 发表时间: 2025年10月16日
  • 论文链接: https://arxiv.org/abs/2510.14749

摘要

本文研究循环证明系统中替换规则的可容许性问题。替换规则会使理论分析复杂化并增加证明搜索的计算成本，因为每个继式都可能是替换规则实例的结论，因此可容许性在理论和实践两方面都是理想的。虽然在非循环系统中可容许性通常通过局部证明变换来证明，但这种变换可能破坏循环结构，不能直接应用。先前的研究表明，替换规则在带归纳谓词的一阶逻辑循环证明系统CLKIDω中很可能不可容许。本文证明了在存在切割规则的情况下，CLKIDω中替换规则是可容许的。我们的方法是将循环证明展开为无穷形式，提升替换规则，然后放回边来构造不含替换规则的循环证明。如果限制替换不引入函数符号，该结果可扩展到更广泛的系统类别，包括无切割的CLKIDω和分离逻辑的循环证明系统。

研究背景与动机

问题定义

循环证明是传统证明树的扩展，通过引入循环结构来推理归纳定义的谓词。替换规则 Γ⊢ΔΓ[θ]⊢Δ[θ]\frac{\Gamma \vdash \Delta}{\Gamma[\theta] \vdash \Delta[\theta]} (Subst) 在许多循环证明系统中被引入，用于帮助构造循环结构。

问题重要性

  1. 理论角度：替换规则总是可应用的，这使得证明分析变得复杂
  2. 实践角度：无限制地应用替换规则会增加计算成本，因为每一步都可以应用许多替换

现有方法的局限性

在非循环证明系统中，替换规则的可容许性通常通过两个阶段实现：

  1. 提升阶段：将替换规则向上移动
  2. 消除阶段：在公理处消除替换规则

但在循环证明系统中，这种方法面临根本性困难：

  • 提升阶段可能破坏芽-伴侣关系（bud-companion relationship）
  • 消除阶段无法在芽处消除替换

研究动机

Brotherston 1 提出了替换规则在CLKIDω中是否可容许的问题，暗示在一般情况下，至少在无切割设置中，它很可能不可容许。本文旨在解决这一开放问题。

核心贡献

  1. 主要理论结果：证明了在存在切割规则的情况下，CLKIDω中替换规则是可容许的
  2. 扩展结果：当限制替换为原子替换（不引入正元数函数符号）时，结果扩展到无切割CLKIDω
  3. 应用推广：该结果适用于其他证明系统，如分离逻辑的循环证明系统
  4. 新颖方法：提出了通过无穷展开、替换提升和循环重构的三步消除策略

方法详解

任务定义

给定一个在CLKIDω中包含替换规则的证明Pr+，构造一个不包含替换规则的证明Pr-，使得两者证明相同的继式。

核心方法架构

本文的消除过程分为两个主要阶段：

1. 复合替换的消除

定义：

  • 原子替换：像只包含变量和常量
  • 复合替换：像包含正元数函数符号的项

方法：通过以下变换消除复合替换：

Γ ⊢ Δ
────────────────────────── (Subst)
Γ[x₁:=t₁,...,xₙ:=tₙ] ⊢ Δ[x₁:=t₁,...,xₙ:=tₙ]

变换为使用切割规则、等式规则和存在量词规则的组合，最终只保留原子替换。

2. 原子替换的消除

这是核心创新，包含三个步骤：

步骤1：循环展开

  • 将循环证明Pr_var+展开为无穷证明Pr^ω
  • 定义映射f^ω：Seq(Pr^ω) → Seq(Pr_var+)关联继式出现

步骤2：替换提升

  • 递归构造LKIDω证明Pr^ω_d，在深度d内不包含替换规则
  • 使用替换应用性质（substitution-application property）

步骤3：循环重构

  • 从Pr^ω_d构造CLKIDω预证明Pr-
  • 选择芽和伴侣，确保全局轨迹条件

技术创新点

1. 偏替换闭包（Partial-substitution Closure）

定义10：给定替换集合Θ和变量集合X，偏替换闭包Cps(Θ,X)是满足以下条件的最小集合：

  • Θ ⊆ Cps(Θ,X)
  • 对于θ∈Cps(Θ,X)和x,y∈X：θx→y ∈ Cps(Θ,X)
  • 对于θ₁,θ₂∈Cps(Θ,X)：θ₁θ₂ ∈ Cps(Θ,X)

关键性质：当限制为原子替换时，偏替换闭包是有限的。

2. 替换应用性质（Substitution-application Property）

定义11：规则(R)满足替换应用性质，如果对于任何规则实例和原子替换θ，都存在相应的替换应用实例，且保持轨迹。

引理4：CLKIDω和LKIDω满足替换应用性质。

3. 全局轨迹条件的保持

通过对应路径的概念确保重构的证明满足全局轨迹条件：

定义12：对于Pr-中的路径(eᵢ)，定义Pr_var+中的对应路径(e'ⱼ)，使得每个无穷进行轨迹都被保持。

实验设置

本文是纯理论工作，没有传统意义上的实验。验证通过以下方式进行：

理论验证

  1. 构造性证明：通过显式构造算法证明可容许性
  2. 反例分析：分析在限制条件下不满足可容许性的情况
  3. 系统扩展：验证结果在其他系统中的适用性

示例分析

论文提供了具体的证明变换示例：

  • 图1：包含替换规则的循环证明
  • 图3：展开后的无穷证明
  • 展示了如何从N(x) ⊢ E(x)∨O(x)的循环证明消除替换规则

实验结果

主要理论结果

定理2（CLKIDω中替换规则的可容许性）： 如果Γ ⊢ Δ在CLKIDω中可证，那么它在不含(Subst)的CLKIDω中也可证。

定理3（原子替换的强结果）： 如果Pr是CLKIDω中Γ ⊢ Δ的证明且Θ(Pr)只包含原子替换，那么存在不含(Subst)的证明，且只包含Pr中出现的规则。

扩展结果

定理4（无切割系统中的可容许性）： 在CLKIDω^-（无切割CLKIDω）中，原子替换规则是可容许的。

定理5（分离逻辑中的应用）： 替换规则在CSLω和CSLω^-中都是可容许的。

理论发现

  1. 切割规则的关键作用：复合替换的消除需要切割规则
  2. 原子替换的普遍性：原子替换的消除适用于更广泛的系统
  3. 函数符号的限制性：函数符号的存在是可容许性的关键障碍

相关工作

主要研究方向

  1. 循环证明理论：Brotherston等人的开创性工作1,4,6
  2. 证明搜索：避免启发式归纳假设搜索的研究2,3,5,11,12
  3. 分离逻辑：循环证明在分离逻辑中的应用2,7,9

本文与相关工作的关系

  • 解决了Brotherston 1提出的开放问题
  • 扩展了Kimura等人7的工作到更一般的设置
  • 为证明搜索提供了理论基础

本文的优势

  1. 首次证明：首次严格证明CLKIDω中替换规则的可容许性
  2. 方法创新：提出了适用于循环结构的新消除技术
  3. 广泛适用：结果适用于多个相关系统

结论与讨论

主要结论

  1. 在存在切割规则的CLKIDω中，替换规则是可容许的
  2. 当限制为原子替换时，结果扩展到无切割系统
  3. 该结果适用于分离逻辑等其他重要系统

局限性

  1. 切割规则依赖：复合替换的消除需要切割规则
  2. 函数符号限制：完全一般的结果需要排除函数符号
  3. 构造复杂性：证明构造过程相对复杂

未来方向

  1. 最小规则集：研究在存在函数符号时仍允许替换规则消除的最小规则集
  2. 切割消除：通过引入额外规则研究循环证明系统的切割消除性质
  3. 计算复杂性：分析替换规则消除的计算复杂性

深度评价

优点

  1. 理论重要性：解决了该领域的一个重要开放问题
  2. 方法创新：提出了适用于循环结构的新技术
  3. 严格性：证明严格且构造性
  4. 广泛适用：结果适用于多个相关系统
  5. 清晰表述：技术细节表述清晰，易于理解

不足

  1. 实用性限制：对切割规则的依赖限制了实际应用
  2. 复杂性：证明变换过程相对复杂
  3. 完全性：在无切割设置中仍有限制

影响力

  1. 理论贡献：为循环证明理论提供了重要理论基础
  2. 实用价值：为证明搜索实现提供了更大灵活性
  3. 可扩展性：方法可能适用于其他相关系统

适用场景

  1. 自动定理证明：提高循环证明搜索的效率
  2. 程序验证：在分离逻辑等验证框架中的应用
  3. 理论研究：为进一步的循环证明理论研究提供基础

参考文献

论文引用了19篇相关文献，主要包括：

  1. Brotherston的循环证明开创性工作
  2. 分离逻辑中循环证明的应用研究
  3. 自动证明搜索的相关工作
  4. 切割消除和证明理论的基础研究

这篇论文在循环证明理论方面做出了重要贡献，通过创新的技术手段解决了一个重要的开放问题，为该领域的进一步发展奠定了基础。