PREDICATIVITY THROUGH TRANSFINITE REFLECTION
Andrés Cordón–Franco, David Fernández–Duque, Joost J. Joosten, Francisco Martín · Journal of Symbolic Logic · 2017
Abstract Let T be a second-order arithmetical theory, Λ a well-order, λ < Λ and X ⊆ ℕ. We use $[\lambda |X]_T^{\rm{\Lambda }}\varphi$ as a formalization of “φ is provable from T and an oracle for the set X, using ω-rules of nesting depth at most λ”. For a set of formulas Γ, define predicative oracle reflection for T over Γ (Pred–O–RFNΓ(T)) to be the schema that asserts that, if X ⊆ ℕ, Λ is a well-order and φ ∈ Γ, then $$\forall \,\lambda < {\rm{\Lambda }}\,([\lambda |X]_T^{\rm{\Lambda }}\varphi \to \varphi ).$$ In particular, define predicative oracle consistency (Pred–O–Cons(T)) as Pred–O–RFN{0=1}(T). Our main result is as follows. Let ATR0 be the second-order theory of Arithmetical Transfinite Recursion, ${\rm{RCA}}_0^{\rm{*}}$ be Weakened Recursive Comprehension and ACA be Arithmetical Comprehension with Full Induction. Then, $${\rm{ATR}}_0 \equiv {\rm{RCA}}_0^{\rm{*}} + {\rm{Pred - O - Cons\ }}\left( {{\rm{RCA}}_0^{\rm{*}} } \right) \equiv {\rm{RCA}}_0^{\rm{*}} + \,{\rm{Pred - O - Cons\ }}\left( {{\rm{RCA}}_0^{\rm{*}} } \right) \equiv {\rm{RCA}}_0^{\rm{*}} + \,{\rm{Pred - O - RFN}}\,_{{\bf{\Pi }}_2^1 } \left( {{\rm{ACA}}} \right).$$ We may even replace ${\rm{RCA}}_0^{\rm{*}}$ by the weaker ECA0, the second-order analogue of Elementary Arithmetic. Thus we characterize ATR0, a theory often considered to embody Predicative Reductionism, in terms of strong reflection and consistency principles.