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

TL;DR

This paper demonstrates that cut-elimination fails in cyclic proof systems for first-order logic with inductive definitions by providing a specific sequent that requires the cut rule.

Contribution

It proves the conjecture that cut-elimination does not hold in this cyclic proof system by constructing a provable sequent that cannot be proved without cut.

Findings

Cut-elimination does not hold in the cyclic proof system for first-order logic with inductive definitions.

A specific sequent is shown to be provable only with the cut rule.

The result confirms the conjecture about the failure of cut-elimination in this context.

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.