2.1.2 The base theory of higher-order Reverse Mathematics.

We introduce Kohlenbach’s base theory ${\mathsf {RCA}}_{0}^{\omega }$ , first introduced in [Reference Kohlenbach61, Section 2].

Note that variables (of any finite type) are allowed in quantifier-free formulas of the language ${\mathsf {L}}_{\omega }$ : only quantifiers are banned. Recursion as in (2.2) is called primitive recursion; the class of functionals obtained from $\mathbf {R}_{\rho }$ for all $\rho \in \mathbf {T}$ is called Gödel’s system T of all (higher-order) primitive recursive functionals.

Definition 2.2. The axiom ${\mathsf {QF\text{-}AC}}$ consists of the following for all $\sigma , \tau \in \textbf {T}$ :

(QF–ACσ,τ) $$\begin{align} (\forall x^{\sigma})(\exists y^{\tau})A(x, y)\rightarrow (\exists Y^{\sigma\rightarrow \tau})(\forall x^{\sigma})A(x, Y(x)), \end{align}$$

for any quantifier-free formula A in the language of ${\mathsf {L}}_{\omega }$ .

As discussed in [Reference Kohlenbach61, Section 2], ${\mathsf {RCA}}_{0}^{\omega }$ and ${\mathsf {RCA}}_{0}$ prove the same sentences ‘up to language’ as the latter is set-based and the former function-based. This conservation results is obtained via the so-called ${\mathsf {ECF}}$ -interpretation, which we now discuss.

In light of the widespread use of codes in RM and the common practice of identifying codes with the objects being coded, it is no exaggeration to refer to ${\mathsf {ECF}}$ as the canonical embedding of higher-order into second-order arithmetic.

Finally as noted above, Theorem 1.1 is provable in the base theory.

2.1.3 Notations and the like.

We introduce the usual notations for common mathematical notions, like real numbers, as also introduced in [Reference Kohlenbach61].

For completeness, we list the following notational convention for finite sequences.

2.1.4 Some axioms and functionals.

As noted in Section 1, the logical hardness of a theorem is measured via what fragment of the comprehension axiom is needed for a proof. For this reason, we introduce some axioms and functionals related to higher-order comprehension in this section. We are mostly dealing with conventional comprehension here, i.e., only parameters over ${\mathbb N}$ and ${\mathbb N}^{{\mathbb N}}$ are allowed in formula classes like $\Pi _{k}^{1}$ and $\Sigma _{k}^{1}$ .

First of all, the following functional is clearly discontinuous at $f=11\dots $ ; in fact, $(\exists ^{2})$ is equivalent to the existence of $F:{\mathbb R}\rightarrow {\mathbb R}$ such that $F(x)=1$ if $x>_{{\mathbb R}}0$ , and $0$ otherwise [Reference Kohlenbach61, Section 3]. This fact shall be repeated often.

(∃2) $$\begin{align} (\exists \varphi^{2}\leq_{2}1)(\forall f^{1})\big[(\exists n)(f(n)=0) \leftrightarrow \varphi(f)=0 \big]. \end{align}$$

Related to $(\exists ^{2})$ , the functional $\mu ^{2}$ in $(\mu ^{2})$ is also called Feferman’s $\mu $ [Reference Avigad and Feferman3].

(μ2) $$\begin{align} (\exists \mu^{2})(\forall f^{1})\big[ (\exists n)(f(n)=0) \rightarrow [f(\mu(f))=0&\wedge (\forall i<\mu(f))(f(i)\ne 0) ]\\ & \wedge [ (\forall n)(f(n)\ne0)\rightarrow \mu(f)=0] \big]. \notag \end{align}$$

We have $(\exists ^{2})\leftrightarrow (\mu ^{2})$ over ${\mathsf {RCA}}_{0}^{\omega }$ and ${\mathsf {ACA}}_{0}^{\omega }\equiv {\mathsf {RCA}}_{0}^{\omega }+(\exists ^{2})$ proves the same sentences as ${\mathsf {ACA}}_{0}$ by [Reference Hunter52, Theorem 2.5].

Secondly, the functional ${\mathsf {S}}^{2}$ in $({\mathsf {S}}^{2})$ is called the Suslin functional [Reference Kohlenbach61].

(S2) $$\begin{align}(\exists{\mathsf{S}}^{2}\leq_{2}1)(\forall f^{1})\big[ (\exists g^{1})(\forall n^{0})(f(\overline{g}n)=0)\leftrightarrow {\mathsf{S}}(f)=0 \big]. \end{align}$$

The system $\Pi _{1}^{1}\text {-}\textsf {CA}_{0}^{\omega }\equiv {\mathsf {RCA}}_{0}^{\omega }+({\mathsf {S}}^{2})$ proves the same $\Pi _{3}^{1}$ -sentences as $\Pi _{1}^{1}\text {-}\textsf {CA}_{0}$ by [Reference Sakamoto and Yamazaki97, Theorem 2.2]. By definition, the Suslin functional ${\mathsf {S}}^{2}$ can decide whether a $\Sigma _{1}^{1}$ -formula as in the left-hand side of $({\mathsf {S}}^{2})$ is true or false. We similarly define the functional ${\mathsf {S}}_{k}^{2}$ which decides the truth or falsity of $\Sigma _{k}^{1}$ -formulas from ${\mathsf {L}}_{2}$ ; we also define the system $\Pi _{k}^{1}\text {-}\textsf {CA}_{0}^{\omega }$ as ${\mathsf {RCA}}_{0}^{\omega }+({\mathsf {S}}_{k}^{2})$ , where $({\mathsf {S}}_{k}^{2})$ expresses that ${\mathsf {S}}_{k}^{2}$ exists. We note that the operators $\nu _{n}$ from [Reference Buchholz, Feferman, Pohlers and Sieg16, p. 129] are essentially ${\mathsf {S}}_{n}^{2}$ strengthened to return a witness (if existant) to the $\Sigma _{n}^{1}$ -formula at hand.

Thirdly, full second-order arithmetic ${\mathsf {Z}}_{2}$ is readily derived from $\cup _{k}\Pi _{k}^{1}\text {-}\textsf {CA}_{0}^{\omega }$ , or from

(∃3) $$\begin{align} (\exists E^{3}\leq_{3}1)(\forall Y^{2})\big[ (\exists f^{1})(Y(f)=0)\leftrightarrow E(Y)=0 \big], \end{align}$$

and we therefore define ${\mathsf {Z}}_{2}^{\varOmega }\equiv {\mathsf {RCA}}_{0}^{\omega }+(\exists ^{3})$ and ${\mathsf {Z}}_{2}^{\omega }\equiv \cup _{k}\Pi _{k}^{1}\text {-}\textsf {CA}_{0}^{\omega }$ , which are conservative over ${\mathsf {Z}}_{2}$ by [Reference Hunter52, Corollary 2.6]. Despite this close connection, ${\mathsf {Z}}_{2}^{\omega }$ and ${\mathsf {Z}}_{2}^{\varOmega }$ can behave quite differently, as discussed in, e.g., [Reference Normann and Sanders86, Section 2.2]. The functional from $(\exists ^{3})$ is also called ‘ $\exists ^{3}$ ’, and we use the same convention for other functionals.

