Predicativity through Transfinite Reflection

Abstract

Let T be a second-order arithmetical theory, Λ a well-order, λ < Λ and X ⊆ ℕ. We use 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

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, be Weakened Recursive Comprehension and ACA be Arithmetical Comprehension with Full Induction. Then,

We may even replace 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.