Cyclic proof theory of generalised inductive definitions

Gianluca Curzi, Lukas Melgaard

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