Fourth, the Heine–Borel theorem states the existence of a finite sub-covering for an open covering of certain spaces. Now, a functional $\Psi :{\mathbb R}\rightarrow {\mathbb R}^{+}$ gives rise to a canonical cover  $\cup _{x\in I} I_{x}^{\Psi }$ for $I\equiv [0,1]$ , where $I_{x}^{\Psi }$ is the open interval $(x-\Psi (x), x+\Psi (x))$ . Hence, the uncountable covering $\cup _{x\in I} I_{x}^{\Psi }$ has a finite sub-covering by the Heine–Borel theorem; in symbols:

Note that ${\mathsf {HBU}}$ is almost verbatim Cousin’s lemma (see [Reference Cousin25, p. 22]), i.e., the Heine–Borel theorem restricted to canonical covers. This restriction does not make a difference, as studied in [Reference Sanders100]. Let ${\mathsf {WHBU}}$ be the following weakening of ${\mathsf {HBU}}$ :

Note that ${\mathsf {WHBU}}$ expresses the essence of the Vitali covering theorem for uncountable coverings; Vitali already considered the latter in [Reference Vitali125]. By [Reference Normann and Sanders86, Reference Normann and Sanders88, Reference Normann and Sanders91], ${\mathsf {Z}}_{2}^{\varOmega }$ proves ${\mathsf {HBU}}$ and ${\mathsf {WHBU}}$ but ${\mathsf {Z}}_{2}^{\omega }+{\mathsf {QF\text{-}AC}}^{0,1}$ cannot. Basic properties of the gauge integral [Reference Muldowney77, Reference Swartz115] are equivalent to ${\mathsf {HBU}}$ while ${\mathsf {WHBU}}$ is equivalent to basic properties of the Lebesgue integral (without RM-codes [Reference Normann and Sanders91]).

We note that ${\mathsf {HBU}}$ (resp. ${\mathsf {WHBU}}$ ) is the higher-order counterpart of ${\mathsf {WKL}}$ (resp. ${\mathsf {WWKL}}$ ), i.e., weak König’s lemma (resp. weak weak König’s lemma) from [Reference Simpson108, Secs. IV and X] as ${\mathsf {ECF}}$ maps ${\mathsf {HBU}}$ (resp. ${\mathsf {WHBU}}$ ) to ${\mathsf {WKL}}$ (resp. ${\mathsf {WWKL}}$ ), i.e., these are (intuitively) weak principles.

Finally, the aforementioned results suggest that (higher-order) comprehension as in $\Pi _{k}^{1}\text {-}\textsf {CA}_{0}^{\omega }$ is not the right way of measuring the strength of ${\mathsf {HBU}}$ . As a better alternative, we have introduced the following axiom in [Reference Sanders98].

By [Reference Sanders98, Section 3], ${\mathsf {BOOT}}$ is equivalent to convergence theorems for nets, we have the implication ${\mathsf {BOOT}}\rightarrow {\mathsf {HBU}}$ , and ${\mathsf {RCA}}_{0}^{\omega }+{\mathsf {BOOT}}$ has the same first-order strength as ${\mathsf {ACA}}_{0}$ . Moreover, ${\mathsf {BOOT}}$ is a natural fragment of Feferman’s projection axiom  $\textsf {(Proj1)}$ from [Reference Feferman33]. Thus, ${\mathsf {BOOT}}$ is a natural axiom that provides a better ‘scale’ for measuring the strength of ${\mathsf {HBU}}$ and its ilk, as discussed in [Reference Sanders98] and Section 1.3.3.

2.2.2 Kleene’s computation schemes.

For those familiar with Turing computability, Kleene’s S1–S9 in a nutshell is as follows: the schemes S1–S8 merely introduce (higher-order) primitive recursion, while S9 essentially states that the recursion theorem holds. In this section we will provide a slightly more detailed introduction to Kleene computability. All further details can be found in [Reference Longley and Normann68, Section 5.1.4].

We note that $\mathsf {Tp}$ involves only total objects. As we will see, the Kleene schemes can be interpreted for all type structures. One of our applications of type structures is that they will serve as models for fragments of higher-order arithmetic, structures for the language ${\mathsf {L}}_{\omega }$ . While the Kleene schemes are defined for pure types, the language ${\mathsf {L}}_{\omega }$ is over a richer set of types, known as the finite types. However, assuming some modest closure properties of a type structure $ \mathsf {Tp}$ , the extension to the finite types is unique (see [Reference Longley and Normann68, Section 4.2]). This is the case when $\mathsf {Tp}$ is Kleene closed as in Definition 2.13.

The following main definition is [Reference Longley and Normann68, Definition 5.1.1] adjusted to a type structure $\mathsf {Tp}$ . We assume a standard sequence numbering over ${\mathbb N}$ : variables a, b, c, x, y, q, e, and d denote elements of ${\mathbb N}$ , while f, $g, \dots $ denote elements of $\mathsf {Tp}[1]$ . We let $\varPhi _{i}^{k_{i}}$ stand for an element of $\mathsf {Tp}[k_{i}]$ . The index ‘e’ in ( K ) serves as a Gödel number denoting the e-th Kleene algorithm. We use the notation ‘ $\{e\}_{{\mathsf {Tp}}}$ ’ if we need to specify the particular type structure $\mathsf {Tp}$ .

Definition 2.12 (Kleene S1–S9 schemes relative to ${\mathsf {Tp}}$ ).

Let ${\mathsf {Tp}} = \{\mathsf {Tp}[k]\}_{k \in {\mathbb N}}$ be a type structure. Over the latter, we define the relation

(K) $$ \begin{align} \{e\}(\varPhi_{0}^{k_{0}} , \ldots , \varPhi_{n-1}^{k_{n-1}}) = a \end{align} $$

by a monotone inductive definition as follows. We omit the upper indices for the types whenever they are clear from context.

1. S1 If $e = \langle 1 \rangle $ , then $\{e\}(x,\vec \varPhi ) = x+1$ .

2. S2 If $e = \langle 2,q\rangle $ , then $\{e\}(\vec \varPhi ) = q$ .

3. S3 If $e = \langle 3 \rangle $ , then $ \{e\}(x,\vec \varPhi ) = x$ .

4. S4 If $e = \langle 4 , e_{0} , e_{1}\rangle $ , then $\{e\}(\vec \varPhi ) = a$ if for some b we have that $\{e_{1}\}(\vec \varPhi ) = b$ and $\{e_{0}\}(b,\vec \varPhi ) = a$ .

5. S5 If $e = \langle 5 , e_{0} , e_{1} \rangle $ then

   • – $\{e\}(0, \vec \varPhi ) = a$ if $\{e_{0}\}(\vec \varPhi ) = a$ ,

   • – $\{e\}(x+1 , \vec \varPhi ) = a$ if there is some b such that $\{e\}(x,\vec \varPhi ) = b$ and $\{e_{1}\}(b, \vec \varPhi ) = a$ .

6. S6 If $e = \langle 6 , d , \pi (0) , \ldots , \pi (n-1)\rangle $ , where $\pi $ is a permutation of $\{0 , \ldots , n-1\}$ , then $\{e\}(\varPhi _{0} , \ldots , \varPhi _{n-1}) = a$ if $\{d\}(\varPhi _{\pi (0)} , \ldots , \varPhi _{\pi (n-1)}) = a$ .

