Approximation of hyperarithmetic analysis by $\omega$-model reflection

TL;DR

This paper explores new variants of the dependent choice axiom and their relation to hyperarithmetic analysis, demonstrating how $ ext{RFN}^{-1}( ext{ATR}_0)$ theories approximate hyperarithmetic analysis through $ ext{ω}$-model reflection.

Contribution

It introduces novel variants of the dependent choice axiom that belong to hyperarithmetic analysis and connects $ ext{RFN}^{-1}( ext{ATR}_0)$ theories with hyperarithmetic analysis.

Findings

New variants of dependent choice imply $ ext{ACA}_0^+$ but not $ ext{Σ}^1_1$-induction.

These variants are situated within hyperarithmetic analysis.

$ ext{RFN}^{-1}( ext{ATR}_0)$ theories approximate hyperarithmetic analysis.

Abstract

This paper presents two types of results related to hyperarithmetic analysis. First, we introduce new variants of the dependent choice axiom, namely $\mathrm{unique}~\Pi^1_0(\mathrm{resp.}~\Sigma^1_1)\text{-}\mathsf{DC}_0$ and $\mathrm{finite}~\Pi^1_0(\mathrm{resp.}~\Sigma^1_1)\text{-}\mathsf{DC}_0$. These variants imply $\mathsf{ACA}_0^+$ but do not imply $\Sigma^1_1\mathrm{~Induction}$. We also demonstrate that these variants belong to hyperarithmetic analysis and explore their implications with well-known theories in hyperarithmetic analysis. Second, we show that $\mathsf{RFN}^{-1}(\mathsf{ATR}_0)$, a class of theories defined using the $\omega$-model reflection axiom, approximates to some extent hyperarithmetic analysis, and investigate the similarities between this class and hyperarithmetic analysis.