Numerical choice and reverse mathematics

Question

Consider the following fragment of numerical choice in the language of second-order arithmetic:

for any arithmetical $\varphi$, we have: $$ (\forall n\in \mathbb{N})(\exists m\in \mathbb{N})(\forall X\subset \mathbb{N})\varphi(X, n, m) \rightarrow (\exists g\in \mathbb{N}^{ \mathbb{N}} )(\forall n\in \mathbb{N})(\forall X\subset \mathbb{N})\varphi(X, n, g(n)) $$ Is anything known about this principle? How does it interact with the Big Five, for instance, or how does it relate to hyperarithmetical analysis?

What happens if we only require $g$ to provide an upper bound, i.e. $(\exists m\leq g(n))$ in the consequent?

Answer 1

Both your choice principle, and its weakening to only give upper bounds, are equivalent to $\text{ATR}_0$ over $\text{RCA}_0$. I think your question provides a good illustration of hyperarithmetic theory and $\text{ATR}_0$.

The restriction of your principle to m∈{0,1} amounts to $Σ^1_1$ Separation and thus already equivalent to $\text{ATR}_0$ (Theorem V.5.1 in Simpson's SOSOA 2nd ed).

To see that the full principle is also provable in $\text{ATR}_0$, let $Z$ denote the parameters of $φ$ not shown. For each $Π^1_1(Z)$ statement, assign an ordinal by converting the statement to well-foundness of a $Z$-recursive order, and taking its ordinal, and using $∞$ for false statements. Let $α_{n,m}$ be the ordinal for $∀X \, φ(X,n,m)$, and $α_n=\min_m(α_{n,m})$, and $α=\sup(α_n)$. $α$ exists because we can concatenate $X$-recursive well-orderings exceeding $α_n$ (which we get uniformly), and get an upper bound on $α$. Finally, a desired $g$ exists in $L_{α+1}(Z)$ (and is hyperarithmetic in $Z$). This is because $L_{α+1}(Z)$ contains the set of all $Π^1_1(Z)$ statements whose ordinals are $≤α$, along with their assigned ordinals.

From the upper bound version to $\text{ATR}_0$

For the choice principle weakened to only give upper bounds, we first derive $\text{ACA}_0$ by using it (for every $Z$) to give bounds for true $Σ^0_1(Z)$ statements, and thus computing the Turing jump of $Z$. Next, let '$≺$' be a $Z$-recursive well-ordering. It suffices to show that, starting at $Z$, the Turing jump can be iterated along $≺$.

Let $φ(X,n,m)$ be "decode $n$ as $(a,e)$; if $X$ encodes an iteration of the Turing jump (starting at $Z$) for the restriction of $≺$ below $a$, and Turing machine $e$ with oracle $(Z,X)$ halts, then it halts in $≤m$ steps". Such an $m$ exists (i.e. $∀n ∃m ∀X \, φ(X,n,m)$) because otherwise we would get conflicting arithmetic transfinite recursions for an initial segment of $≺$, which we can then compare (in $\text{ACA}_0$) to get an infinite $≺$-descending sequence.

Let $g$ be as in the principle. Then the iterated Turing jump is computable from $Z,g$ by converting transfinite recursion into bounded recursion using $g$. (By weak Kőnig's lemma, a failure of the bounded recursion to terminate would give an infinite $≺$-descending path.) Next, if there are no inconsistencies below $a$, then the Turing jump can be iterated from $Z$ along $≺$ up to $a$ (uniquely, per above), and thus no inconsistencies at $a$ either. Thus, each inconsistency gives a $≺$-lower inconsistency, and since an inconsistency is an arithmetic property, an infinite $≺$-descending sequence.

Answer 2

For intuitionistic logic there is a technique for showing conservativity of countable choice, originally due to Goodman in Relativized Realizability in Intuitionistic Arithmetic of All Finite Types. The original result shows that $\mathbf{HA}^\omega + \mathbf{AC_{\mathbb{N},\mathbb{N}}}$ is conservative over $\mathbf{HA}$ for all arithmetic formulas, so in particular has the same consistency strength. Here $\mathbf{HA}^\omega$ is higher order in the sense that it has a type of natural numbers and a type of functions $\sigma \to \tau$ for all types $\sigma, \tau$.

Beeson showed we can break the model into 2-steps as a realizability model inside a forcing model in Goodman's theorem and beyond, and in the same paper he generalised from $\mathbf{HA}$ to second order $\mathbf{HA}$ (i.e. $\mathbf{HA}$ with sets of numbers with full comprehension). If you just want to bound consistency strength, without getting conservativity for all arithmetic formulas, you can also just use realizability directly.

There are some other later variants of this result in topos theory and set theory, but that is getting quite far from second order arithmetic (see e.g. https://etheses.whiterose.ac.uk/1439/).