7. S7 If $e = \langle 7 \rangle $ , then $\{e\}(f,x,\vec \varPhi ) = f(x)$ .

8. S8 If $e = \langle 8, d\rangle $ , then $\{e\}(\varPhi ^{k+2}, \vec \varPhi ) = a$ if there is a $\phi ^{k+1} \in \mathsf {Tp}[k+1]$ such that $\varPhi (\phi ) = a$ and for all $\xi ^{k} \in \mathsf {Tp}[k]$ we have that $\{d\}(\varPhi , \xi , \vec \varPhi ) = \phi (\xi )$ .

9. S9 If $e = \langle 9,m+1\rangle $ and $m \leq n$ , $\{e\}(d,\varPhi _{0} , \ldots , \varPhi _{n}) = a$ if $\{d\}(\varPhi _{0} , \ldots , \varPhi _{m}) = a$ .

Intuitively speaking, $\{e\}(\vec \varPhi ) = a$ represents the result of a terminating computation, where S1–S3 and S7 provide us with the initial computation, S4 is composition, S5 represents primitive recursion, and S6 represents permutations of arguments. Finally, S8 represents higher-order-composition with two requirements: that the computation of $\{d\}(\varPhi , \xi , \vec \varPhi )$ must terminate for all $\xi \in \mathsf {Tp}[k]$ and that the functional $\phi $ thus computed must be an element of $\mathsf {Tp}[k+1]$ . In the original definition from [Reference Kleene58], the schemes are interpreted over the maximal type structure and the latter requirement is vacuous. This requirement is essential to our development, as will become clear below.

When a type structure ${\mathsf {Tp}}$ is Kleene closed, it will have a canonical extension to an interpretation $\mathsf {Tp}[\sigma ]$ for all finite types $\sigma $ as in the language ${\mathsf {L}}_{\omega }$ . This is folklore and is discussed at length in [Reference Longley and Normann68, Section 4.2]. We use ${\mathsf {Tp}}^{*}$ to denote this unique extension. What is important to us is that if ${\mathsf {Tp}}$ is Kleene closed, then ${\mathsf {Tp}}^{*}$ is a model of ${\mathsf {RCA}}_{0}^{\omega }$ and all terms in Gödel’s T have canonical interpretations in ${\mathsf {Tp}}^{*}$ .

Finally, we motivate our choice of framework as follows.

In the next sections, we discuss some aspects of Kleene computability essential to this paper while foregoing a full introduction. For instance, we will not prove that being computable in is transitive, while we freely use this fact.

2.2.3 Basic results in Kleene computability theory.

We discuss two folklore results (Lemmas 2.15 and 2.16) and one important theorem (Theorem 2.17).

As to the first folklore result, since the relation $\{e\}(\vec \varPhi ) = a$ is defined by a positive inductive definition, all such computation tuples $\langle e , \vec \varPhi , a \rangle $ will either stem from one of the schemes S1, S2, S3, or S7, or there will be a unique base of other such computation tuples. The elements of this base are called the immediate sub-computations and the transitive closure of this relation gives us the well-founded relation of being a sub-computation. The ordinal rank of a terminating computation is, by definition, the rank of the corresponding computation tuple in this well-founded relation. The list of arguments in a sub-computation may contain more objects, but as they are only added through the use of S8, they will only be two type levels (or more) below the maximal type in the original list. In particular this means that if all arguments in a computation $\{e\}(\vec \varPhi ) = a$ are of type 2 or lower, all extra arguments in the sub-computations will be integers. This further means that in a computation like this, say of the form $\{e\}(\vec F , \vec f , \vec a) = b$ , where each $F_{i}$ is of type 2, whenever we use the value $F_{i}(g)$ in a sub-computation based on S8, g itself will be computable in the argument list. For the sake of notational simplicity, we often order the arguments of a computation according to their types.

Lemma 2.15 (Restriction).

Let $A \subseteq {\mathbb N}^{\mathbb N}$ and consider $F:{\mathbb N}^{\mathbb N} \rightarrow {\mathbb N}$ with its restriction to A denoted $F_{A}$ . If all f computable in F and elements in A are in A, then for all indices e, for all $\vec f$ from A and all $\vec a$ we have that

$$ \begin{align*}\{e\}(F,\vec f , \vec a) \simeq \{e\}(F_{A} , \vec f , \vec a)\end{align*} $$

where ‘ $\simeq $ ’ is the Kleene-equality: both sides are either undefined or both sides are defined and equal.

We also have the following lemma, combining the observation of Lemma 2.15 with the transitivity of the relation computable in.

As to the second folklore result, the following theorem shows that we have a high degree of flexibility when defining type structures from sets of functionals.

The fan functional is a non-normal object computing a modulus of uniform continuity for continuous inputs [Reference Longley and Normann68, Section 8.3].

All elements in $\mathsf {Tp}[2]$ in the proof are continuous with an associate in $\mathsf {Tp}[1]$ . Moreover, there is a Kleene closed type structure ${\mathsf {Tp}}^{\prime }$ containing all of ${\mathbb N}^{\mathbb N}$ , but not the fan functional, by the same argument. In this case, $\mathsf {Tp}^{\prime }[2]$ are exactly the continuous functionals, implying that the fan functional is total, but not in $\mathsf {Tp}^{\prime }[3]$ .

2.2.4 Advanced Kleene computability theory.

We discuss Gandy selection, a technique expressing that Kleene computability satisfies a kind of ‘computable Axiom of Choice’. This technique is based on stage comparison, discussed next.

Now, given a type structure ${\mathsf {Tp}}$ , Kleene computations are defined by a positive inductive definition and the set of computations $\{e\}(\vec \varPhi ) = a$ are equipped with ordinal ranks. For the latter, we refer to [Reference Longley and Normann68, Section 5.1.1] and the first folklore result in Section 2.2.3. Moreover, if the elements of $\vec \varPhi $ have types $\leq 2$ , this ordinal rank is countable, which holds for any Kleene closed type structure.

Recall the functional ∃² introduced in Section 2.1.4. A functional F of type 2 is called normal if $\exists ^{2}$ is computable in F, a definition that works for all Kleene closed type structures. If F is normal, we can use $\exists ^{2}$ and the recursion theorem to prove the following theorem, originally due to Gandy [Reference Gandy38].

A ‘soft’ consequence of stage comparison is Gandy selection, first proved in [Reference Gandy38]. We only state the version we need in this paper. Intuitively, $\lambda f.\{d\}(F, f)$ is a (partial) choice function with the biggest possible domain.

Most of our applications of Gandy selection are based on the following corollary. Intuitively speaking, the functional G computes an F-index for f.

Note that the functional G is always injective. Of course, these results are equally valid for all Kleene closed type structures, and we may replace ${\mathbb N}^{\mathbb N}$ in Theorem 2.21 with any finite product of ${\mathbb N}$ and ${\mathbb N}^{\mathbb N}$ .

2.2.5 Two type structures.

In this section, we define two Kleene closed type structures $\mathbf {P}$ and $\bf Q$ that are crucial for the below independence results involving ${\mathsf {Z}}_{2}^{\omega }$ . Moreover, the construction of $\mathbf {Q}$ unifies constructions from earlier work that were used to prove, e.g., [Reference Normann and Sanders84, Theorem 3.4], [Reference Normann and Sanders88, Theorem 4.9], and [Reference Normann and Sanders87, Theorem 3.5].

