Cyclic proofs for arithmetic with least and greatest fixed points
Lukas Melgaard, University of Birmingham
We investigate the cyclic proof theory of extensions of Peano Arithmetic, in particular µPA, a theory that extends Peano Arithmetic with least and greatest fixed point operators. Our cyclic system CµPA subsumes Simpson’s cyclic arithmetic and the stronger CID<ω. Our main result, which is still work in progress, is that the inductive system µPA and the cyclic system CµPA prove the same arithmetical theorems. We intend to conduct a metamathematical argument for Cyclic Arithmetic to formalize the soundness of cyclic proofs within second-order arithmetic by a form of induction on closure ordinals and then appealing to conservativity results. Since the closure ordinals of our inductive definitions far exceed the recursive ordinals we cannot rely on ordinal notations and must instead formalize a theory of ordinals within second-order arithmetic. This is similar to what is for CID<ω except here we also need to use the reverse mathematics of a more powerful version of Knaster-Tarski.