Lifting Recursive Counterexamples to Higher-Order Arithmetic

Abstract

In classical computability theory, a recursive counterexample to a theorem shows that the latter does not hold when restricted to computable objects. These counterexamples are highly useful in the Reverse Mathematics program, where the aim of the latter is to determine the minimal axioms needed to prove a given theorem of ordinary mathematics. Indeed, recursive counterexamples often (help) establish the ‘reverse’ implication in the typical equivalence between said minimal axioms and the theorem at hand. The aforementioned is generally formulated in the language of second-order arithmetic and we show in this paper that recursive counterexamples are readily modified to provide similar implications in higher-order arithmetic. For instance, the higher-order analogue of ‘sequence’ is the topological notion of ‘net’, also known as ‘Moore-Smith sequence’. Our results on metric spaces suggest that the latter can only be reasonably studied in weak systems via representations (aka codes) in the language of second-order arithmetic.

1 Introduction

Computability theory has its roots in the seminal work of Turing, providing an intuitive notion of computation based on what we nowadays call Turing machines ([34]). Now, classical (resp. higher-order) computability theory deals with the computability of sets of natural numbers (resp. higher-order objects). In classical computability theory, a recursive counterexample to a theorem (formulated in an appropriate language) shows that the latter does not hold when restricted to computable sets. An historical overview may be found in the introduction of [7].

Recursive counterexamples are also highly useful in the Reverse Mathematics program (RM hereafter; see Sect. 2.1). Indeed, the aim of RM is to determine the minimal axioms needed to prove a given theorem of ordinary mathematics, often resulting in an equivalence between these axioms and the theorem; recursive counterexamples often (help) establish the ‘reverse’ implication from the theorem at hand to the minimal axioms (see e.g. [29, p. 1368] for this opinion).

As is well-known, both (classical) RM and classical recursion theory are (essentially) restricted to the language of second-order arithmetic, i.e. natural numbers and sets thereof. It is then a natural, if somewhat outlandish, question whether recursive counterexamples (and the associated implications in classical RM) yield any interesting results in higher-order RM and computability theory. In this paper, we show that recursive counterexamples are readily modified to provide interesting implications in higher-order arithmetic. We shall treat the following theorems: montone convergence theorem/Specker sequences (Sect. 3.1), compactness of metric spaces (Sect. 3.2), the Rado selection lemma (Sect. 3.3), and the ordering of fields (Sect. 3.4).

We shall work in Kohlenbach’s higher-order RM ([16]; see Sect. 2.1). We do not claim that the above results are always optimal or new; we even provide a counterexample in Sect. 3.1. Our aim is to show that with little modification recursive counterexamples, second-order as they may be, also establish results in higher-order arithmetic. As a bonus, our results pertaining to metric spaces suggest that the latter can only be reasonably studied in weak systems via representations (aka codes) in the language of second-order arithmetic.

Finally, the reader is welcome to their own interpretation of the aforementioned results, as long it accords with all the facts. In our opinion, one reasonable interpretation is that second- and higher-order arithmetic are not as different as sometimes claimed, and that recursive counterexamples and reversals provide a bridge of sorts between the two. However, the results in this paper do not support the argument that higher-order arithmetic contains ‘nothing new’ compared to second-order arithmetic, as discussed in detail in Sect. 4.2.

2 Preliminaries

We introduce Reverse Mathematics in Sect. 2.1, as well as its generalisation to higher-order arithmetic, and the associated base theory . We introduce some essential axioms in Sect. 2.2.

2.1 Reverse Mathematics

Reverse Mathematics is a program in the foundations of mathematics initiated around 1975 by Friedman ([8, 9]) and developed extensively by Simpson ([28]). The aim of RM is to identify the minimal axioms needed to prove theorems of ordinary, i.e. non-set theoretical, mathematics. In almost all cases, these minimal axioms are also equivalent to the theorem at hand (over a weak logical system). The reversal, i.e. the derivation of the minimal axioms from the theorem, is often proved based on recursive counterexample to the latter (see [29, p. 1368]).

We refer to [32] for an introduction to RM and to [28] for an overview of RM. We expect basic familiarity with RM, but do sketch some aspects of Kohlenbach’s higher-order RM ([16]) essential to this paper, including the base theory (Definition 1). As will become clear, the latter is officially a type theory but can accommodate (enough) set theory via Definition 4.

First of all, in contrast to ‘classical’ RM based on second-order arithmetic $\textsf {Z}_{2}$, higher-order RM uses $\textsf {L }_{\omega }$, the richer language of higher-order arithmetic. Indeed, while $\textsf {L }_{2}$, the language of $\textsf {Z}_{2}$, is restricted to natural numbers and sets of natural numbers, higher-order arithmetic can accommodate sets of sets of natural numbers, sets of sets of sets of natural numbers, et cetera. To formalise this idea, define the collection of all finite types $\mathbf {T}$ by the two clauses:

$$\begin{aligned} \text {(i) } 0\in \mathbf {T} \text { and (ii) if } \sigma , \tau \in \mathbf {T} \text { then }( \sigma \rightarrow \tau ) \in \mathbf {T}, \end{aligned}$$

where 0 is the type of natural numbers, and $\sigma \rightarrow \tau$ is the type of mappings from objects of type $\sigma$ to objects of type $\tau$. In this way, $1\equiv 0\rightarrow 0$ is the type of functions from numbers to numbers, and $n+1\equiv n\rightarrow 0$ maps type n objects to numbers. Viewing sets as characteristic functions, we note that $\textsf {Z}_{2}$ only includes objects of type 0 and 1.

Secondly, the language $\textsf {L }_{\omega }$ includes variables $x^{\rho }, y^{\rho }, z^{\rho },\dots$ of any finite type $\rho \in \mathbf {T}$. Types may be omitted when they can be inferred from context. The constants of $\textsf {L }_{\omega }$ include the type 0 objects 0, 1 and $<_{0}, +_{0}, \times _{0},=_{0}$ which are intended to have their usual meaning as operations on ${\mathbb N}$. Equality at higher types is defined in terms of ‘$=_{0}$’ as follows: for any objects $x^{\tau }, y^{\tau }$, we have

$$\begin{aligned}{}[x=_{\tau }y] \equiv (\forall z_{1}^{\tau _{1}}\dots z_{k}^{\tau _{k}})[xz_{1}\dots z_{k}=_{0}yz_{1}\dots z_{k}], \end{aligned}$$

(1)

if the type $\tau$ is composed as $\tau \equiv (\tau _{1}\rightarrow \dots \rightarrow \tau _{k}\rightarrow 0)$. Furthermore, $\textsf {L }_{\omega }$ includes the recursor constant $\mathbf {R}_{\sigma }$ for any $\sigma \in \mathbf {T}$, which allows for iteration on type $\sigma$-objects as in the special case (2). Formulas and terms are defined as usual.

Definition 1

The base theory consists of the following axioms.

• a. Basic axioms expressing that $0, 1, <_{0}, +_{0}, \times _{0}$ form an ordered semi-ring with equality $=_{0}$.

• b. Basic axioms defining the well-known $\varPi$ and $\varSigma$ combinators (aka K and S in [1]), which allow for the definition of $\lambda$-abstraction.

• c. The defining axiom of the recursor constant $\mathbf {R}_{0}$: For $m^{0}$ and $f^{1}$:

  $$\begin{aligned} \mathbf {R}_{0}(f, m, 0):= m \text { and } \mathbf {R}_{0}(f, m, n+1):= f(n, \mathbf {R}_{0}(f, m, n)). \end{aligned}$$

  (2)

• d. The axiom of extensionality: for all $\rho , \tau \in \mathbf {T}$, we have:

  

• e. The induction axiom for quantifier-free¹ formulas of $\textsf {L }_{\omega }$.

• f. $\textsf {QF}\text{- }\textsf {AC} ^{1,0}$: The quantifier-free Axiom of Choice as in Definition 2.

Definition 2

