Cyclic proof theory of positive inductive definitions

TL;DR

This paper demonstrates that cyclic proof systems for positive inductive definitions in arithmetic have the same proof-theoretic strength as traditional inductive systems, using formal translations and conservativity within second-order arithmetic.

Contribution

It establishes the equivalence in proof-theoretic strength between cyclic and inductive proof systems for positive inductive definitions in arithmetic, extending the analysis within second-order arithmetic.

Findings

Cyclic and inductive proofs prove the same theorems for $ ext{μ} ext{PA}$.

Translation of cyclic proofs into an annotated variant simplifies soundness proofs.

Formalisation within $ ext{Pi}^1_2$-$ ext{CA}_0$ leverages M"{o}llerfeld's conservativity.

Abstract

We study cyclic proof systems for $\mu\mathsf{PA}$, an extension of Peano arithmetic by positive inductive definitions that is arithmetically equivalent to the (impredicative) subsystem of second-order arithmetic $\Pi^1_2$-$\mathsf{CA}_0$ by M\"{o}llefeld. The main result of this paper is that cyclic and inductive $\mu\mathsf{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 $\mu$-calculus, whose stronger validity condition allows for a simpler proof of soundness. We then formalise this argument within $\Pi^1_2$-$\mathsf{CA}_0$, leveraging M\"{o}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 $\mu\mathsf{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.