On a proof-theoretical analysis of Σ ¹₁ -AC, Σ ¹₁ -DC and Δ ¹₁ -CA

Abstract

We present a simple method of embedding of δ ¹₁ -CA, σ ¹₁ -AC and σ ¹₁ -DC into $RA_{\varepsilon _0 } ,(RA + PAC)_{\varepsilon _0 }$, and $(RA + PDC)_{\varepsilon _0 }$ respectively, where PAC is Predicative Axiom of Choice and PDC is Predicative Axiom of Dependent Choice, These ramified systems are known to have proof-theoretic ordinals Φε ₀0, which in the case of PAC and PDC can be proved by normalization of Ramified Analysis with Hilbert's epsilon-symbol. In all cases (particularly, of δ ¹₁ -CA) our embedding is straightforward and avoids any intermediate steps (like σ ¹₁ -Reflection), which was always the case before.