Cyclic proofs for arithmetic with least and greatest fixed points
Lukas Melgaard
Authors: Lukas Melgaard and Gianluca Curzi
We investigate the cyclic proof theory of \(\mu \mathrm{PA}\), a theory that extends Peano Arithmetic with least and greatest fixed point operators. Our cyclic system \(\mathrm{C} \mu \mathrm{PA}\) subsumes Simpson’s cyclic arithmetic [3] and the stronger \(\mathrm{CID}_{< \omega}\) from [1].
Our main result is that the inductive system \(\mu \mathrm{PA}\) and the cyclic system \(\mathrm{C} \mu \mathrm{PA}\) prove the same arithmetical theorems. We conduct a metamathematical argument inspired by those in [3,1] 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 done in [1] for \(\mathrm{CID}_{< \omega}\) except here we also need to use the reverse mathematics of a more powerful version of Knaster-Tarski as seen in [2].
Bibliography
- A. Das and L. Melgaard,Cyclic Proofs for Arithmetical Inductive Definitions,8th International Conference on Formal Structures for Computation and Deduction, {FSCD},vol. 260,Schloss Dagstuhl - Leibniz-Zentrum f{ü}r Informatik,2023,pp. 27:1–27:18.
- G. Curzi and A. Das,Computational expressivity of (circular) proofs with fixed points,2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS),IEEE,2023,pp. 1–13.
- Alex Simpson,Cyclic Arithmetic Is Equivalent to Peano Arithmetic,Foundations of Software Science and Computation Structures - 20th International Conference, {FOSSACS},vol. 10203,Lecture Notes in Computer Science,2017,pp. 283–300.