Admissibility of Substitution Rule in Cyclic-Proof Systems

Basic Information

• Paper ID: 2510.14749
• Title: Admissibility of Substitution Rule in Cyclic-Proof Systems
• Authors: Kenji Saotome, Koji Nakazawa (Nagoya University)
• Classification: cs.LO (Logic)
• Publication Date: October 16, 2025
• Paper Link: https://arxiv.org/abs/2510.14749

Abstract

This paper investigates the admissibility of the substitution rule in cyclic-proof systems. The substitution rule complicates theoretical analysis and increases computational costs in proof search, since every sequent could potentially be the conclusion of a substitution rule instance; therefore, admissibility is desirable from both theoretical and practical perspectives. While admissibility in non-cyclic systems is typically established through local proof transformations, such transformations may destroy cyclic structures and cannot be directly applied. Previous research suggested that the substitution rule is likely inadmissible in CLKIDω, a cyclic-proof system for first-order logic with inductive predicates. This paper proves that the substitution rule is admissible in CLKIDω in the presence of the cut rule. Our approach unfolds cyclic proofs into infinite forms, lifts the substitution rule, and then reconstructs edges to build cyclic proofs without the substitution rule. When restricted to substitutions that do not introduce function symbols, this result extends to a broader class of systems, including cut-free CLKIDω and cyclic-proof systems for separation logic.

Research Background and Motivation

Problem Definition

Cyclic proofs extend traditional proof trees by introducing cyclic structures to reason about inductively defined predicates. The substitution rule $\frac{\Gamma \vdash \Delta}{\Gamma[\theta] \vdash \Delta[\theta]}$ (Subst) is introduced in many cyclic-proof systems to facilitate the construction of cyclic structures.

Problem Significance

1. Theoretical perspective: The substitution rule is always applicable, which complicates proof analysis
2. Practical perspective: Unrestricted application of the substitution rule increases computational costs, as many substitutions can be applied at each step

Limitations of Existing Approaches

In non-cyclic proof systems, admissibility of the substitution rule is typically established through two stages:

1. Lifting stage: Moving the substitution rule upward
2. Elimination stage: Eliminating the substitution rule at axioms

However, in cyclic-proof systems, this approach faces fundamental difficulties:

• The lifting stage may destroy bud-companion relationships
• The elimination stage cannot eliminate substitution at buds

Research Motivation

Brotherston 1 raised the question of whether the substitution rule is admissible in CLKIDω, suggesting that in general, at least in the cut-free setting, it is likely inadmissible. This paper aims to resolve this open problem.

Core Contributions

1. Main theoretical result: Proves that the substitution rule is admissible in CLKIDω in the presence of the cut rule
2. Extended result: When restricted to atomic substitutions (not introducing positive-arity function symbols), the result extends to cut-free CLKIDω
3. Generalized application: The result applies to other proof systems, such as cyclic-proof systems for separation logic
4. Novel methodology: Proposes a three-step elimination strategy through infinite unfolding, substitution lifting, and cyclic reconstruction

Detailed Methodology

Task Definition

Given a proof Pr+ in CLKIDω containing the substitution rule, construct a proof Pr- without the substitution rule such that both prove the same sequent.

Core Method Architecture

The elimination process consists of two main stages:

1. Elimination of Composite Substitutions

Definition:

• Atomic substitution: Substitutions containing only variables and constants
• Composite substitution: Substitutions containing terms with positive-arity function symbols

Method: Eliminate composite substitutions through the following transformation:

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

Transform into combinations using cut rules, equality rules, and existential quantifier rules, ultimately preserving only atomic substitutions.

2. Elimination of Atomic Substitutions

This is the core innovation, consisting of three steps:

Step 1: Cyclic Unfolding

• Unfold the cyclic proof Pr_var+ into an infinite proof Pr^ω
• Define mapping f^ω: Seq(Pr^ω) → Seq(Pr_var+) associating sequent occurrences

Step 2: Substitution Lifting

• Recursively construct LKIDω proof Pr^ω_d that contains no substitution rules within depth d
• Employ the substitution-application property

Step 3: Cyclic Reconstruction

• Construct CLKIDω pre-proof Pr- from Pr^ω_d
• Select buds and companions ensuring the global trace condition

Technical Innovations

1. Partial-substitution Closure

Definition 10: Given a set of substitutions Θ and a set of variables X, the partial-substitution closure Cps(Θ,X) is the minimal set satisfying:

• Θ ⊆ Cps(Θ,X)
• For θ∈Cps(Θ,X) and x,y∈X: θx→y ∈ Cps(Θ,X)
• For θ₁,θ₂∈Cps(Θ,X): θ₁θ₂ ∈ Cps(Θ,X)

Key property: When restricted to atomic substitutions, the partial-substitution closure is finite.

2. Substitution-application Property

