Admissibility of Substitution Rule in Cyclic-Proof Systems
Kenji Saotome, Koji Nakazawa
TL;DR
Addresses the admissibility of the substitution rule in cyclic-proof systems for the first-order logic with inductive predicates, a property with implications for proof search efficiency. Proposes a method that unfolds cyclic proofs into an infinitary form, lifts substitution rules, and reconstructs a cyclic proof without the substitution rule, assuming the presence of a cut. Proves admissibility of $(Subst)$ in $CLKID^omega$, and shows that restricting substitutions to atomic terms extends the result to cut-free $CLKID^omega$ and to cyclic-proof systems for separation logic. The work provides a constructive procedure and discusses generalization to other cyclic-proof frameworks.
Abstract
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.