We note that $\mathbf {P}$ is constructed under the set-theoretical assumption that $\textsf {V = L}$ . There is no harm in this, since what is of interest is the logic of the structure, which statements are true and which are false, and our results will not depend on the assumption that $\textsf {V = L}$ ; they are proved within ${\mathsf {ZF}}$ . For the unfamiliar reader, the axiom $\textsf {V = L}$ , which expresses that every set is constructible, was used by Gödel to show that the Continuum Hypothesis is consistent with ${\mathsf {ZFC}}$ (see [Reference Devlin27] for details).

Recall the functionals ${\mathsf {S}}^{2}_{k}$ from Section 2.1.4. We use the assumption $\textsf {V = L}$ motivated by the following fact from set theory.

The model $\mathbf {P}$ , under another name, has been used to prove [Reference Normann and Sanders88, Theorem 4.3]. Recall the unique extension ${\mathsf {Tp}}^{*}$ of ${\mathsf {Tp}}$ introduced below Definition 2.13.

Proof We assume that $\textsf {V = L}$ , which implies that all $\Pi ^{1}_{n}$ -formulas are absolute for $\mathbf {P}[1]$ . Since $\mathbf {P}[1]$ is closed under computability relative to each ${\mathsf {S}}^{2}_{k}$ , we have that $\mathbf {P}[1]$ satisfies all $\Pi ^{1}_{n}$ -comprehension axioms. Now assume that $(\forall n^{0}) (\exists f^{1}) Q(n,f,\vec \varPhi )$ is true in $\mathbf {P}$ , where Q is quantifier-free and $\vec \varPhi $ is a list of parameters from $\mathbf {P}$ . Since all functionals in $\vec \varPhi $ are computable in ${\mathsf {S}}^{2}_{\omega }$ , the set

$$ \begin{align*} R=\{(n, e)\in {\mathbb N}^{2} : (\exists f^{1})[ Q(n,f,\vec \varPhi)\wedge (\forall a^{0})(f(a) = \{e\}({\mathsf{S}}_{2}^{\omega},a))] \} \end{align*} $$

is semi-computable in ${\mathsf {S}}^{2}_{\omega }$ . Moreover, we have that $(\forall n^{0}) (\exists e^{0})[(n,e) \in R]$ . By assumption and Gandy selection, there is a function g computable in ${\mathsf {S}}^{2}_{\omega }$ such that $R(n,g(n))$ for all $n^{0}$ . If $G(n)$ is the function f computed from ${\mathsf {S}}^{2}_{\omega }$ with index $g(n)$ , we have that $G^{0\rightarrow 1} \in \bf P$ witnesses this instance of quantifier-free choice.

For the rest of this section, we fix some notation. We let $A \subseteq {\mathbb N}^{\mathbb N}$ be a countable set such that all $\Pi ^{1}_{n}$ formulas are absolute for $(A, {\mathbb N}^{\mathbb N}) $ for all n. We let $A = \{g_{k} : k \in {\mathbb N}\}$ and we let $A_{k}$ be the set of functions computable in ${\mathsf {S}}^{2}_{k}$ and $g_{0} , \ldots , g_{k-1}$ . For the sake of unity, we put ${\mathsf {S}}^{2}_{0} = \exists ^{2}$ , so $A_{0}$ is the set of hyperarithmetical functions.

Proof This follows from the choice of A and the fact that the relation

$$ \begin{align*}\{e\}({\mathsf{S}}^{2}_{k} , g_{0} , \ldots , g_{k-1}, \vec a) = b\end{align*} $$

is $\Pi ^{1}_{k+1}$ (for $k> 0$ even $\Delta ^{1}_{k+1}$ ) and that ${\mathsf {S}}^{2}_{k+1}$ computes an enumeration of all functions computable in ${\mathsf {S}}^{2}_{k}$ relative to any fixed list of type 1 arguments.

Now fix $F:A \rightarrow {\mathbb N}$ . We intend to use Theorem 2.17 and let $F \in B_{0}$ if there is a $k_{0}$ such that for all $k \geq k_{0}$ , the restriction of F to $A_{k}$ is partially computable in ${\mathsf {S}}^{2}_{k}$ and $g_{0} , \ldots , g_{k-1}$ . Note that the join of finitely many functionals from $B_{0}$ is in $B_{0}$ .

Recall the unique extension ${\mathsf {Tp}}^{*}$ of ${\mathsf {Tp}}$ introduced below Definition 2.13. The type structure $\mathbf {Q}^{*}$ is then a model for ${\mathsf {Z}}_{2}^{\omega }$ since all $\Pi ^{1}_{k}$ -statements are absolute for A for all k. In the next section, we show that $\mathbf {Q}^{*}$ does not satisfy ${\mathsf {QF\text{-}AC}}^{0,1}$ , while we use $\bf Q$ to show that ${\mathsf {Z}}_{2}^{\omega }$ is consistent with $\neg {\mathsf {NBI}}$ (see Theorem 3.28).

3.2.1 Comprehension and ${\mathsf {NIN}}$ .

In this section, we show that ${\mathsf {NIN}}$ relates to comprehension as follows. Recall that ${\mathsf {Z}}_{2}^{\omega }$ and ${\mathsf {Z}}_{2}^{\varOmega }$ are conservative extensions of ${\mathsf {Z}}_{2}$ .

Proof For the negative result, we use the model $\mathbf {P}$ from Definition 2.24. This model satisfies ${\mathsf {Z}}_{2}^{\omega } + {\mathsf {QF\text{-}AC}}^{0,1}$ . We observe that $\mathbf {P}[2]$ contains a functional $G:A \rightarrow {\mathbb N}$ that is injective, which is a direct consequence of Corollary 2.22 using ${\mathsf {S}}^{2}_{\omega }$ for F.

For the positive result, fix $Y:[0,1]\rightarrow {\mathbb N}$ and consider the following formula, which is trivial under classical logic:

(3.1) $$ \begin{align} (\forall n\in {\mathbb N})(\exists y\in [0,1])\big[ (\exists x\in [0,1])(Y(x)=n)\rightarrow Y(y)=n \big]. \end{align} $$

Note that ${\mathsf {QF\text{-}AC}}^{0,1}$ applies to (3.1) (modulo $\exists ^{3}$ ) and let $\varPhi ^{0\rightarrow 1}$ be the resulting sequence, which obviously lists the range of Y. Using [Reference Simpson108, Sec. II.4.9], let $y\in [0,1]$ be a real number such that $y\ne _{{\mathbb R}}\varPhi (n)$ for all $n\in {\mathbb N}$ . For $n_{0}:=Y(y)$ , we have $y\ne _{{\mathbb R}} \varPhi (n_{0})$ while $Y(y)=n_{0}=Y(\varPhi (n_{0}))$ , i.e., ${\mathsf {NIN}}$ follows.