Definition 11: A rule (R) satisfies the substitution-application property if for any rule instance and atomic substitution θ, there exists a corresponding substitution-applied instance that preserves the trace.

Lemma 4: CLKIDω and LKIDω satisfy the substitution-application property.

3. Preservation of Global Trace Condition

Ensure the reconstructed proof satisfies the global trace condition through the concept of corresponding paths:

Definition 12: For a path (eᵢ) in Pr-, define a corresponding path (e'ⱼ) in Pr_var+ such that every infinite progressing trace is preserved.

Experimental Setup

This paper is purely theoretical work without traditional experiments. Verification is conducted through:

Theoretical Verification

1. Constructive proof: Prove admissibility through explicit algorithm construction
2. Counterexample analysis: Analyze cases where admissibility fails under restricted conditions
3. System extension: Verify applicability of results to other systems

Example Analysis

The paper provides concrete proof transformation examples:

• Figure 1: Cyclic proof containing the substitution rule
• Figure 3: Unfolded infinite proof
• Demonstrates elimination of substitution rule from cyclic proof of N(x) ⊢ E(x)∨O(x)

Experimental Results

Main Theoretical Results

Theorem 2 (Admissibility of Substitution Rule in CLKIDω): If Γ ⊢ Δ is provable in CLKIDω, then it is also provable in CLKIDω without (Subst).

Theorem 3 (Stronger Result for Atomic Substitutions): If Pr is a proof of Γ ⊢ Δ in CLKIDω and Θ(Pr) contains only atomic substitutions, then there exists a proof without (Subst) containing only rules appearing in Pr.

Extended Results

Theorem 4 (Admissibility in Cut-free Systems): In CLKIDω^- (cut-free CLKIDω), the atomic substitution rule is admissible.

Theorem 5 (Application to Separation Logic): The substitution rule is admissible in both CSLω and CSLω^-.

Theoretical Findings

1. Critical role of cut rule: Elimination of composite substitutions requires the cut rule
2. Universality of atomic substitutions: Elimination of atomic substitutions applies to broader systems
3. Restrictiveness of function symbols: The presence of function symbols is a key obstacle to admissibility

Related Work

Main Research Directions

1. Cyclic proof theory: Pioneering work by Brotherston et al. 1,4,6
2. Proof search: Research avoiding heuristic inductive hypothesis search 2,3,5,11,12
3. Separation logic: Applications of cyclic proofs in separation logic 2,7,9

Relationship to Related Work

• Resolves the open problem posed by Brotherston 1
• Extends work by Kimura et al. 7 to more general settings
• Provides theoretical foundation for proof search

Advantages of This Paper

1. First rigorous proof: First strict proof of admissibility of substitution rule in CLKIDω
2. Methodological innovation: Proposes new elimination techniques applicable to cyclic structures
3. Broad applicability: Results apply to multiple related systems

Conclusions and Discussion

Main Conclusions

1. The substitution rule is admissible in CLKIDω with the cut rule
2. When restricted to atomic substitutions, the result extends to cut-free systems
3. The result applies to other important systems such as separation logic

Limitations

1. Cut rule dependence: Elimination of composite substitutions requires the cut rule
2. Function symbol restriction: Complete general results require excluding function symbols
3. Construction complexity: The proof construction process is relatively complex

Future Directions

1. Minimal rule sets: Investigate minimal rule sets that still allow substitution rule elimination in the presence of function symbols
2. Cut elimination: Study cut elimination properties of cyclic-proof systems through introduction of additional rules
3. Computational complexity: Analyze computational complexity of substitution rule elimination

In-depth Evaluation

Strengths

1. Theoretical importance: Resolves an important open problem in the field
2. Methodological innovation: Proposes new techniques applicable to cyclic structures
3. Rigor: Proofs are rigorous and constructive
4. Broad applicability: Results apply to multiple related systems
5. Clear presentation: Technical details are clearly presented and easy to understand

Weaknesses

1. Practical limitations: Dependence on cut rule limits practical applications
2. Complexity: The proof transformation process is relatively complex
3. Completeness: Restrictions remain in the cut-free setting

Impact

1. Theoretical contribution: Provides important theoretical foundation for cyclic proof theory
2. Practical value: Provides greater flexibility for proof search implementation
3. Extensibility: Methods may apply to other related systems

Applicable Scenarios

1. Automated theorem proving: Improve efficiency of cyclic proof search
2. Program verification: Applications in verification frameworks such as separation logic
3. Theoretical research: Provides foundation for further research in cyclic proof theory

References

The paper cites 19 related references, primarily including:

1. Pioneering work on cyclic proofs by Brotherston
2. Research on applications of cyclic proofs in separation logic
3. Related work on automated proof search
4. Foundational research on cut elimination and proof theory

This paper makes important contributions to cyclic proof theory by resolving an important open problem through innovative technical methods, laying the foundation for further development in the field.