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.

翻译：循环证明系统是一种证明图形为带循环的树的证明系统。证明系统中的切割消除是基础性的。据推测，在具有归纳定义的一阶逻辑循环证明系统中，切割消除不成立。本文通过给出一个在不使用切割规则时不可证明、但在循环证明系统中可证明的矢列，证明了该推测是正确的。