We study cyclic proof systems for μPA, an extension of Peano arithmetic by positive inductive definitions that is arithmetically equivalent to the (impredicative) subsystem of second-order arithmetic Π¹₂-CA₀ by Möllefeld. The main result of this paper is that cyclic and inductive μPA have the same proof-theoretic strength. First, we translate cyclic proofs into an annotated variant based on Sprenger and Dam's systems for first-order μ-calculus, whose stronger validity condition allows for a simpler proof of soundness. We then formalise this argument within Π¹₂-CA₀, leveraging Möllerfeld's conservativity properties. To this end, we build on prior work by Curzi and Das on the reverse mathematics of the Knaster-Tarski theorem. As a byproduct of our proof methods we show that, despite the stronger validity condition, annotated and "plain" cyclic proofs for μPA prove the same theorems. This work represents a further step in the non-wellfounded proof-theoretic analysis of theories of arithmetic via impredicative fragments of second-order arithmetic, an approach initiated by Simpson's Cyclic Arithmetic, and continued by Das and Melgaard in the context of arithmetical inductive definitions.
Curzi et al. (Thu,) studied this question.