The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions
Yukihiro Oda, James Brotherston, Makoto Tatsuta
TL;DR
This work addresses the open question of cut-elimination for cyclic proofs in $CLKID^{\omega}$ over first-order logic with inductive definitions. It develops a rigorous framework combining $LKID^{\omega}$, a cyclic system $CLKID^{\omega}$, and a cycle-normalization technique, then constructs a concrete counterexample using inductive predicates $Add_1$ and $Add_2$ to show a sequent provable in $CLKID^{\omega}$ cannot be proved without cuts. The argument leverages a variant system $CLKID^{\omega}_a$, an index congruence $\cong_{\Gamma}$, and index-path methods to produce an infinite sequence of switching points, yielding a contradiction with finiteness of any cut-free pre-proof. The result demonstrates that cut-elimination fails in this setting, pointing to the need for restrictions or alternate systems to recover the subformula property and related metatheoretic benefits of cut-elimination.
Abstract
A cyclic proof system is a proof system whose proof figure is a tree with cycles. The cut-elimination in a proof system is fundamental. It is conjectured that the cut-elimination in the cyclic proof system for first-order logic with inductive definitions does not hold. This paper shows that the conjecture is correct by giving a sequent not provable without the cut rule but provable in the cyclic proof system.