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.

We prove that the standard cut is definable in each existentially closed model of IΔ0 + exp by a (parameter free) П1–formula. This definition is optimal with respect to quantifier complexity and allows us to improve some previously known results on existentially closed models of fragments of arithmetic.