The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions

Yukihiro Oda, James Brotherston, Makoto Tatsuta

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 i…