Comparing theorems of hyperarithmetic analysis with the arithmetic Bolzano-Weierstrass theorem

Abstract:

In 1975 H. Friedman introduced two statements of hyperarithmetic analysis, $\mathsf {SL_0}$ (sequential limit system) and $\mathsf {ABW_0}$ (arithmetic Bolzano-Weierstrass), which are motivated by standard and well-known theorems from analysis such as the Bolzano-Weierstrass theorem for $F_\sigma$ and $G_\delta$ sets of reals. In this article we characterize the reverse mathematical strength of $\mathsf {ABW_0}$ by comparing it to most known theories of hyperarithmetic analysis.

In particular we show that, over $\mathsf {RCA_0+I\Sigma ^1_1}$, $\mathsf {SL_0}$ is equivalent to $\mathsf {\Sigma ^1_1-AC_0}$, and that $\mathsf {ABW_0}$ is implied by $\mathsf {\Sigma ^1_1-AC_0}$, and implies $\mathsf {weak-\Sigma ^1_1-AC_0}$. We then use Steel’s method of forcing with tagged trees to show that $\mathsf {ABW_0}$ is incomparable with $\mathsf {INDEC}$ (i.e. Jullien’s Theorem) and $\mathsf {\Delta ^1_1-CA_0}$. This makes $\mathsf {ABW_0}$ the first theory of hyperarithmetic analysis that is known to be incomparable with other (known) theories of hyperarithmetic analysis. We also examine the reverse mathematical strength of the Bolzano-Weierstrass theorem in the context of open, closed, $F_\sigma$, $G_\delta$, and other types of sets.