On the $Π^1_2$ consequences of $Π^1_1$-$\mathsf{CA}_0$

Yudai Suzuki, Keita Yokoyama

Published 2024-02-11, updated 2024-11-22Version 2

In this paper, we introduce a hierarchy dividing the set $\{\sigma \in \Pi^1_2 : \Pi^1_1$-$\mathsf{CA}_0 \vdash \sigma\}$. Then, we give some characterizations of this set using weaker variants of some principles equivalent to $\Pi^1_1$-$\mathsf{CA}_0$: leftmost path principle, Ramsey's theorem for $\Sigma^0_n$ classes of $[\mathbb{N}]^{\mathbb{N}}$ and determinacy for $(\Sigma^0_1)_n$ classes of $\mathbb{N}^{\mathbb{N}}$.