A study for recovering the cut-elimination property in cyclic proof systems by restricting the arity of inductive predicates
Yukihiro Oda, Daisuke Kimura
TL;DR
The paper investigates whether restricting inductive predicates by arity can recover cut-elimination in cyclic proof systems. It constructs a base system $\mathcal{B}$ with unary inductive predicates $TeF$ and $FsT$ and shows that the cyclic system $C\mathcal{B}^{\omega}$ proves $TeF(s)\vdash FsT(e)$, yet this sequent is not cut-free provable, establishing a unary counterexample to cut-elimination. The result extends to the classical cyclic system $CLKID^{\omega}$ (and a variant $CLKID^{\omega}_{a}$ with a weakened left rule) and thus demonstrates that restricting predicates to unary does not restore cut-elimination, clarifying the limitations of naive cut-free proof search in cyclic settings. The work also discusses the cycle-normalization property and its role in the proof, and it outlines implications for automated theorem provers and future directions for restricting cuts or exploring other arity-based restrictions. Overall, the paper significantly sharpens understanding of why cut-elimination fails in cyclic proofs and informs the design of proof-search strategies for inductive definitions.
Abstract
The framework of cyclic proof systems provides a reasonable proof system for logics with inductive definitions. It also offers an effective automated proof search procedure for such logics without finding induction hypotheses. Recent researches have shown that the cut-elimination property, one of the most fundamental properties in proof theory, of cyclic proof systems for several logics does not hold. These results suggest that a naive proof search, which avoids the Cut rule, is not enough. This paper shows that the cut-elimination property still fails in a simple cyclic proof system even if we restrict languages to unary inductive predicates and unary functions, aiming to clarify why the cut-elimination property fails in the cyclic proof systems. The result in this paper is a sharper one than that of the first authors' previous result, which gave a counterexample using two ternary inductive predicates and a unary function symbol to show the failure of the cut-elimination property in the cyclic proof system of the first-order logic.