The axiom $\textsf {QF}\text{- }\textsf {AC}$ consists of the following for all $\sigma , \tau \in \mathbf T$:

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

We let $\textsf {IND}$ be the induction axiom for all formulas in $\textsf {L }_{\omega }$.

As discussed in [16, §2], and $\textsf {RCA} _{0}$ prove the same sentences ‘up to language’ as the latter is set-based and the former function-based. Recursion as in (2) is called primitive recursion; the class 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.

We use the usual notations for natural, rational, and real numbers, and the associated functions, as introduced in [16, pp. 288–289].

Definition 3

(Real numbers and related notions in ) 

• a. Natural numbers correspond to type zero objects, and we use ‘$n^{0}$’ and ‘$n\in {\mathbb N}$’ interchangeably. Rational numbers are defined as signed quotients of natural numbers, and ‘$q\in {\mathbb Q}$’ and ‘$<_{{\mathbb Q}}$’ have their usual meaning.

• b. Real numbers are coded by fast-converging Cauchy sequences $q_{(\cdot )}:{\mathbb N}\rightarrow {\mathbb Q}$, i.e. such that $(\forall n^{0}, i^{0})(|q_{n}-q_{n+i}|<_{{\mathbb Q}} \frac{1}{2^{n}})$. We use Kohlenbach’s ‘hat function’ from [16, p. 289] to guarantee that every $q^{1}$ defines a real number.

• c. We write ‘$x\in {\mathbb R}$’ to express that $x^{1}:=(q^{1}_{(\cdot )})$ represents a real as in the previous item and write $[x](k):=q_{k}$ for the k-th approximation of x.

• d. Two reals x, y represented by $q_{(\cdot )}$ and $r_{(\cdot )}$ are equal, denoted $x=_{{\mathbb R}}y$, if $(\forall n^{0})(|q_{n}-r_{n}|\le {2^{-n+1}})$. Inequality ‘$<_{{\mathbb R}}$’ is defined similarly. We sometimes omit the subscript ‘${\mathbb R}$’ if it is clear from context.

• e. Functions $F:{\mathbb R}\rightarrow {\mathbb R}$ are represented by $\varPhi ^{1\rightarrow 1}$ mapping equal reals to equal reals, i.e. satisfying $(\forall x , y\in {\mathbb R})(x=_{{\mathbb R}}y\rightarrow \varPhi (x)=_{{\mathbb R}}\varPhi (y))$.

• f. The relation ‘$x\le _{\tau }y$’ is defined as in (1) but with ‘$\le _{0}$’ instead of ‘$=_{0}$’. Binary sequences are denoted ‘$f^{1}, g^{1}\le _{1}1$’, but also ‘$f,g\in C$’ or ‘$f, g\in 2^{{\mathbb N}}$’. Elements of Baire space are given by $f^{1}, g^{1}$, but also denoted ‘$f, g\in {\mathbb N}^{{\mathbb N}}$’.

• g. For a binary sequence $f^{1}$, the associated real in [0, 1] is $\mathbb {r}(f):=\sum _{n=0}^{\infty }\frac{f(n)}{2^{n+1}}$.

• h. Sets of type $\rho$ objects $X^{\rho \rightarrow 0}, Y^{\rho \rightarrow 0}, \dots$ are given by their characteristic functions $F^{\rho \rightarrow 0}_{X}\le _{\rho \rightarrow 0}1$, i.e. we write ‘$x\in X$’ for $F_{X}(x)=_{0}1$.

The following special case of item (h) is singled out, as it will be used frequently.

Definition 4

[]. A ‘subset D of ${\mathbb N}^{{\mathbb N}}$’ is given by its characteristic function $F_{D}^{2}\le _{2}1$, i.e. we write ‘$f\in D$’ for $F_{D}(f)=1$ for any $f\in {\mathbb N}^{{\mathbb N}}$. A ‘binary relation $\preceq$ on a subset D of ${\mathbb N}^{{\mathbb N}}$’ is given by some functional $G_{\preceq }^{(1\times 1)\rightarrow 0}$, namely we write ‘$f\preceq g$’ for $G_{\preceq }(f, g)=1$ and any $f, g\in D$. Assuming extensionality on the reals as in item (e), we obtain characteristic functions that represent subsets of ${\mathbb R}$ and relations thereon. Using pairing functions, it is clear we can also represent sets of finite sequences (of reals), and relations thereon.

Next, we mention the highly useful $\textsf {ECF}$-interpretation.

Remark 5

(The ${\mathbf {\mathsf{{ECF}}}}$-interpretation) . The (rather) technical definition of $\textsf {ECF}$ may be found in [33, p. 138, §2.6]. Intuitively, the $\textsf {ECF}$-interpretation $[A]_{\textsf {ECF} }$ of a formula $A\in \textsf {L }_{\omega }$ is just A with all variables of type two and higher replaced by countable representations of continuous functionals. Such representations are also (equivalently) called ‘associates’ or ‘RM-codes’ (see [15, §4]). The $\textsf {ECF}$-interpretation connects and $\textsf {RCA} _{0}$ (see [16, Prop. 3.1]) in that if proves A, then $\textsf {RCA} _{0}$ proves $[A]_{\textsf {ECF} }$, again ‘up to language’, as $\textsf {RCA} _{0}$ is formulated using sets, and $[A]_{\textsf {ECF} }$ is formulated using types, namely only using type zero and one objects.

In light of the widespread use of codes in RM and the common practise of identifying codes with the objects being coded, it is no exaggeration to refer to $\textsf {ECF}$ as the canonical embedding of higher-order into second-order RM. For completeness, we also list the following notational convention for finite sequences.

Notation 6

(Finite sequences) . We assume a dedicated type for ‘finite sequences of objects of type $\rho$’, namely $\rho ^{*}$. Since the usual coding of pairs of numbers goes through in , we shall not always distinguish between 0 and $0^{*}$. Similarly, we do not always distinguish between ‘$s^{\rho }$’ and ‘$\langle s^{\rho }\rangle$’, where the former is ‘the object s of type $\rho$’, and the latter is ‘the sequence of type $\rho ^{*}$ with only element $s^{\rho }$’. The empty sequence for the type $\rho ^{*}$ is denoted by ‘$\langle \rangle _{\rho }$’, usually with the typing omitted.

Furthermore, we denote by ‘$|s|=n$’ the length of the finite sequence $s^{\rho ^{*}}=\langle s_{0}^{\rho },s_{1}^{\rho },\dots ,s_{n-1}^{\rho }\rangle$, where $|\langle \rangle |=0$, i.e. the empty sequence has length zero. For sequences $s^{\rho ^{*}}, t^{\rho ^{*}}$, we denote by ‘$s*t$’ the concatenation of s and t, i.e. $(s*t)(i)=s(i)$ for $i<|s|$ and $(s*t)(j)=t(|s|-j)$ for $|s|\le j< |s|+|t|$. For a sequence $s^{\rho ^{*}}$, we define $\overline{s}N:=\langle s(0), s(1), \dots , s(N-1)\rangle$ for $N^{0}<|s|$. For a sequence $\alpha ^{0\rightarrow \rho }$, we also write $\overline{\alpha }N=\langle \alpha (0), \alpha (1),\dots , \alpha (N-1)\rangle$ for any $N^{0}$. By way of shorthand, $(\forall q^{\rho }\in Q^{\rho ^{*}})A(q)$ abbreviates $(\forall i^{0}<|Q|)A(Q(i))$, which is (equivalent to) quantifier-free if A is.

2.2 Some Axioms of Higher-Order RM

We introduce some functionals which constitute the counterparts of some of the Big Five systems, in higher-order RM. We use the formulation from [16] and [19]. First of all, $\textsf {ACA} _{0}$ is readily derived from:

$$\begin{aligned} (\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 ] \qquad \quad (\mu ^{2})\\&\wedge [ (\forall n)(f(n)\ne 0)\rightarrow \mu (f)=0] \big ], \nonumber \end{aligned}$$

