Cyclic proof theory of generalised inductive definitions

Gianluca Curzi, Lukas Melgaard

We study cyclic proof systems for $\mu \mathsf{PA}$, an extension of Peano arithmetic by positive inductive definitions that is arithmetically equivalent to the (impredicative) subsys…