On the Π¹₂ consequences of Π¹₁-CA₀

The system Π¹₁-CA₀ is known as the strongest system of the big five in reverse mathematics. It is known that some theorems represented by a Π¹₂ sentence, for example Kruskal's theorem, are provable from Π¹₁-CA₀ but not provable from the second strongest system ATR₀ of the big five. However, since any Π¹₂ sentence is not equivalent to Π¹₁-CA₀, Π¹₁-CA₀ is too strong to prove such theorems. In this paper, we introduce a hierarchy dividing the set \σ ∈ Π¹₂ : Π¹₁-CA₀ σ\. Then, we give some characterizations of this hierarchy using some principles equivalent to Π¹₁-CA₀: leftmost path principle, Ramsey's theorem for Σ⁰ₙ classes of [N]N and determinacy for (Σ⁰₁)ₙ classes of NN. As an application, our hierarchy explicitly shows that the number of application of the hyperjump operator needed to prove Σ⁰ₙ Ramsey's theorem or (Σ⁰₁)ₙ determinacy increases when the subscript n increases.