An elementary argument allows us to replace $(\exists ^{3})$ by ${\mathsf {BOOT}}$ and restrict to the Axiom of unique Choice in the previous, but we obtain a much sharper proof in Theorem 3.4; the theorem holds if we restrict ${\mathsf {NIN}}$ to measurable functionals. The proof also establishes that the Axiom of Countable Choice suffices to prove ${\mathsf {NIN}}$ , while the same holds for (many?) other fragments, like HR35 and HR38 from [Reference Howard and Rubin50].

We finish this section with a remark on the (very recent) RM of ${\mathsf {NIN}}$ .

3.2.2 Ordinary mathematics and ${\mathsf {NIN}}$ .

In this section, we derive ${\mathsf {NIN}}$ from weakFootnote ⁸ theorems of ordinary mathematics, including Arzelà’s convergence theorem ${\mathsf {Arz}}$ . We also note that countable choice as in ${\mathsf {QF\text{-}AC}}^{0,1}$ is not needed to prove ${\mathsf {NIN}}$ .

Let ${\mathsf {BCT}}$ be the Baire category theorem for open sets given by characteristic functions as in [Reference Normann and Sanders87, Section 6]. The following proof still goes through if we further restrict ${\mathsf {BCT}}$ to open sets with at most finitely many isolated points in the complement.

We note that the Heine–Borel and Vitali theorems for countable coverings similarly imply ${\mathsf {NIN}}$ , as shown in Section 3.2.4. Since ${\mathsf {BCT}}$ for open sets given as countable unions (aka RM-codes) is provable in ${\mathsf {RCA}}_{0}$ ([Reference Simpson108, Sec. II.4.10]), ${\mathsf {NIN}}$ also follows from the ‘coding principle’ that expresses that a sequence of open sets given by characteristic functions as in [Reference Normann and Sanders87, Section 6] can be expressed as a sequence of RM-codes of open sets. Moreover, the second part of this proof can be combined with Lemma 2.16 to yield a simpler proof of [Reference Normann and Sanders87, Theorem 6.6] as done in Theorem 4.4.

As noted above and in [Reference Normann and Sanders91], ${\mathsf {WHBU}}$ constitutes the combinatorial essence of the Vitali covering theorem. The former is equivalent to fundamental properties of the Lebesgue measure, like countable additivity, over a slight extension of ${\mathsf {RCA}}_{0}^{\omega }$ to accommodate basic measure theory [Reference Normann and Sanders91]. In Section 6, we list some very basic properties of the Lebesgue measure and integral that imply ${\mathsf {NIN}}$ . A much more basic ‘integral’ theorem that implies ${\mathsf {NIN}}$ is provided by Arzelà’s convergence theorem for the Riemann integral, first published in 1885 [Reference Arzelà2] and discussed in (historical) detail in [Reference Hawkins46, Reference Luxemburg70]. The proof in [Reference Thomson119] readily yields ${\mathsf {Arz}}$ in ${\mathsf {Z}}_{2}^{\varOmega }$ , using ${\mathsf {HBU}}$ , while Yokoyama studies ${\mathsf {Arz}}$ for continuous functions in second-order RM in [Reference Yokoyama128, Theorem 3.33].

As is clear from its proof, the following theorem does not change if we require a modulus of convergence for $\lim _{n\rightarrow \infty }f_{n}=f$ , (universal) moduli of Riemann integrability, or if we assume the sequence $\lambda n.\int _{0}^{1}f_{n}(x)dx$ to be given.

The following theorems yield ${\mathsf {NIN}}$ in the same way as for ${\mathsf {Arz}}$ in the previous proof:

• • Arzelà’s lemma, called ‘Theorem B’ in [Reference Luxemburg70] and ‘item 2’ in [Reference Gordon40, Theorem 4].

• • Luxemburg’s Fatou’s lemma for the Riemann integral as in [Reference Luxemburg70, p. 977].

• • Thomson’s monotone convergence theorem for the Riemann integral [Reference Thomson119].

• • The Carslaw and Young term-by-term Riemann integration theorems (see [Reference Carslaw22, Theorem II] and [Reference Young129]).

• • Kestelman’s Cauchy–Riemann convergence theorem [Reference Kestelman56, Theorem 2].

• • The above formulated using ‘continuous almost everywhere and bounded’ by Lebesgue’s criterion for Riemann integrability (see also Section 3.2.4).

• • Helly’s convergence theorem for the Stieltjes integral [Reference Helly47, VIII, p. 288].

As discussed in [Reference Hawkins46, Section 4.4] in the context of Fourier series, Ascoli, Dini, and du Bois Reymond already made use of term-by-term integration for the Riemann integral involving discontinuous functions as early as 1874. Moreover, if one requires in Helly’s selection theorem that the sub-sequence exhibits pointwise convergence (like in the original [Reference Helly47, VII, p. 283]) and  $L_{1}$ -convergence (like in HST in [Reference Kreuzer65]), then this version, which can be found in, e.g., [Reference Barbu and Precupanu6], implies ${\mathsf {NIN}}$ in the same way as in the theorem. By contrast, Helly’s selection theorem involving codes (called $\textsf {HST}$ in [Reference Kreuzer65]) is equivalent to ${\mathsf {ACA}}_{0}$ .

The previous theorem has a rather remarkable corollary. Indeed, Tao’s notion of metastability generally has nicerFootnote ⁹ logical/computational properties than ‘usual’ convergence to a limit [Reference Kohlenbach62, Reference Tao116]. The situation is rather different for ${\mathsf {Arz}}$ .

Proof Let $Y:[0,1]\rightarrow {\mathbb N}$ be an injection and let $g_{i}(x)$ and $f(x)$ be as in the proof of the theorem. Now define $f_{n}(x)$ as follows:

$$ \begin{align*} f_{2n+1}(x):= \!\begin{cases} 1, & 0\leq x\leq \frac{1}{4},\\ \sum_{i=0}^{2n+1} g_{i}(x), & \textrm{otherwise}, \end{cases} \textrm{ and } f_{2n}(x):= \!\begin{cases} 1, & \frac{7}{8}\leq x\leq 1,\\ \sum_{i=0}^{2n} g_{i}(x), & \textrm{ otherwise}. \end{cases} \end{align*} $$

In the same way as in the proof of Theorem 3.6, we have $\lim _{n\rightarrow \infty }f_{n}=f$ (with a modulus of convergence), $\int _{0}^{1}f_{2n+1}(x)dx =\frac {1}{4}$ , and $\int _{0}^{1}f_{2n}(x)dx =\frac {1}{8}$ . Hence, any one of the conditions of the corollary leads to a contradiction, and ${\mathsf {NIN}}$ follows.

The previous proof goes through for g in the definition of metastability restricted to constant functions (see, e.g., [Reference Kohlenbach62, p. 499] for such results ‘in the wild’). Moreover, the above results have clear implications for the ‘coding practice’ of RM, which we shall however discuss elsewhere in detail.

Finally, on a conceptual note, a number of early critics (including Borel) of the Axiom of Choice actually implicitly used this axiom in their work (see [Reference Ferreirós34, p. 315]). A similar observation can be made for ${\mathsf {NBI}}$ and ${\mathsf {NIN}}$ as follows: around 1874, Weierstrass seems to have held the beliefFootnote ¹¹ that there cannot be essential differences between infinite sets (see [Reference Ferreirós34, p. 184]), although basic compactness results, pioneered in part by Weierstrass himself, imply the uncountability of ${\mathbb R}$ .

