In:
The Journal of Symbolic Logic, Cambridge University Press (CUP), Vol. 82, No. 3 ( 2017-09), p. 787-808
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 ATR 0 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 ECA 0 , the second-order analogue of Elementary Arithmetic. Thus we characterize ATR 0 , a theory often considered to embody Predicative Reductionism, in terms of strong reflection and consistency principles.
Type of Medium:
Online Resource
ISSN:
0022-4812
,
1943-5886
Language:
English
Publisher:
Cambridge University Press (CUP)
Publication Date:
2017
detail.hit.zdb_id:
2010607-5
SSG:
5,1
SSG:
17,1