and proves the same sentences as $\textsf {ACA} _{0}$ by [13, Theorem 2.5]. The (unique) functional $\mu ^{2}$ in $(\mu ^{2})$ is called Feferman’s $\mu$ ([1]), and is clearly discontinuous at $f=_{1}11\dots$; in fact, $(\mu ^{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 ([16, §3]), and to

Finally, we list the following comprehension axiom, first introduced in [24].

Definition 7

$\mathrm{[}\textsf {BOOT} \mathrm{]}$ . $(\forall Y^{2})(\exists X^{1})(\forall n^{0})\big [ n\in X \leftrightarrow (\exists f^{1})(Y(f, n)=0) \big ].$

Clearly, $\textsf {BOOT}$ is inspired by the following axiom:

yielding full second-order arithmetic $\textsf {Z}_{2}$, while is a conservative extension of the latter (see [13]). No comprehension axiom weaker than $(\exists ^{3})$ can prove $\textsf {BOOT}$ by the results in [19], [20], [25]. Nonetheless, one readily shows that $[\textsf {BOOT} ]_{\textsf {ECF} }$ is equivalent to $\textsf {ACA} _{0}$ and we finish this section with a conceptual remark on how $\textsf {ECF}$ connects second- and higher-order arithmetic.

Remark 8

(The nature of ${\mathbf {\mathsf{{ECF}}}}$) . We discuss the meaning of the words ‘A is converted into B by the $\textsf {ECF}$-translation’. Such statement is obviously not to be taken literally, as e.g. $[\textsf {BOOT} ]_{\textsf {ECF} }$ is not verbatim $\textsf {ACA} _{0}$. Nonetheless, $[\textsf {BOOT} ]_{\textsf {ECF} }$ follows from $\textsf {ACA} _{0}$ by noting that $(\exists f^{1})(Y(f, n)=0)\leftrightarrow (\exists \sigma ^{0^{*}})(Y(\sigma *00, n)=0)$ for continuous $Y^{2}$ (see [24, §3]). Similarly, let $\textsf {HBU}$ be the Heine-Borel theorem for uncountable covers of Cantor space as studied in [19]. Then $[\textsf {HBU} ]_{\textsf {ECF} }$ is not verbatim the Heine-Borel theorem for countable covers, but the latter does imply the former by noting that for continuous functions, the associated canonical cover has a trivial countable sub-cover enumerated by the rationals in [0, 1].

In general, that continuous objects have countable representations is the very foundation of the formalisation of mathematics in $\textsf {L }_{2}$, and identifying continuous objects and their countable representations is routinely done. Thus, when we say that A is converted into B by the $\textsf {ECF}$-translation, we mean that $[A]_{\textsf {ECF} }$ is about a class of continuous objects to which B is immediately seen to apply, with a possible intermediate step involving representations. Since this kind of step forms the bedrock of classical RM, it is therefore harmless in this context.

3 Main Results

We establish the results sketched in Sect. 1. In each section, we study a known recursive counterexample and show that it lifts to higher-order arithmetic with minimal effort.

3.1 Specker Nets

In Sect. 3.1, we lift the implication involving the monotone convergence theorem for sequences and arithmetical comprehension to higher-order arithmetic. This results in an implication involving the monotone convergence theorem for nets indexed by Baire space and the comprehension axiom $\textsf {BOOT}$ from Sect. 2.2. Nets and associated concepts are introduced in Sect. 3.1.

In more detail, the proof that the monotone convergence theorem implies $\textsf {ACA} _{0}$ from [28, III.2] is based on a recursive counterexample by Specker ([31]), who proved the existence of a computable increasing sequence of rationals in the unit interval that does not converge to any computable real number. We show that these results lift to the higher-order setting in that essentially the same proof yields that the monotone convergence theorem for nets indexed by Baire space implies $\textsf {BOOT}$. In particular, the notion of Specker sequence readily generalises to Specker net. We provide full details for this case, going as far as comparing the original and ‘lifted’ proof side-by-side. A much less detailed proof was first published in [24].

Nets: Basics and Definitions. We introduce the notion of net and associated concepts. Intuitively speaking, nets are the generalisation of sequences to (possibly) uncountable index sets; nets are essential for convergence in topology and domain theory. On a historical note, Moore-Smith and Vietoris independently introduced these notions about a century ago in [18] and [35], which is why nets are also called Moore-Smith sequences. Nets and filters yield the same convergence theory, but e.g. third-order nets are represented by fourth-order filters, i.e. nets are more economical in terms of type complexity (see [2]).

We use the following definition from [14, Ch. 2].

Definition 9

$\mathrm{[Nets]}$ . A set $D\ne \emptyset$ with a binary relation ‘$\preceq$’ is directed if

• a. The relation $\preceq$ is transitive, i.e. $(\forall x, y, z\in D)([x\preceq y\wedge y\preceq z] \rightarrow x\preceq z )$.

• b. For $x, y \in D$, there is $z\in D$ such that $x\preceq z\wedge y\preceq z$.

• c. The relation $\preceq$ is reflexive, i.e. $(\forall x\in D)(x \preceq x)$.

For such $(D, \preceq )$ and topological space X, any mapping $x:D\rightarrow X$ is a net in X. We denote $\lambda d. x(d)$ as ‘$x_{d}$’ or ‘$x_{d}:D\rightarrow X$’ to suggest the connection to sequences. The directed set $(D, \preceq )$ is not always explicitly mentioned together with a net $x_{d}$.

We only use directed sets that are subsets of ${\mathbb N}^{{\mathbb N}}$, i.e. as given by Definition 4. Similarly, we only study nets $x_{d}:D\rightarrow {\mathbb R}$ where D is a subset of ${\mathbb N}^{{\mathbb N}}$. Thus, a net $x_{d}$ in ${\mathbb R}$ is just a type $1\rightarrow 1$ functional with extra structure on its domain D provided by ‘$\preceq$’ as in Definition 4, i.e. part of third-order arithmetic.

The definitions of convergence and increasing net are of course familiar.

Definition 10

$\text {[Convergence of nets]}$ . If $x_{d}$ is a net in X, we say that $x_{d}$ converges to the limit $\lim _{d} x_{d}=y\in X$ if for every neighbourhood U of y, there is $d_{0}\in D$ such that for all $e\succeq d_{0}$, $x_{e}\in U$.

Definition 11

$\text {[Increasing nets]}$ . A net $x_{d}:D\rightarrow {\mathbb R}$ is increasing if $a\preceq b$ implies $x_{a}\le _{{\mathbb R}} x_{b}$ for all $a,b\in D$.

Many (convergence) notions concerning sequences carry over to nets mutatis mutandis. A rather general RM study of nets may be found in [26], [27], [24], [25]. We shall study the monotone convergence theorem for nets as follows.

Definition 12

$\mathrm{[}\textsf {MCT} _{\textsf {net} }^{[0,1]}\mathrm{]}$ . Any increasing net in [0, 1] indexed by ${\mathbb N}^{{\mathbb N}}$ converges.

The ‘original’ monotone convergence theorem for sequences as in [28, III.2] is denoted $\textsf {MCT} _{\textsf {seq} }^{[0,1]}$. Following Remark 8, we say that $\textsf {MCT} _{\textsf {seq} }^{[0,1]}$ is the $\textsf {ECF}$-interpretation of $\textsf {MCT} _{\textsf {net} }^{[0,1]}$. The implications $\textsf {MCT} _{\textsf {seq} }^{[0,1]}\leftarrow \textsf {ACA} _{0}$ and $\textsf {MCT} _{\textsf {net} }^{[0,1]}\leftarrow \textsf {BOOT}$ are in fact proved in exactly the same way.

Finally, sequences are nets with index set $({\mathbb N}, \le _{{\mathbb N}})$ and theorems pertaining to nets therefore apply to sequences. However, some care is advised as e.g. a sub-net of a sequence is not necessarily a sub-sequence (see [25, §3]).

Specker Nets and Comprehension. In this section, we show that $\textsf {MCT} _{\textsf {net} }^{[0,1]}\rightarrow \textsf {BOOT}$ using a minor variation of the well-known proof $\textsf {MCT} _{\textsf {seq} }^{[0,1]}\rightarrow \textsf {ACA} _{0}$ from [28, III.2.2] involving Specker sequences.

First of all, we distill the essence of the latter proof, as follows.

• i. We prove $\textsf {MCT} _{\textsf {seq} }^{[0,1]}\rightarrow \textsf {range}$, where the latter states that the range exists for any function, i.e. $(\forall f^{1})(\exists X\subset {\mathbb N})(\forall k\in {\mathbb N})\big (k \in X\leftrightarrow (\exists m^{0})(f(m)=k)\big )$.

• ii. Fix $f^{1}$ and define the Specker sequence $c_{n}:=\sum _{i=0}^{n}2^{-f(i)}$.

• iii. Note that $\textsf {MCT} _{\textsf {seq} }^{[0,1]}$ applies and let c be $\lim _{n\rightarrow \infty }c_{n}$.

• iv. Establish the following equivalence:

  $$\begin{aligned} (\exists m^{0})(f(m)=k)\leftrightarrow (\forall n^{0})\big ( |c_{n}-c|<2^{-k}\rightarrow (\exists i\le n)(f(i)=k) \big ), \end{aligned}$$

  (3)

• v. Apply $\varDelta _{1}^{0}$-comprehension to (3), yielding the set X needed for $\textsf {range}$.

We now show how to lift the previous steps to higher-order arithmetic, resulting in a proof of $\textsf {MCT} _{\textsf {net} }^{[0,1]}\rightarrow \textsf {BOOT}$ in Theorem 15.

Regarding item (v), to lift proofs involving $\varDelta _{1}^{0}$-comprehension to the higher-order framework, we introduce the following comprehension axiom:

$$\begin{aligned} (\forall Y^{2}, Z^{2})\big [ (\forall n^{0})\big ( (\exists f^{1})&(Y(f, n)=0) \leftrightarrow (\forall g^{1})(Z(g, n)=0) \big ) \qquad \qquad \quad \quad (\varDelta \hbox {-}\textsf {CA} ) \\&\rightarrow (\exists X^{1})(\forall n^{0})(n\in X\leftrightarrow (\exists f^{1})(Y(f, n)=0)\big ].\nonumber \end{aligned}$$

A snippet of countable choice suffices to prove $\varDelta$-comprehension and we observe that the $\textsf {ECF}$-translation converts $\varDelta$-comprehension into $\varDelta _{1}^{0}$-comprehension while $\textsf {QF}\text{- }\textsf {AC} ^{0,1}$ becomes $\textsf {QF}\text{- }\textsf {AC} ^{0,0}$, all following Remark 8.

Theorem 13

The system proves $\varDelta \text {-}\textsf {CA}$.

Proof

The antecedent of $\varDelta$-comprehension implies the following

$$\begin{aligned} (\forall n^{0})(\exists g^{1}, f^{1})( Z(g, n)=0\rightarrow Y(f, n)=0 ). \end{aligned}$$

(4)

Applying $\textsf {QF}\text{- }\textsf {AC} ^{0,1}$ to (4) yields $\varPhi ^{0\rightarrow 1}$ such that

$$\begin{aligned} (\forall n^{0})\big ( (\forall g^{1})(Z(g, n)=0)\rightarrow Y(\varPhi (n), n)=0 \big ), \end{aligned}$$

(5)

and by assumption an equivalence holds in (5), and we are done.    $\square$

The previous is not spielerei: the crux of numerous reversals $T\rightarrow \textsf {ACA} _{0}$ is that the theorem T somehow allows for the reduction of $\varSigma _{1}^{0}$-formulas to $\varDelta _{1}^{0}$-formulas, while $\varDelta _{1}^{0}$-comprehension -included in $\textsf {RCA} _{0}$- then yields the required $\varSigma _{1}^{0}$-comprehension, and $\textsf {ACA} _{0}$ follows. Additional motivation for $\varDelta \text {-}\textsf {CA}$ is provided by Theorem 30.

Regarding item (i), lifting $\textsf {range}$ to the higher-order framework is fairly basic: we just consider the existence of the range of type two functionals (rather than type one functions), as in $\textsf {RANGE}$ below.

Theorem 14

The system proves that $\textsf {BOOT}$ is equivalent to

Proof

The forward direction is immediate. For the reverse direction, define $G^{2}$ as follows for $n^{0}$ and $g^{1}$: put $G(\langle n\rangle *g)=n+1$ if $Y(g, n)=0$, and 0 otherwise. Let $X\subseteq {\mathbb N}$ be as in $\textsf {RANGE}$ and note that

$$\begin{aligned} (\forall m^{0}\ge 1 )( m\in X \leftrightarrow (\exists f^{1})(G(f)=m)\leftrightarrow (\exists g^{1})(Y(g, m-1)=0) ). \end{aligned}$$

(6)

which is as required for $\textsf {BOOT}$ after trivial modification.    $\square$

This theorem was first proved as [24, Theorem 3.19]. Again, the previous is not a gimmick: reversals involving $\textsf {ACA} _{0}$ are often established using $\textsf {range}$, and those yield implications involving $\textsf {RANGE}$, for instance as follows.

Theorem 15

The system proves $\textsf {MCT} _{\textsf {net} }^{[0,1]}\rightarrow \textsf {BOOT}$.

Proof

In case $\lnot (\exists ^{2})$, note that $\textsf {MCT} _{\textsf {net} }^{[0,1]}$ implies $\textsf {MCT} _{\textsf {seq} }^{[0,1]}$ as sequences are nets with directed set $({\mathbb N}, \le _{{\mathbb N}})$. By [28, III.2], $\textsf {ACA} _{0}$ is available, which readily implies $\textsf {BOOT}$ for continuous $Y^{2}$, but all functions on ${\mathbb N}^{{\mathbb N}}$ are continuous by [16, §3].

In case $(\exists ^{2})$, we shall establish $\textsf {RANGE}$ and obtain $\textsf {BOOT}$ by Theorem 14, which mimics the above item (i). We let $(D, \preceq _{D})$ be a directed set with D consisting of the finite sequences in ${\mathbb N}^{{\mathbb N}}$ and $v\preceq _{D} w$ if $(\forall i<|v|)(\exists j<|w|)(v(i)=_{1}w(j))$ for any $v^{1^{*}}, w^{1^{*}}$. Note that $(\exists ^{2})$ is necessary for this definition.

Following item (ii), fix some $Y^{2}$ and define the ‘Specker net’ $c_{w}:D\rightarrow [0,1]$ as $c_{w}:= \sum _{i=0}^{|w|-1}2^{-Y(w(i))}$. Clearly, $c_{w}$ is increasing as in Definition 11 and let c be the limit provided by $\textsf {MCT} _{\textsf {net} }^{[0,1]}$, following item (iii). Following item (iv), consider the following generalisation of (3), for any $k\in {\mathbb N}$:

$$\begin{aligned} (\exists f^{1})(Y(f)=k)\leftrightarrow (\forall w^{1^{*}})\big ( |c_{w}-c|<2^{-k}\rightarrow (\exists g\in w)(Y(g)=k) \big ), \end{aligned}$$

(7)

for which the reverse direction is trivial thanks to $\lim _{w}c_{w}=c$. For the forward direction in (7), assume the left-hand side holds for $f=f_{1}^{1}$ and fix some $w_{0}^{1^{*}}$ such that $|c-c_{w_{0}}|<\frac{1}{2^{k}}$. Since $c_{w}$ is increasing, we also have $|c-c_{w}|<\frac{1}{2^{k}}$ for $w\succeq _{D} w_{0}$. Now there must be $f_{0}$ in $w_{0}$ such that $Y(f_{0})=k$, as otherwise $w_{1}=w_{0}*\langle f_{1}\rangle$ satisfies $w_{1}\succeq _{D}w_{0}$ but also $c_{w_{1}}>c$, which is impossible.

Note that (7) has the right form to apply $\varDelta \text {-}\textsf {CA}$ (modulo obvious coding), and the latter provides the set required by $\textsf {RANGE}$, following item (v).    $\square$

We refer to the net $c_{w}$ from the proof as a Specker net following the concept of Specker sequence pioneered in [31]. We hope that the reader agrees that the previous proof is exactly the final part of the proof of [28, III.2.2] as in items (i)–(v), save for the replacement of sequences by nets and functions by functionals. The aforementioned ‘reuse’ comes at a cost however: the proof of $\textsf {MCT} _{\textsf {net} }^{[0,1]}\leftrightarrow \textsf {BOOT}$ in [24, §3.2] does not make use of countable choice or $\varDelta \text {-}\textsf {CA}$. Moreover, from the proof of this equivalence, once can essentially ‘read off’ that a realiser for $\textsf {MCT} _{\textsf {net} }^{[0,1]}$ computes $\exists ^{3}$ in the sense of Kleene’s S1-S9, and vice versa (see also [25, §3.1]). It seems one cannot obtain this S1-S9 result from the above proof because of $\varDelta \text {-}\textsf {CA}$.

Finally, Theorem 15 readily generalises by increasing the size of the index sets to any set of objects of finite type. The case of nets indexed by $\mathcal {N}\equiv {\mathbb N}^{{\mathbb N}}\rightarrow {\mathbb N}$ may be found in [24, Theorem 3.38]. In particular, the monotone convergence theorem for nets indexed by $\mathcal {N}$ in [0, 1] implies the following axiom:

which states the existence of the range of type three functionals.

3.2 Compactness of Metric Spaces

Complete separable metric spaces are represented (or: coded) in second-order arithmetic by countable dense subsets with a pseudo-metric (see e.g. [4, 28]). Various notions of compactness can then be formulated and their relations have been analysed in detail (see e.g. [4]). In this section, we lift some of these results to higher-order arithmetic; in doing so, we shall observe that the development of metric spaces in weak systems must proceed via codes, lest strong comprehensions or countable choice be needed in basic cases.

Our starting point is [4, Theorem 3.13], which establishes the equivalence between $\textsf {ACA} _{0}$ and every (countable) Heine-Borel compact complete metric space is totally bounded. The reverse implication is established via $\textsf {range}$ and we lift this result to higher-order arithmetic. We make use of the standard definition of metric spaces, which does not use coding and can be found verbatim in [22, 23].

Definition 16

A complete metric space $\tilde{D}$ over ${\mathbb N}^{{\mathbb N}}$ consists of $D\subseteq {\mathbb N}^{{\mathbb N}}$, an equivalence² relation $=_{D}$, and $d: (D\times D)\rightarrow {\mathbb R}$ such that for all $e, f, g \in D$:

• a. $d(e, f)=_{{\mathbb R}}0 \leftrightarrow e=_{D}f$,

• b. $0\le _{{\mathbb R}} d(e, f)=_{{\mathbb R}}d(f, e),$

• c. $d(f, e)\le _{{\mathbb R}} d(f, g)+ d(g, e)$,

and such that every Cauchy sequence in D converges to some element in D.

To be absolutely clear, the final condition regarding $\tilde{D}$ in the definition means that if $\lambda n.f_{n}$ is a sequence in D such that $(\forall k^{0})(\exists N^{})(\forall m^{0}, n^{0}\ge N)(d(f_{n}, f_{m})<_{{\mathbb R}}\frac{1}{2^{k}})$, then there is $g\in D$ such that $(\forall k^{0})(\exists n^{0})(\forall m\ge n)(d(f_{m}, g)<\frac{1}{2^{k}})$. A point in $\tilde{D}$ is just any element in D. Two points $e, f\in \tilde{D}$ are said to be equal if $e=_{D}f$. Note that the ‘hat function’ from [16] readily yields ${\mathbb R}$ as a metric space over ${\mathbb N}^{{\mathbb N}}$.

We use standard notation like B(e, r) for the open ball $\{f\in D: d(f, e)<_{{\mathbb R}}r\}$. The first item in Definition (16) expresses a kind of extensionality property and we tacitly assume that every mapping with domain D respects ‘$=_{D}$’.

Definition 17

$\text {[Heine-Borel]}$ . A complete metric space $\tilde{D}$ over ${\mathbb N}^{{\mathbb N}}$ is Heine-Borel compact if for any $Y: {D}\rightarrow {\mathbb R}^{+}$, the cover $\cup _{e\in {D}} B(e, Y(e))$ has a finite sub-cover.

We define countable Heine-Bore compactness as the previous definition restricted to countable covers of D.

Definition 18

$\text {[Totally bounded]}$ . A complete metric space $\tilde{D}$ over ${\mathbb N}^{{\mathbb N}}$ is totally bounded if there is a sequence of finite sequences $\lambda n.x_{n}^{0\rightarrow 1^{^{*}}}$ of points in $\tilde{D}$ such that for any $x\in {D}$ there is $n\in {\mathbb N}$ such that $d(x, x_{n}(i))<2^{-n}$ for some $i<|x_{n}|$.

We now obtain the following theorem by lifting the proof of [4, Theorem 3.13].

Theorem 19

proves that either of the following items:

• a. a Heine-Borel compact complete metric space over ${\mathbb N}^{{\mathbb N}}$ is totally bounded,

• b. item (a) restricted to countable Heine-Borel compactness,

• c. item (a) with sequential compactness instead of Heine-Borel compactness,

implies the comprehension axiom $\textsf {BOOT}$.

Proof

We derive $\textsf {RANGE}$ from item (a), and $\textsf {BOOT}$ is therefore immediate; the implication involving item (b) is then immediate. Fix some $Y^{2}$ and define $D={\mathbb N}^{{\mathbb N}}\cup \{0_{D}\}$ where $0_{D}$ is some special element. Define $f=_{D}e$ as $Y(f)=_{0}Y(e)$ for any $e, f\in D\setminus \{0_{D}\}$, while $0_{D}=0_{D}$ is defined as true and $f=_{D}0_{D}$ is defined as false for $d\in D\setminus \{0_{D} \}$.

Define $d:D^{2}\rightarrow {\mathbb R}$ as follows: $d(f, g)= |2^{-Y(f)}-2^{-Y(g)}|$ if $f, g\ne _{D}0$, $d(0_{D}, 0_{D})=0$, and $d(0_{D}, f)=d(f, 0_{D})= 2^{-Y(f)}$ for $f \ne _{D} 0$. Clearly, this is a metric space in the sense of Definition 16 and the ‘zero element’ $0_{D}$ satisfies $\lim _{n\rightarrow \infty }d(0_{D},f_{n} )=_{{\mathbb R}}0$, assuming Y is unbounded on ${\mathbb N}^{{\mathbb N}}$ and $\lambda n.f_{n}$ is a sequence in D witnessing this, i.e. $Y(f_{n})\ge n$ for any $n\in {\mathbb N}$.

Now, given a Cauchy sequence $\lambda n.f_{n}$ in D, either it converges to $0_{D}$ or $d(0_{D}, f_{n})$ is eventually constant, i.e. the completeness property of $\tilde{D}$ is satisfied. Moreover, the Heine-Borel property as in Definition 17 is also straightforward, as any neighbourhood of $0_{D}$ covers all but finitely many $2^{-Y(f)}$ for $f\in {\mathbb N}^{{\mathbb N}}$ by definition. One seems to need $\textsf {IND}$ to form the finite sub-cover. Let $\lambda n.x_{n}$ be the sequence provided by item (a) that witnesses that $\tilde{D}$ is totally bounded. Now define $X\subseteq {\mathbb N}$ as:

$$\begin{aligned} n\in X \leftrightarrow (\exists i<|x_{n+1}|)\big [2^{-n}=_{{\mathbb R}}d(0_{D}, x_{n+1}(i))], \end{aligned}$$

(8)

and one readily shows that $n\in X\leftrightarrow (\exists f^{1})(Y(f)=n)$, i.e. $\textsf {RANGE}$ follows. Note that one can remove ‘$=_{{\mathbb R}}$’ from (8) in favour of a decidable equality.

Regarding item (c), if a sequence $\lambda n.f_{n}$ is ‘unbounded’ as in $(\forall m^{0})(\exists n^{0})(Y(f_{n})> m)$, then there is an obvious sub-sequence that converges to $0_{D}$. In case we have $(\exists m^{0})(\forall n^{0})(Y(f_{n})\le m)$, there is a constant sub-sequence, and the space $\tilde{D}$ is clearly sequentially compact.    $\square$

In light of the considerable logical hardness of $\textsf {BOOT}$, it is clear that for developing mathematics in weak systems, one must avoid items (a)–(c) and therefore Definition 16, i.e. the use of codes for metric spaces would seem to be essential for this development. This is particularly true since item (b) only deals with countable covers, i.e. the only higher-order object is the metric space, and the same for item (c). For those still not entirely convinced, Corollary 20 below shows that countable choice can be derived from item (a), i.e. the non-constructive nature of the latter is rampant compared to the version involving codes, namely [4, Theorem 3.13.ii].

Now, Definition 18 is used in RM (see e.g. [4, 28]) and is sometimes referred to as effective total boundedness as there is a sequence that enumerates the finite sequences of approximating points. As it turns out, this extra information yields countable choice in the higher-order setting. Note that the monotone convergence theorem for nets with a modulus of convergence similarly yields $\textsf {BOOT} +\textsf {QF}\text{- }\textsf {AC} ^{0,1}$ by [24, §3.3]; obtaining countable choice in this context therefore seems normal.

Corollary 20

The system proves the implication $[\mathrm{item \ (a) } \rightarrow \textsf {QF}\text{- }\textsf {AC} ^{0,1}]$.

Proof

In light of $n\in X\leftrightarrow (\exists f^{1})(Y(f)=n)$ and (8), one of the $x_{n+1}(i)$ for $i<|x_{n+1}|$ provides a witness to $(\exists f^{1})(Y(f)=n)$ if such there is.    $\square$

One can show that item (b) implies the associated second-order statement in case $\lnot (\exists ^{2})$; the usual proof of [4, Theorem 3.13] can then be used. Thus, the $\textsf {ECF}$-translation (more or less) converts item (a) to the original second-order theorem. Intuitively speaking, assuming $D\subseteq {\mathbb N}^{{\mathbb N}}$ has a continuous characteristic function, it can be replaced with an enumeration of all finite sequences $\sigma ^{0^{*}}$ such that $\sigma *00\in D$.

Finally, one can generalise the previous to higher types. For instance, Definition 16 obviously generalises mutatis mutandis to yield the definition of complete metric spaces $\tilde{D}$ over $\mathcal {N}\equiv {\mathbb N}^{{\mathbb N}}\rightarrow {\mathbb N}$, and the same for any finite type. As opposed to nets indexed by function spaces like $\mathcal {N}$, a metric space based on the latter is quite standard. The proof of Theorem 19 can then be relativised with ease.

Corollary 21

proves that the following:

$\mathrm{(d)}$ a countable Heine-Borel compact complete metric space over $\mathcal {N}$ is totally bounded,

implies the comprehension axiom $\textsf {RANGE} ^{1}$.

Note that $\textsf {RANGE} ^{1}$ was first introduced in [24, §3.7] and follows from the monotone convergence theorem for nets indexed by $\mathcal {N}$. In fact, the usual proof of the monotone convergence theorem involving Specker sequences immediately generalises to Specker nets indexed by $\mathcal {N}$, as discussed in Sect. 3.1.

In conclusion, it seems the development of metric spaces in weak systems must proceed via codes, lest strong comprehensions or countable choice be needed in basic cases. Indeed, $\textsf {BOOT}$ is not provable from any comprehension axiom weaker than $(\exists ^{3})$, and ‘larger’ metric spaces require even stronger comprehension axioms (see Corollary 21). Moreover, countable choice is also lurking around the corner by Corollary 20, implying codes are the only way we can reasonably study general metric spaces in weak logical systems.

3.3 Rado Selection Lemma

We study the Rado selection lemma, introduced in [21]. The countable version of this lemma is equivalent to $\textsf {ACA} _{0}$ by [28, III.7.8], while a proof based on $\textsf {range}$ can be found in [12, §3]. We shall lift the reversal to higher-order arithmetic, making use of $\textsf {RANGE}$. We first need some definitions.

Definition 22

A choice function f for a collection of non-empty $A_{i}$ indexed by I, is such that $f(i)\in A_{i}$ for all $i\in I$.

A collection of finite subsets of ${\mathbb N}$ indexed by ${\mathbb N}^{{\mathbb N}}$ is of course given by a mapping $Y^{1\rightarrow 0^{*}}$. In case the latter is continuous, the index set is actually countable.

Definition 23

$\mathrm{[(}\textsf {Rado} ({\mathbb N}^{{\mathbb N}})\mathrm{]}$ . Let $A_{i}$ be a collection of finite sets indexed by ${\mathbb N}^{{\mathbb N}}$ and let $F_{J}^{2}$ be a choice function for the collection $A_{j}$ for $j\in J$, for any finite set $J\subset {\mathbb N}^{{\mathbb N}}$. Then there is a choice function $F^{2}$ for the entire collection $A_{j}$ such that for all finite $J\subset {\mathbb N}^{{\mathbb N}}$, there is a finite $K\supseteq J$ such that for $j\in J$, $F(j)=_{0}F_{K}(j)$.

The following theorem is obtained by lifting the proof of [12, Theorem 3.30] to higher-order arithmetic.

Theorem 24

The system proves $\textsf {Rado} ({\mathbb N}^{{\mathbb N}})\rightarrow \textsf {BOOT}$.

Proof

We assume that finite sequences in ${\mathbb N}^{{\mathbb N}}$ are coded by elements of ${\mathbb N}^{{\mathbb N}}$ in the usual way. We will prove $\textsf {RANGE}$, i.e. fix some $G^{2}$. For any $w^{1^{*}}$, define $A_{w}:=\{0,1\}$ and the associated choice function $F_{w}^{2}(h^{1}):=1$ if $(\exists g\in w)(G(g)=h(0))$, and zero otherwise. For $F^{2}$ as in $\textsf {Rado} ({\mathbb N}^{{\mathbb N}})$, we have the following implications for any $n\in {\mathbb N}$ and where $\widetilde{n}:=\langle n\rangle * \langle n\rangle *\dots$ is a sequence:

$$\begin{aligned} (\exists g^{1})(G(g)=n)\rightarrow (\exists w_{0}^{1^{*}})(F_{w_{0}}(\widetilde{n})=1)\rightarrow F(\widetilde{n})=1\rightarrow (\exists g^{1})(G(g)=n). \end{aligned}$$

(9)

The first implication in (9) follows by definition, while the others follow by the properties of $F^{2}$. Hence, $\textsf {RANGE}$ follows, yielding $\textsf {BOOT}$.    $\square$

The previous proof, does not make use of countable choice or $\varDelta \text {-}{\textsf {CA}}$. Thus, for larger collections indexed by subsets of type n objects, one readily obtains e.g. $\textsf {RANGE} ^{1}$ as in Corollary 21, but without extra choice or comprehension. Finally, a reversal in Theorem 24 seems to need $\textsf {BOOT}$ plus choice.

Hirst introduces a version of the Rado selection lemma in [12, §3] involving a bounding function, resulting in a reversal to $\textsf {WKL} _{0}$. A similar bounding function could be introduced, restricting ${\mathbb N}^{{\mathbb N}}$ to some compact sub-space while obtaining (only) the Heine-Borel theorem for uncountable covers as in $\textsf {HBU}$ from [19].

3.4 Fields and Order

We lift the following implication to higher-order arithmetic: that any countable formally real field is orderable implies weak König’s lemma (see [28, IV.4.5]). This result is based on a recursive counterexample by Ershov from [6], as (cheerfully) acknowledged in [10, p. 145].

First of all, the aforementioned implication is obtained via an intermediate principle involving the separation of disjoint ranges of functions (see [28, IV.4.4]). The generalisation of the latter to higher-order arithmetic and type two functionals is $\textsf {SEP} ^{1}$ as follows:

$$ (\forall Y^{2}, Z^{2})\big [(\forall f^{1}, g^{1})(Y(f)\ne Z(g))\rightarrow (\exists X^{1})(\forall g^{1})(Y(g)\in X \wedge Z(g)\not \in X ) \big ]. $$

Modulo $\textsf {QF}\text{- }\textsf {AC} ^{0,1}$, $\textsf {SEP} ^{1}$ is equivalent to the Heine-Borel theorem for uncountable covers of [0, 1] as in $\textsf {HBU}$ from [19]. We need the following standard definitions.

Definition 25

$\text {[Field over Baire space]}$ . A field K over Baire space consists of a set $|K|\subseteq {\mathbb N}^{{\mathbb N}}$ with distinguished elements $0_{K}$ and $1_{K}$, an equivalence relation $=_{K}$, and operations $+_{K}$, $-_{K}$ and $\times _{K}$ on |K| satisfying the usual field axioms.

Definition 26

A field K is formally real if there is no sequence $c_{0}, \dots , c_{n}\in |K|$ such that $0=_{K}\sum _{i=0}^{n}c_{i}^{2}$.

Definition 27

A field K over ${\mathbb N}^{{\mathbb N}}$ is orderable if there exists an binary relation ‘$<_{K}$’ on |K| satisfying the usual axioms of ordered field.

As in [28], we sometimes identify K and |K|. With these definitions, the following theorem is a generalisation of [28, IV.4.5.2].

Definition 28

$\mathrm{[}\textsf {ORD} \mathrm{]}$ A formally real field over ${\mathbb N}^{{\mathbb N}}$ is orderable.

We have the following theorem where the proof is obtained by lifting the proof of [28, IV.4.5] to higher-order arithmetic.

Theorem 29

The system proves that $\textsf {ORD} \rightarrow \textsf {SEP} ^{1}$.

Proof

Let $p_{k}$ be an enumeration of the primes and fix some $Y^{2}, Z^{2}$ as in the antecedent of $\textsf {SEP} ^{1}$. By [28, II.9.7], the algebraic closure of ${\mathbb Q}$, denoted $\overline{{\mathbb Q}}$, is available in $\textsf {RCA} _{0}$. For $w^{1^{*}}$, define $K_{w}$ as the sub-field of $\overline{{\mathbb Q}}(\sqrt{-1})$ generated by:

$$\textstyle \{\root 4 \of {p_{Y(w(i))}}:i<|w|\}\cup \{\sqrt{-\sqrt{ p_{Z(w(j))}}}:j<|w|\}\cup \{ \sqrt{p_{k}}:k<|w| \}. $$

Note that one can define such a sub-field from a finite set of generators in $\textsf {RCA} _{0}$ (see [28, IV.4]). Unfortunately, this is not possible for infinite sets and we need a different approach, as follows. By the proof of Theorem 14 (and (6) in particular), there is a functional $G^{2}$ such that:

$$\begin{aligned} \big (\forall b\in \overline{{\mathbb Q}}(\sqrt{-1})\big )\big [ (\exists w^{1^{*}})(b\in K_{w})\leftrightarrow (\exists v^{1^{*}})(G(v)=b) \big ]. \end{aligned}$$

(10)

Intuitively, we now want to define the field $\cup _{f\in {\mathbb N}^{{\mathbb N}}}K_{\langle f\rangle }$, but the latter cannot be (directly) defined as a set in weak systems. We therefore take the following approach: we define a field K over Baire space using G from (10), as follows: for $w^{1^{*}}, v^{1^{*}}$, define $w+_{K}v$ as that $u^{1^{*}}$ such that $G(u)=G(v)+_{\overline{{\mathbb Q}}(\sqrt{-1})}~G(w)$. This $u^{1^{*}}$ is found by removing from $v*w$ all elements from G(v) and G(w) that sum to 0 in $G(v)+_{\overline{{\mathbb Q}}(\sqrt{-1})}G(w)$. Multiplication $\times _{K}$ is defined similarly, while $-_{K}w^{1^{*}}$ provides an extra label such that $G(-_{K}w)=-b$ if $G(w)=b$ and the ‘inverse function’ of $\times _{K}$ is defined similarly. Using (10) for $w=\langle \rangle$, $0_{K}$ and $1_{K}$ are given by those finite sequences $v_{0}$ and $v_{1}$ such that $G(v_{0})=0_{\overline{{\mathbb Q}}(\sqrt{-1})}$ and $G(v_{1})=1_{\overline{{\mathbb Q}}(\sqrt{-1})}$. Finally, $v^{1^{*}}=_{K} w^{1^{*}}$ is defined as the decidable equality $G(w)=_{{\mathbb Q}(\sqrt{-1})}G(v)$.

We call the resulting field K and proceed to show that it is formally real. To this end, note that $K_{w}$ can be embedded into $\overline{{\mathbb Q}}$ by mapping $\sqrt{p_{Y(w(i))}}$ to $\sqrt{p_{Y(w(i))}}$ and $\sqrt{p_{k}}$ to $-\sqrt{p_{k}}$ for $k\ne Y(w(i))$ for $i<|w|$. Hence, $K_{w}$ is formally real for every $w^{1^{*}}$. As a result, K is also formally real because a counterexample to this property would live in $K_{v}$ for some $v^{1^{*}}$. Applying $\textsf {ORD}$, K now has an order $<_{K}$. Since $\sqrt{p_{Y(f)}}$ has a square root in $K_{\langle f\rangle }$, namely $\root 4 \of {p_{Y(f)}}$, we have $u^{1^{*}}>_{K}0_{K}$ if $G(u)=\sqrt{p_{Y(f)}}$, using the basic properties of the ordered field K. One similarly obtains $v^{1^{*}}<_{K}0_{K}$ if $G(v)=\sqrt{p_{Z(g)}}$. Intuitively speaking, the order $<_{K}$ thus allows us to separate the ranges of Y and Z. To this end, consider the following equivalence, for every $k^{0}$:

$$\begin{aligned} (\exists u^{1^{*}})(u>_{K} 0_{K}\wedge G(u)=\sqrt{p_{k}})\leftrightarrow (\forall v^{1^{*}})\big ( G(v)=\sqrt{p_{k}}\rightarrow v>_{K}0_{K}\big ). \end{aligned}$$

(11)

The forward direction in (11) is immediate in light of the properties of $=_{K}$ and $<_{K}$. For the reverse direction in (11), fix $k_{0}$ and find $w_{0}^{1^{*}}$ such that $|w_{0}|>k_{0}$. Since $\sqrt{p_{k_{0}}}\in K_{w_{0}}$, (10) yields $v_{0}^{1^{*}}$ such that $G(v_{0})=\sqrt{p_{k_{0}}}$. The right-hand side of (11) implies $v_{0}>_{K}0_{K}$, and the left-hand side of (11) follows.

Finally, apply $\varDelta$-comprehension to (11) and note that the resulting set X satisfies $(\forall f^{1})(Y(f)\in X\wedge Z(f)\not \in X)$. Indeed, fix $f_{1}^{1}$ and put $k_{1}:=Y(f_{1})$. Clearly, $\sqrt{p_{k_{1}}}\in K_{\langle f_{1}\rangle }$, yielding $v_{1}$ such that $G(v_{1})=\sqrt{p_{k_{1}}}$ by (10). As noted above, the latter number has a square root, implying $v_{1}>_{K}0$, and $Y(f_{1})=k_{1}\in X$ by definition. Similarly, $k_{2}:=Z(f_{1})$ satisfies $\sqrt{p_{k_{2}}}\in K_{\langle f_{1}\rangle }$ and (10) yields $v_{2}$ such that $G(v_{2})=\sqrt{p_{k_{2}}}$. Since $-\sqrt{p_{k_{2}}}$ has a square root in K, $v_{2}<_{K}0_{K}$ follows, and $k_{2}\not \in X$, again by the definition of X.    $\square$

Next, the following theorem yield further motivation for $\varDelta \text {-}\textsf {CA}$.

Theorem 30

The system proves $\textsf {SEP} ^{1}\rightarrow \varDelta \text {-}\textsf {CA}$.

Proof

To establish this implication, let $G^{2}, H^{2}$ be such that

$$\begin{aligned} (\forall k^{0})\big [(\exists f^{1})(G(f)=k)\leftrightarrow (\forall g^{1})(H(g)\ne k)\big ]. \end{aligned}$$

(12)

By definition, G, H satisfy the antecedent of $\textsf {SEP} ^{1}$. Let X be the set obtained by applying the latter and consider:

$$ (\exists f^{1})(G(f)=k)\rightarrow k\in X\rightarrow (\forall g^{1})(H(g)\ne k)\rightarrow (\exists f^{1})(G(f)=k), $$

where the final implication follows from (12); for the special case (12), X is now the set required by $\varDelta$-$\textsf {CA}$. For $Y^{(1\times 0)\rightarrow 0}$, define $G^{2}$ as follows for $n^{0}$ and $g^{1}$: put $G(\langle n\rangle *g)=n+1$ if $Y(g, n)=0$, and 0 otherwise. Note that for $k\ge 1$, we have

$$ (\exists f^{1})(Y(f,k)=0)\leftrightarrow (\exists g^{1})(G(g)=k). $$

Hence, (12) is ‘general enough’ to obtain full $\varDelta$-$\textsf {CA}$, and we are done.    $\square$

4 Concluding Remarks

We finish this paper with some conceptual remarks.

4.1 Future Work and Alternative Approaches

In this section, we discuss future work and alternative approaches.

First of all, we list some topics that can be lifted to higher-order arithmetic in the same way as in the previous sections.

• a. Algebraic closures of countable fields (see [28, III.3 and IV.4]).

• b. Maximal ideals of countable fields (see [28, III.3] or [11]).

• c. Ordering countable groups (see [30]).

• d. Persistence of real numbers (see [5]).

• e. Closed and separably closed sets in ${\mathbb R}$ (see [3, §2]).

In each case, the theorem at hand allows one to define the range of functions, or separate the disjoint ranges of functions. The proofs in the indicated references then generalise as in the previous sections.

Secondly, we discuss possible alternative approaches, and why they are not fruitful. Now, recursive counterexamples often give rise to Brouwerian counterexamples, and vice versa (see [7, p. xii] for this opinion). A Brouwerian counterexample to a theorem shows that the latter is rejected in (a certain strand of) constructive mathematics (see [17] for details). We choose to use recursive counterexamples (and the associated RM results) because those are formulated in a formal system, which enables us to lift the associated proofs without too much trouble. The same would not be possible for Brouwerian counterexamples, due to the lack of an explicit/unified choice of formal system for e.g. Bishop’s constructive mathematics. To be absolutely clear, there is nothing wrong with constructive mathematics in general; however, the lack of an explicit/unified formal system for constructive mathematics means that we cannot ‘lift’ Brouwerian counterexamples with the same ease (or at all).

4.2 Implications and Interpretations

While we initially had no intention of discussing the implications of the above results in this paper, at least two colleagues have provided interpretations that do not do the justice to the bigger picture provided by [19] and [24]. This section is an attempt at avoiding further misconceptions.

In our opinion, one reasonable interpretation of the results in this paper is that second- and higher-order arithmetic are not as different as sometimes claimed, and that recursive counterexamples and reversals provide a bridge of sorts between the two. However, the results in this paper do not support the argument that higher-order arithmetic contains ‘nothing new’ compared to second-order arithmetic. The exact opposite is the case, as follows; associated results may be found in [19] and [24].

In a nutshell, Kohlenbach’s higher-order RM (see Sect. 2.1) is based on comprehension and discontinuity, while the aforementioned principles $\textsf {BOOT}$, $\textsf {HBU}$, and $\textsf {SEP} ^{1}$ cannot be captured well in this hierarchy, necessitating a new ‘continuity’ hierarchy based on the neighbourhood function principle $\textsf {NFP}$, as first developed in [24]. Let us discuss the previous sentence in a lot more detail.

First of all, as noted in Sect. 2.2, Kohlenbach’s counterpart of arithmetical comprehension $\textsf {ACA} _{0}$ is given by $(\exists ^{2})$, and the functional in the latter is clearly discontinuous. As shown in [16, §3], this axiom is also equivalent to e.g. the existence of a discontinuous function on ${\mathbb R}$. As expected, $\textsf {ECF}$ converts $(\exists ^{2})$ to ‘$0=1$’, as a discontinuous function does not have a continuous representation by an RM-code. The same holds for the higher-order versions of $\varPi _{k}^{1}\text {-}\textsf {CA }_{0}$ mutatis mutandis; the higher-order version of $\varPi _{1}^{1}\text {-}\textsf {CA} _{0}$ is given by the Suslin functional. In a nutshell, Kohlenbach’s higher-order comprehension is based on discontinuity.

Secondly, one of the main (conceptual) results of [19] is that higher-order comprehension does not capture e.g. Heine-Borel compactness well at all. Indeed, while $\textsf {Z}_{2}^{\varOmega }$ proves $\textsf {HBU}$, the system $\textsf {Z}_{2}^{\omega }\equiv \cup _{k}\varPi _{k}^{1}\text {-}\textsf {CA }_{0}^{\omega }$ does not; note that $\varPi _{k}^{1}\text {-}\textsf {CA }_{0}^{\omega }$ is plus the existence of a type two functional deciding $\varPi _{k}^{1}$-formulas (allowing for type zero and one parameters only). The same holds for $\textsf {BOOT}$ and related theorems like the Lindelöf lemma for Baire space (see [19] for the latter). Since all the aforementioned axioms have relatively weak first-order strength (at most $\textsf {ACA} _{0}$) in isolation, higher-order comprehension seems unsuitable for capturing them. By contrast, we show in [24] that these axioms are equivalent to natural fragments of the neighbourhood function principle $\textsf {NFP}$, which is as follows:

$$\begin{aligned} (\forall f^{1})(\exists n^{0})A(\overline{f}n)\rightarrow (\exists \gamma \in K_{0})(\forall f^{1})A(\overline{f}\gamma (f)), \end{aligned}$$

(13)

for any formula $A\in \textsf {L }_{\omega }$ and where ‘$\gamma \in K_{0}$’ means that $\gamma ^{1}$ is a total associate/RM code on ${\mathbb N}^{{\mathbb N}}$. Thus, (13) expresses the existence of a continuous choice function. In a nutshell, $\textsf {NFP}$ is based on continuity and $\textsf {ECF}$ converts $\textsf {NFP}$, $\textsf {BOOT}$, and $\textsf {HBU}$ to resp. $\textsf {Z}_{2}$, $\textsf {ACA} _{0}$, and $\textsf {WKL} _{0}$.

In conclusion, while comprehension is generally a great axiom schema for classifying theorems in RM (of any order), principles like $\textsf {BOOT}$ and $\textsf {HBU}$ do not have a nice classification based on Kohlenbach’s higher-order comprehension. By contrast, the latter do have a nice classification based on $\textsf {NFP}$. Now, higher-order comprehension amounts to discontinuity, while $\textsf {NFP}$ is a continuity schema, stating as it does the existence of a continuous choice function. In this light, higher-order arithmetic includes (at least) two ‘orthogonal’ scales (one based on continuity, one based on discontinuity) for classifying theorems. The ‘liftings’ in this paper generalise second-order theorems to higher-order theorems from the $\textsf {NFP}$-scale with little modification. One disadvantage is that the ‘lifted’ proofs from this paper often use more comprehension or countable choice than the known proofs, as discussed in Sect. 3.1.