Cyclic versions of arithmetic theories with inductive definitions
Lukas Melgaard
We investigate the cyclic proof theory of extensions of Peano Arithmetic by (finitely iterated) inductive definitions. Such theories are essential to proof theoretic analyses of certain `impredicative’ theories; moreover, our cyclic systems naturally subsume Simpson’s Cyclic Arithmetic.
Our main result is that cyclic and inductive systems for arithmetical inductive definitions are equally powerful. We conduct a metamathematical argument, formalising the soundness of cyclic proofs within second-order arithmetic and appealing to conservativity. This approach is inspired by those of Simpson and Das for Cyclic Arithmetic, however we must further address a difficulty that the closure ordinals of our inductive definitions (around Church-Kleene) far exceed the proof theoretic ordinal of the appropriate metatheory (around Bachmann-Howard or Bucholz), and so explicit induction on their notations is not possible. For this reason, we rather rely on a formalisation of the theory of (recursive) ordinals within second-order arithmetic.