3.2.3 Metric spaces and ${\mathsf {NIN}}$ .

In this section, we derive ${\mathsf {NIN}}$ from a most basic separability property of metrics on the unit interval.

Now, the study of metric spaces in RM proceeds—unsurprisingly—via codes, namely a complete separable metric space is represented via a countable and dense subset ([Reference Simpson108, Sec. II.5.1]). It is then a natural question how hard it is to prove that this countable and dense subset exists for the original/non-coded metric spaces. We study the special case for metrics defined on the unit interval, as in Definition 3.8 and ${\mathsf {STS}}$ below, which implies ${\mathsf {NIN}}$ by Theorem 3.12.

We note that Definition 3.10 is used in constructive mathematics (see [Reference Troelstra and van Dalen122, Chapter 7, Definition 2.2]). Our notion of separability is also implied by total boundedness as used in RM (see [Reference Simpson108, Sec. III.2.3] or [Reference Brown14, p. 53]). According to Simpson [Reference Simpson108, p. 14], one cannot speak at all about non-separable spaces in ${\mathsf {L}}_{2}$ .

It should also be straightforward to derive ${\mathsf {NIN}}$ from the non-separability of, e.g., the sequence space $\ell ^{\infty }$ or the space $\textsf {BV}$ of functions of bounded variation.

3.2.4 Countable sets versus sets that are countable.

We derive ${\mathsf {NIN}}$ from basic theorems about countable sets where the latter has its usual meaning, namely Definition 3.14 taken from [Reference Kunen67]. Among others, we study the Lebesgue criterion for Riemann integrability for countable sets, as well as central theorems from RM concerning countable sets as in items (i)–(viii).

First of all, we use the usual definition of countable set, as follows. By item (h) in Definition 2.5, sets $A\subset {\mathbb R}$ are given by characteristic functions, as in [Reference Hunter52, Reference Kreuzer66, Reference Normann and Sanders87, Reference Normann and Sanders91].

This definition is from Kunen’s textbook on set theory [Reference Kunen67, p. 63]; we could additionally require that $Y:{\mathbb R}\rightarrow {\mathbb N}$ in Definition 3.14 is also surjective, as in, e.g., [Reference Hrbacek and Jech51]. This stronger notion is called ‘strongly countable’ (see Definition 3.32) and studied in Section 3.3. If we replace ‘countable’ by ‘strongly countable’, all the below proofs go through mutatis mutandis for ${\mathsf {NIN}}$ replaced by ${\mathsf {NBI}}$ .

Now, a cursory search reveals that the word ‘countable’ appears hundreds of times in the ‘bible’ of RM [Reference Simpson108]. Sections titles of [Reference Simpson108] also reveal that the objects of study are ‘countable’ rings, vector spaces, groups, et cetera. Of course, the above definition of ‘countable subset of ${\mathbb R}$ ’ cannot be expressed in ${\mathsf {L}}_{2}$ . Indeed, all the aforementioned objects are given by sequences in ${\mathsf {L}}_{2}$ (see also [Reference Simpson108, Sec. V.4.2]). Thus, the followingFootnote ¹² ‘coding principle’ ${\mathsf {cocode}}_{0}$ is crucial to RM if one wants the results in [Reference Simpson108] to have the same scope as third-order theorems about countable objects as in Definition 3.14. This is particularly true for the RM of topology from [Reference Mummert78–Reference Mummert and Simpson80], as this enterprise is based on countable bases at its very core.

Coding principles for continuous functionsFootnote ¹³ are used or studied in, e.g., [Reference Kohlenbach60, Reference Normann and Sanders87, Reference Sanders102]. As it happens, a version of ${\mathsf {cocode}}_{0}$ for representations has been studied in the context of Weihrauch reducibility in the form of List and wList from [Reference Kihara, Marcone and Pauly57, Section 6]. By Theorem 3.19, a lot of comprehension is needed to prove ${\mathsf {cocode}}_{0}$ , but then the latter is clearlyFootnote ¹⁴ non-normal. We also discuss the following basic theorems, which have fairly trivial proofs when formulated in ${\mathsf {L}}_{2}$ . Around 1885, Harnack proves the following in [Reference Harnack44, p. 243] (see [Reference Bressoud13, Reference Stillwell112, Reference Stillwell113] for a critical discussion).

Tao formulates a pigeon hole principle for measure spaces in [Reference Tao117, p. 91] and Principle 3.17 is a special case for $[0,1]$ . To ensure that the union in ${\mathsf {Pohm}}$ exists, we always assume $(\exists ^{2})$ . Note that ${\mathsf {Pohm}}$ is a special case of $\textsf {CUZ}$ from [Reference Normann and Sanders91].

Note that these principles can be formulated withoutFootnote ¹⁵ mentioning the Lebesgue measure, like was done for ${\mathsf {WHBU}}$ , and, e.g., by Harnack himself in [Reference Harnack44]. The following is a special case of the Lebesgue criterion for the Riemann integral; the latter was discovered before 1870 [Reference Hankel42, p. 92] with a correct proof in [Reference du Bois-Reymond11, Reference Dini30, Reference Harnack43]. Smith studies ${\mathsf {Lebesgue}}_{0}$ for a sequence of exceptional points in [Reference Smith110], motivated by [Reference Hankel42].

Now, the weakest comprehension principle that can prove ${\mathsf {cocode}}_{0}$ seems to be ${\mathsf {BOOT}}^{-}$ from [Reference Normann and Sanders87], which is a weakening of ${\mathsf {BOOT}}$ via the following extra condition:

$$ \begin{align*} (\forall n\in {\mathbb N})(\exists \textrm{ at most one } f\in {\mathbb N}^{{\mathbb N}})(Y(f, n)=0). \end{align*} $$

As discussed below, ${\mathsf {BOOT}}^{-}$ follows from basic theorems on open sets as in [Reference Normann and Sanders87].

Theorem 3.19. The system ${\mathsf {RCA}}_{0}^{\omega }+{\mathsf {WKL}}$ proves

(3.2) $$ \begin{align} {\mathsf{BOOT}}^{-}\rightarrow {\mathsf{cocode}}_{0}\rightarrow {\mathsf{Harnack}}_{0} \rightarrow{\mathsf{Lebesgue}}_{0}\rightarrow {\mathsf{NIN}} \end{align} $$

with ${\mathsf {WKL}}$ only used in the third implication $; {\mathsf {ACA}}_{0}^{\omega }$ proves ${\mathsf {Pohm}}\rightarrow {\mathsf {Harnack}}_{0}$ .

Proof We note that all principles in (3.2) (as well as ${\mathsf {Pohm}}$ and ${\mathsf {Harnack}}_{0}$ ) are outright provable in ${\mathsf {RCA}}_{0}^{\omega }+{\mathsf {WKL}}$ if all functions on ${\mathbb N}^{{\mathbb N}}$ and ${\mathbb R}$ are continuous. Since the latter is the case given $\neg (\exists ^{2})$ by [Reference Kohlenbach61, Section 3], we may assume $(\exists ^{2})$ for the rest of the proof. The functional $\exists ^{2}$ allows us to (uniformly) convert between real numbers and their binary or decimal representations, which we will tacitly do.

First of all, we show ${\mathsf {BOOT}}^{-}\rightarrow {\mathsf {NIN}}$ ; repeating the proof with $[0,1]$ replaced by countable $A\subset [0,1]$ , one obtains ${\mathsf {BOOT}}^{-}\rightarrow {\mathsf {cocode}}_{0}$ . Let $Y:[0,1]\rightarrow {\mathbb N}$ be an injection and use ${\mathsf {BOOT}}^{-}$ to define $X\subset {\mathbb N}^{2}\times {\mathbb Q}$ such that for all $n, m\in {\mathbb N}$ and $q\in {\mathbb Q}\cap [0,1]$ , we have

(3.3) $$ \begin{align}\textstyle (n, m, q)\in X\leftrightarrow (\exists x\in B(q, \frac{1}{2^{m}})\cap [0,1])(Y(x)= n ). \end{align} $$

Since Y is an injection, the following condition, required for ${\mathsf {BOOT}}^{-}$ , is satisfied:

$$ \begin{align*}\textstyle (\forall n, m\in {\mathbb N}, q\in {\mathbb Q}\cap [0,1])(\exists \textrm{ at most one } x\in B(q, \frac{1}{2^{m}})\cap [0,1])(Y(x)= n ). \end{align*} $$

We now use X from (3.3) and the well-known interval-halving technique to create a sequence $(x_{n})_{n\in {\mathbb N}}$ . For fixed $n\in {\mathbb N}$ , define $[x_{n}](0)$ as $0$ if $(\exists x\in [0, 1/2))(Y(x)=n)$ , and $1/2$ otherwise; define $[x_{n}](m+1)$ as $[x_{n}](m)$ if $(\exists x\in \big [[x_{n}](m), [x_{n}](m)+\frac {1}{2^{m+1}}\big )\big )(Y(x)=n)$ , and $[x_{n}](m)+\frac {1}{2^{m+1}}$ otherwise. By definition, we have

$$ \begin{align*} (\forall n\in {\mathbb N})\big[(\exists x\in [0,1])(Y(x)=n)\leftrightarrow Y(x_{n})=n \big]. \end{align*} $$

Now use [Reference Simpson108, Sec. II.4.9] to find $y_{0}\in [0,1]$ not in the sequence $(x_{n})_{n\in {\mathbb N}}$ . Then $n_{0}=Y(y_{0})$ yields a contradiction as $x_{n_{0}}\ne _{{\mathbb R}} y $ and $Y(y_{0})=n_{0}=Y(x_{n_{0}})$ .

Secondly, for the implication ${\mathsf {cocode}}_{0} \rightarrow {\mathsf {Harnack}}_{0}$ , given a countable set A and a sequence $(x_{n})_{n\in {\mathbb N}}$ listing its elements, consider $I_{n}:= (x_{n}-\frac {\varepsilon }{2^{n+2}}, x_{n}+\frac {\varepsilon }{2^{n+2}})$ , which are as required to show that A has measure $0$ .

Thirdly, for the implication $ {\mathsf {Harnack}}_{0}\rightarrow {\mathsf {Lebesgue}}_{0}$ , one uses (the proof of) [Reference Kohlenbach60, Proposition 4.7] to show that a function $f:[0,1]\rightarrow {\mathbb R}$ as in ${\mathsf {Lebesgue}}_{0}$ has a continuous modulus of continuity outside of A. This yields an open covering of $[0,1]\setminus A$ , while ${\mathsf {Harnack}}_{0}$ provides an open covering of A. Both coverings are given by sequences. The proof of [Reference Sanders and Yokoyama104, Theorem 10] is now readily adapted to yield that f is Riemann integrable, as required by ${\mathsf {Lebesgue}}_{0}$ .

Fourth, let $Y:[0,1]\rightarrow {\mathbb N}$ be an injection and note that $A\equiv [0,\frac {1}{2}]$ is countable by Definition 3.14. Define $f:[0,1]\rightarrow {\mathbb R}$ as $2$ if $x\in (\frac 12, 1]$ and the indicator function of ${\mathbb Q}$ otherwise. By ${\mathsf {Lebesgue}}_{0}$ , this function is Riemann integrable, a contradiction.

Fifth, assume ${\mathsf {Pohm}}$ and suppose $E\subset [0,1]$ is countable and not measure zero. For $Y:[0,1]\rightarrow {\mathbb N}$ an injection on E, define $E_{n}:=\{x\in E:Y(x)=n\}$ and let $n_{0}$ be such that $E_{n_{0}}$ has positive measure. By the definition of measure zero, there must be at least two distinct $x, y\in E_{n_{0}}$ , a contradiction as $Y(x)=n_{0}=Y(y)$ .

We now formulate a nice corollary involving ${\mathsf {cocode}}_{0}$ and its ilk restricted to closed sets as used in RM. Now, open sets are given in RM by unions $\cup _{n\in {\mathbb N}}(a_{n}, b_{n})$ [Reference Simpson108, Sec. II.5.6], while closed sets are complements thereof. We refer to such sets as ‘RM-open’ and ‘RM-closed’. By the following corollary, ${\mathsf {Z}}_{2}^{\omega }+{\mathsf {QF\text{-}AC}}^{0,1}$ cannot prove that countable RM-closed sets are given by a sequence.

One can show that ${\mathsf {Arz}}$ implies the restriction of ${\mathsf {Pohm}}$ to RM-closed sets, while the latter restriction makes elementhood for $A=\cup _{n\in {\mathbb N}}E_{n}$ in ${\mathsf {Pohm}}$ decidable.

One can push the previous corollary even further as follows: ${\mathsf {NIN}}$ follows from the statement an RM-closed and countable subset of  ${\mathbb R}$ has measure  $<+\infty $ . Other theorems that imply ${\mathsf {NIN}}$ in the same way are as follows, where ‘countable’ is always interpreted as in Definition 3.14:

1. (i) Heine–Borel theorem for countable collections of open intervals.

2. (ii) Vitali’s covering theorem for countable collections of open intervals.

3. (iii) Riemann integrable functions differing on countable sets have equal integral.

4. (iv) $|b-a|$ is the measure of: $[a,b]$ plus a countable set (cf. Footnote 3.2.4).

5. (v) Convergence theorems for nets in $[0,1]$ with countable index sets.

6. (vi) For a countable set, the Lebesgue integral of the indicator function is zero.

7. (vii) Ascoli–Arzelà theorem for countable sets of functions (see, e.g., [Reference Fréchet35]).

8. (viii) Bolzano–Weierstrass: a countable set in $[0,1]$ has a supremum.

9. (ix) Topology formulated with countable bases as in Example 6.5.

Regarding item (i), Borel in [Reference Borel12] uses ‘countable infinity of intervals’ and not ‘sequence of intervals’ in his formulationFootnote ¹⁶ of the Heine–Borel theorem. Vitali similarly talks about countable and uncountable ‘groups’ of intervals in [Reference Vitali125].

As a corollary to Theorem 3.4, we now derive ${\mathsf {NIN}}$ from item (i) as follows. The Heine–Borel theorem for different representations of open coverings is studied in RM [Reference Shafer105], i.e., the motivation for ${\mathsf {HBC}}_{0}$ is already present in second-order RM.

If ${\mathsf {BW}}_{0}$ denotes item (viii) above, the ‘usual’ proof yields ${\mathsf {BW}}_{0}\rightarrow {\mathsf {HBC}}_{0}$ , as expected. The following corollary is immediate and shows the limitations of ${\mathsf {L}}_{2}$ .

Finally, we study the RM of ${\mathsf {BW}}_{0}$ , ${\mathsf {HBC}}_{0}$ , etc. in [Reference Normann and Sanders90]. We do establish the aforementioned ‘explosion’ involving $\Pi _{2}^{1}\text {-}\textsf {CA}_{0}$ and the Bolzano–Weierstrass theorem (for countable sets) in the next section.

3.2.5 An explosive result.

In this section, we establish Theorem 3.25 which expresses that the Bolzano–Weierstrass theorem for countable sets in $2^{{\mathbb N}}$ , namely ${\mathsf {BW}}_{0}^{C}$ as in Definition 3.24, is highly explosive: it yields $\Pi _{2}^{1}\text {-}\textsf {CA}_{0}$ when combined with higher-order $\Pi _{1}^{1}\text {-}\textsf {CA}_{0}$ , i.e., the Suslin functional ${\mathsf {S}}^{2}$ .

First of all, we briefly motivate the importance of Theorem 3.25 as follows: the results in [Reference Normann and Sanders90–Reference Normann and Sanders93] establish equivalences between ${\mathsf {BW}}_{0}^{C}, {\mathsf {cocode}}_{0}$ , and the Jordan decomposition theorem over a suitable base theory. The latter theorem does not mention countable sets and has been classified at the level of ${\mathsf {ACA}}_{0}$ in second-order RM [Reference Kreuzer65, Reference Nies, Triplett and Yokoyama81], i.e., the third-order version behaves quite differently. We discuss the further implications of Theorem 3.25 in Remark 3.26 and the details of the formalisation of ${\mathsf {BW}}_{0}^{C}$ in Remark 3.27.

Secondly, we shall use the following version of the Bolzano–Weierstrass theorem.

Note that ${\mathsf {BW}}_{0}^{C}$ amounts to item (viii) for Cantor space and is provableFootnote ¹⁸ in a conservative extension of ${\mathsf {WKL}}_{0}$ . By contrast, over ${\mathsf {RCA}}_{0}^{\omega }$ , ${\mathsf {ACA}}_{0}$ is equivalent to the existence of $\sup _{n\in {\mathbb N}}F(f_{n})$ for sequences  $(f_{n})_{n\in {\mathbb N}}$ in $2^{{\mathbb N}}$ and any  $F:2^{{\mathbb N}}\rightarrow 2^{{\mathbb N}}$ (via the usual interval-halving proof). Nonetheless, ${\mathsf {BW}}_{0}^{C}$ is quite explosive when combined with the Suslin functional by the following theorem, a computational generalisationFootnote ¹⁹ of which may be found in Theorem 4.6.

Proof The proof consists of two steps: we first show that ${\mathsf {BW}}_{0}^{C}\rightarrow {\mathsf {BOOT}}^{-}_{C}$ and then show that $\Pi _{1}^{1}\text {-}\textsf {CA}_{0}^{\omega }+{\mathsf {BOOT}}^{-}_{C}$ proves $\Pi _{2}^{1}\text {-}\textsf {CA}_{0}$ . Here, ${\mathsf {BOOT}}^{-}_{C}$ is the statement that for all $Y^{2}$ such that $(\forall n^{0})(\exists \textrm {at most one } f\in 2^{{\mathbb N}})(Y(f, n)=0)$ , we have

(3.4) $$ \begin{align} (\exists X\subset {\mathbb N})(\forall n\in {\mathbb N})(n\in X\leftrightarrow (\exists g\in 2^{{\mathbb N}})(Y(g, n)=0)). \end{align} $$

Note that ${\mathsf {BOOT}}^{-}_{C}$ is essentially the restriction to C of ${\mathsf {BOOT}}^{\kern1pt-}$ .

First of all, let $Y^{2}$ be as in ${\mathsf {BOOT}}_{C}^{-}$ . Define $G(w^{1^{*}}, k^{0})$ as $1$ if we have $(\exists i<|w|)(Y(w(i), k)=0)$ , and $0$ otherwise. Define $f_{w}$ as $\lambda k.G(w, k)$ and define the set $A=\{ g\in 2^{{\mathbb N}} :(\exists k^{0})(Y(g, k)=0)\}$ . This set is countable via an obvious injection defined in terms of Y. The set $B=\{w^{1^{*}}: (\forall i<|w|)(w(i)\in A)\}$ is similarly countable, as follows by considering ${\mathbb r}$ from Definition 2.5. Modulo coding and $\exists ^{2}$ , B can be viewed as a subset of $2^{{\mathbb N}}$ . Define $F:2^{{\mathbb N}}\rightarrow 2^{{\mathbb N}}$ as $F(w):=f_{w}$ if $w\in B$ , and $00\dots $ otherwise. Let g be the supremum $\sup _{w\in B}F(w)$ and note that

$$ \begin{align*} (\forall n^{0})\big(g(n)=1\leftrightarrow (\exists f\in 2^{{\mathbb N}})(Y(f, n)=0)\big), \end{align*} $$

as required for ${\mathsf {BOOT}}^{-}_{C}$ and (3.4).

Secondly, to show that $\Pi _{1}^{1}\text {-}\textsf {CA}_{0}^{\omega }+{\mathsf {BOOT}}^{-}_{C}$ proves $\Pi _{2}^{1}\text {-}\textsf {CA}_{0}$ , we make use of the uniformisation result for  $\Pi _{1}^{1}$ -formulas, provable in $\Pi _{1}^{1}\text {-}\textsf {CA}_{0}$ (see [Reference Simpson108, Sec. VI.2]). As noted in [Reference Mummert and Simpson80, p. 530], for a $\Sigma _{2}^{1}$ -formula $(\exists X\subset {\mathbb N})\psi (n, X)$ in ${\mathsf {L}}_{2}$ , we may assume

(3.5) $$ \begin{align} (\forall n \in {\mathbb N})(\exists \textrm{ at most one } X\subset {\mathbb N})\psi(n, X) \end{align} $$

due to the aforementioned uniformisation result. Moreover, since $\psi (n, X)$ is $\Pi _{1}^{1}$ , we may assume it has the normal form $(\forall g^{1})(\exists m^{0})(f(\overline {g}m, \overline {X}m, n)=0)$ . In particular, the latter formula is decidable given ${\mathsf {S}}^{2}$ and (3.5) becomes $(\forall n^{0})(\exists \textrm {at most one } X\subset {\mathbb N})(Y( X, n)=0)$ where $Y(X, n)$ is $1-{\mathsf {S}}(\lambda \sigma ^{0^{*}}.f(\sigma , \overline {X}|\sigma |, n))$ . Applying ${\mathsf {BOOT}}^{-}_{C}$ , the set $\{n\in {\mathbb N}: (\exists X\subset {\mathbb N})(Y(X, n)=0) \}$ is exactly $\{ n\in {\mathbb N}: (\exists X\subset {\mathbb N})\psi (n, X)\}$ , and $\Pi _{2}^{1}\text {-}\textsf {CA}_{0}$ follows immediately.