Banach’s theorem in higher-order reverse mathematics

Abstract

In this paper, methods of second-order and higher-order reverse mathematics are applied to versions of a theorem of Banach that extends the Schröder–Bernstein theorem. Some additional results address statements in higher-order arithmetic formalizing the uncountability of the power set of the natural numbers. In general, the formalizations of higher-order principles here have a Skolemized form asserting the existence of functionals that solve problems uniformly. This facilitates proofs of reversals in axiom systems with restricted choice.

Keywords

Reverse mathematics Weihrauch reducibility bijection metric spaces

1. Introduction

The Schröder–Bernstein theorem is a well-known result about cardinality. In full generality, it states that if A and B are sets, there is an injection $f : A \to B$ , and there is an injection $g : B \to A$ , then there is a bijection from A to B. Unfortunately, this theorem is not ideal for reverse mathematics analysis. If we add the assumption that $A, B \subseteq N$ , the result is computationally trivial: whenever $A, B \subseteq N$ have the same cardinality, there is an $(A \oplus B)$ -computable bijection between them.

In higher-order reverse mathematics, we might consider the case where $A, B \subseteq 2^{N}$ or $A, B \subseteq N^{N}$ . In this setting, the Schröder–Bernstein theorem is no longer trivial. However, because the theorem does not postulate any relationship between the bijection being constructed and the original two injections, obtaining reversals presents a challenge.

Our focus is a classical theorem of Banach [1] from 1924 more suited to reverse mathematical analysis. Banach argued this theorem captures the essence of proofs of the Schröder–Bernstein theorem, such as the well known proof by Julius König.

Theorem 1.1 (Banach).

If A and B are sets, $f : A \to B$ is an injection, and $g : B \to A$ is an injection, there are decompositions $A = A_{1} \cup A_{2}$ and $B = B_{1} \cup B_{2}$ such that $A_{1} \cap A_{2} = \emptyset$ , $B_{1} \cap B_{2} = \emptyset$ , $f (A_{1}) = B_{1}$ , and $g (B_{2}) = A_{2}$ .

Restating this in terms of the existence of a bijection gives a corollary that strengthens the Schröder–Bernstein theorem, which we will also call Banach’s Theorem.

Corollary 1.2.
If f is an injection from a set A to a set B, and g is an injection from B to A, there is a bijection $h : A \to B$ such that, whenever $h (a) = b$ , either $f (a) = b$ or $g (b) = a$ .

A brief history of Banach’s Theorem and the Schröder–Bernstein theorem is given by Remmel [16]. A version of Banach’s Theorem is studied in [13]. An early analysis of Banach’s Theorem for subsets of $N$ , using subsystems of second-order arithmetic, appears in Hirst’s thesis [7, §3.2] and a related article [8]. That development uses symmetric marriage theorems to prove the following second-order arithmetic results.
Theorem 1.3 ([8, Theorem 4.1]).

${RCA}_{0}$ proves the following are equivalent:

${ACA}_{0}$ .

(Countable Banach’s Theorem) Let $f : N \to N$ and $g : N \to N$ be injections. Then there is a bijection $h : N \to N$ such that for all m and n, $h (n) = m$ implies either $f (n) = m$ or $g (m) = n$ .

Theorem 1.4 ([8, Theorem 4.2]).

${RCA}_{0}$ proves the following are equivalent:

${WKL}_{0}$ .

(Bounded Countable Banach’s Theorem) Let $f : N \to N$ and $g : N \to N$ be injections such that the ranges of f and g exist. Then there is a bijection $h : N \to N$ such that for all m and n, $h (n) = m$ implies either $f (n) = m$ or $g (m) = n$ .

In this paper, we use methods from higher-order reverse mathematics to study the uniformity of results like these. We are interested not only in the existence of the bijection h, but also whether there is a functional that can produce h uniformly from f and g. This question of uniformity is purely higher-order, and cannot be expressed directly in second-order reverse mathematics. To study this uniformity, we examine Skolemized versions of theorems. For example, instead of examining Banach’s Theorem in a form such as $\begin{matrix} (\forall f, g, A, B) (\exists h) Φ (f, g, A, B, h), \end{matrix}$ we consider the form $\begin{matrix} (1) & (\exists H) (\forall f, g, A, B) Φ (f, g, A, B, H (f, g, A, B)) . \end{matrix}$

Both versions of a theorem are of interest, of course, and the latter always follows from the former if we assume sufficient choice principles. We are interested in the Skolemized forms because they represent a particular kind of uniformity, and we typically do not assume enough choice to derive them directly from the un-Skolemized form. As discussed in Section 5, this is a different kind of uniformity than Weihrauch reducibility.

Kohlenbach studies the reverse mathematics of Skolemized forms like equation (1) for basic mathematical theorems in [10,12]. Similar functional existence statements have been studied by other authors, including Sakomoto and Yamazaki [17]. A central technique is Grilliot’s trick, a method for effectively deriving a uniform, functional existence version of arithmetical comprehension from the existence of discontinuous functions (on the reals or on Baire space).

Section 3 begins with a survey of reverse mathematics results on countability. Sections 4 and 5 present a number of supporting lemmas to prepare for the analysis of Banach’s theorem. Section 6 examines Theorems 1.3 and 1.4 from the viewpoint of Skolemized uniformity. Section 7 extends the study of Banach’s Theorem to subsets of $2^{N}$ and, more generally, subsets of compact metric spaces. Finally, Section 8 discusses moduli of uniform continuity and a fan functional.

2. Formal theories

This work relies on several well studied systems of second-order arithmetic and higher-order arithmetic. Simpson [18] and Dzhafarov and Mummert [3] provide thorough references for reverse mathematics. Kohlenbach [12] provides a reference for higher-order reverse mathematics. We follow Kohlenbach’s definitions of higher-order systems throughout this paper, noting any exceptions explicitly.

For the purposes of higher-order reverse mathematics, we assume that our systems use the function based language of higher-order arithmetic, rather than the set based language. Accordingly, $2^{N}$ is used throughout this paper to denote the set of all functions from $N$ to ${0, 1}$ .

Many of our results will use fragments of the quantifier-free choice scheme. For types ρ and τ, we have the scheme $\begin{matrix} QF - {AC}^{ρ, τ} : (\forall x^{ρ}) (\exists y^{τ}) A (x, y) \to (\exists Y^{ρ \to τ}) (\forall x^{ρ}) A (x, Y (x)), \end{matrix}$ where A is a quantifier free formula. Here A can have parameters of arbitrary type.

The system ${RCA}_{0}^{ω} = E - {PRA}^{ω} + QF - {AC}^{1, 0}$ is a fragment of higher-order arithmetic. It can be axiomatized by a set of basic axioms along with induction for $Σ_{1}^{0}$ formulas and the choice scheme $QF - {AC}^{1, 0}$ . The syntax has term-forming operations for λ-abstraction and primitive recursion.

The system ${RCA}_{0}^{2}$ is a second-order fragment of ${RCA}_{0}^{ω}$ , with only types 0 and 1 for elements of $N$ and functions $N \to N$ , respectively. Formally, we have ${RCA}_{0}^{2} = E - {PRA}^{2} + QF - {AC}^{0, 0}$ . This system is equivalent to the set based system ${RCA}_{0}$ presented by Simpson [18], and we will henceforth denote ${RCA}_{0}^{2}$ by ${RCA}_{0}$ when no confusion is likely.

A sequence $⟨ f_{n} : n \in N ⟩$ is viewed as a map $f : N \times N \to N$ , so that $f_{n} (m) = f (⟨ n, m ⟩)$ , where $⟨ \cdot, \cdot ⟩$ is a suitable pairing function.

Emulating Kohlenbach [12], we use parentheses around the name of a functional to denote the principle stating that the functional exists. For example, the principle $(\exists^{2})$ asserts the existence of the functional $\exists^{2}$ , defined below.

There are several ways to extend the comprehension axioms of second-order arithmetic to the higher-order setting. One particular functional (set) existence axiom for higher-order arithmetic is $(\exists^{2})$ , defined by $\begin{matrix} (\exists^{2}) : (\exists φ^{1 \to 0}) (\forall f^{1}) (φ (f) = 0 \leftrightarrow (\exists n) [f (n) = 0]) . \end{matrix}$ The functional $φ^{1 \to 0}$ from this principle is itself called $\exists^{2}$ . The system ${RCA}_{0}^{ω} + (\exists^{2})$ implies the arithmetical comprehension scheme. Kohlenbach [12] showed that ${RCA}_{0}^{ω} + (\exists^{2})$ is conservative over first order Peano arithmetic.

Other functional existence principles correspond to ${ACA}_{0}$ . Kohlenbach [12] presents two such functionals. One, $μ_{0}$ , selects a zero of a function if such a zero exists: $\begin{matrix} (μ_{0}) : (\exists μ_{0}^{2}) (\forall f^{1}) [(\exists n^{0}) (f (n) =_{0} 0) \to f (μ_{0} (f)) = 0] . \end{matrix}$ Another returns the least zero of a function, in the fashion of Hilbert and Bernays [6, page 411], also used by Feferman [4, §2.3.3]: $\begin{matrix} (μ) : (\exists μ^{2}) (\forall f^{1}) ((\exists n^{0}) (f (n) =_{0} 0) \to [f (μ (f)) = 0 \land (\forall t < μ (f)) (f (t) \neq 0)]) . \end{matrix}$

Proposition 2.1.
The following are pairwise equivalent over ${RCA}_{0}^{ω}$ : $(\exists^{2})$ , $(μ_{0})$ , and $(μ)$ .
Proof.
Kohlenbach [12, Proposition 3.9] proves the equivalence of $(\exists^{2})$ and $(μ_{0})$ . Because any μ satisfying $(μ)$ also satisfies $(μ_{0})$ , it suffices to show that ${RCA}_{0}^{ω}$ proves that $(μ_{0})$ implies $(μ)$ . Given a functional $μ_{0}$ as in the definition of $(μ_{0})$ , $μ (f)$ is the least $t ⩽ μ_{0} (f)$ such that $f (t) = 0$ . This functional is primitive recursive in $μ_{0}$ and thus exists by ${RCA}_{0}^{ω}$ and $(μ_{0})$ . □

Finally, we note that Grilliot’s trick [5] is an algorithm in computability theory that yields the functional $\exists^{2}$ from any input coding a discontinuous function on Baire space. Kohlenbach [12] shows that Grilliot’s trick can be formalized in ${RCA}_{0}^{ω}$ , so the existence of a discontinuous function (on Baire space or the reals) implies the principle $(\exists^{2})$ .
3. Countability

One motivation for this research is the question: how difficult is it to prove $2^{N}$ is uncountable? As usual, being uncountable simply means not being countable. There are many ways to express the principle that $2^{N}$ is countable, with the following three being particularly natural:

$C_{enum}$ : there is a sequence $⟨ f_{n} : n \in N ⟩$ such that for all $g \in 2^{N}$ there is an $n \in N$ with $g = f_{n}$ .

$C_{inj}$ : there is a functional $Φ^{1 \to 0}$ that is an injection from $2^{N}$ to $N$ .

$C_{bij}$ : there is a functional $Φ^{1 \to 0}$ that is a bijection from $2^{N}$ to $N$ .

The principles $C_{inj}$ and $C_{bij}$ cannot be stated in the language of second-order arithmetic, but they can be stated in ${RCA}_{0}^{ω}$ . When we say we assume $C_{inj}$ or $C_{bij}$ , this means we assume the existence of a functional with the property stated. Similarly, if we assume $\neg C_{inj}$ or $\neg C_{bij}$ , this means we assume no functional has the property stated.

In context of set theory there is little reason to distinguish between $C_{inj}$ and $C_{bij}$ , because of the comprehension principles available. As discussed below, there are key distinctions between these principles in the context of theories of arithmetic with restricted comprehension principles.

Of course, $C_{enum}$ , $C_{bij}$ , and $C_{inj}$ are classically false. There are two key questions: which systems are “strong enough” to disprove these false principles, and which are “weak enough” to be consistent with one or more of the principles. As is well known, Cantor’s diagonalization proof allows us to disprove $C_{enum}$ in very weak systems (compare Theorem II.4.9 of Simpson [18] showing $R$ is not denumerable in ${RCA}_{0}$ ).

Proposition 3.1.
${RCA}_{0}^{2}$ proves $\neg C_{enum}$ .
Proof.
Given $⟨ f_{n} : n \in N ⟩$ witnessing $C_{enum}$ , ${RCA}_{0}^{2}$ can construct the function g defined by $g (m) = 1 - f_{m} (m)$ . Then $g \in 2^{N}$ , but g cannot be $f_{k}$ for any $k \in N$ . □

The principles $C_{inj}$ and $C_{bij}$ have much more interesting behavior. Normann and Sanders [14] provide a detailed analysis of the negations of these principles, which they name $NIN$ and $NBI$ , respectively. (They formulate $NIN$ and $NBI$ for $R$ but the results hold equally for $2^{N}$ .) Normann and Sanders work in extensions of $Z_{2}$ , $Z_{2}^{ω}$ , and $Z_{2}^{Ω}$ , all of which prove the same second-order sentences, as shown in the thesis of Hunter [9]. Their Theorem 3.2 shows that the true principle $NIN$ is not provable in the system $Z_{2}^{ω} + QF - {AC}^{0, 1}$ (which includes third-order functionals deciding $Π_{k}^{1}$ formulas and consequently includes $Π_{\infty}^{1}$ comprehension with parameters of type 1), and hence this system is consistent with $C_{inj}$ [14, Theorem 3.26]. They also show that $NIN$ is provable in $Z_{2}^{Ω} + QF - {AC}^{0, 1}$ , a subsystem that includes the functional $\exists^{3}$ , a functional that emulates $\exists^{2}$ for inputs of type $1 \to 0$ . This subsystem includes $Π_{\infty}^{1}$ comprehension. In the remainder of this section, we discuss some aspects of their results related to $C_{inj}$ and $C_{bij}$ .

A key issue in analyzing $C_{inj}$ is that the range of an injection from $N^{N}$ to $N$ may be hard to form with weak comprehension axioms. We will see that a similar issue arises in the study of Banach’s theorem, as well, where the existence of the range of a functional becomes a key question. By contrast, $C_{bij}$ can be disproved using the weak choice principle $NCC$ [14, Theorem 3.28]. The following short disproof of $C_{bij}$ uses more choice.
Proposition 3.2 ( ${RCA}_{0}^{ω} + QF - {AC}^{0, 1}$ ).

There is no injection $Φ : 2^{N} \to N$ for which the characteristic function for the range exists. In particular, $C_{bij}$ is disprovable in ${RCA}_{0}^{ω} + QF - {AC}^{0, 1}$ .

Proof.
We will work in ${RCA}_{0}^{ω} + QF - {AC}^{0, 1}$ and assume there is a bijection Φ from $2^{N}$ to $N$ with range $D = {n : (\exists g) [Φ (g) = n]}$ given by a characteristic function. We will prove the principle $C_{enum}$ by constructing a kind of left inverse of Φ, which will be a (possibly noninjective) enumeration of $2^{N}$ . Because ${RCA}_{0}$ proves $\neg C_{enum}$ , this gives a contradiction.

By assumption, for each $n \in D$ there is a $g \in 2^{N}$ with $Φ (g) = n$ . Therefore, by $QF - {AC}^{0, 1}$ , we may form a function f so that $(\forall n) [n \in D \to Φ (f_{n}) = n]$ . Then $⟨ f_{n} : n \in N ⟩$ is an enumeration of $2^{N}$ , so $C_{enum}$ holds, a contradiction. □

We now explain how the lemma implies certain higher-order formulations of the Schröder–Bernstein theorem are nontrivial. Suppose, in the context of set theory, we wanted to try to use the Schröder–Bernstein theorem to show $2^{N}$ is countable. Because there is a trivial injection from $N$ to $2^{N}$ , the other assumption in the Schröder–Bernstein theorem is the existence of an injection from $2^{N}$ to $N$ , that is, $C_{inj}$ . The conclusion is the existence of a bijection, that is, $C_{bij}$ . We can thus view the implication $C_{inj} \to C_{bij}$ as a specific formal instance of the Schröder–Bernstein theorem. (Normann and Sanders [13] study a different formulation of the Schröder–Bernstein theorem, which they call $CB N$ .)
Corollary 3.3.
The implication $C_{inj} \to C_{bij}$ is not provable in $Z_{2}^{ω} + QF - {AC}^{0, 1}$ .
Proof.
$Z_{2}^{ω} + QF - {AC}^{0, 1}$ is consistent with $C_{inj}$ but not $C_{bij}$ . □

Lemma 3.2 can also be used to obtain an upper bound on the strength required to disprove $C_{inj}$ . Normann and Sanders [14] provide many examples of third-order theorems that disprove $C_{inj}$ . Among them is a version of the following lemma using the principle $(\exists^{3})$ as a formalization of $Σ_{1}^{1}$ comprehension with functional parameters.
Corollary 3.4 (See Theorem 3.1 of Normann and Sanders [14]).

$C_{inj}$ is disprovable from ${RCA}_{0} + QF - {AC}^{0, 1}$ along with $Σ_{1}^{1}$ comprehension with parameters of type 2.

Proof.
Assume Φ is a functional witnessing $C_{inj}$ . Applying $Σ_{1}^{1}$ comprehension with parameter Φ, we can construct the range of Φ. We then obtain a contradiction from Proposition 3.2. □

A final point of interest is that the classically false principle $C_{inj}$ , although consistent with ${RCA}_{0}^{ω}$ , has nontrivial set existence strength. Normann and Sanders discuss the contrapositive of the following proposition in the guise of a “trick” related to excluded middle [14, §3].
Proposition 3.5.
$C_{inj}$ implies $(\exists^{2})$ over ${RCA}_{0}^{ω}$ .
Proof.
If Φ is an injection from $2^{N}$ to $N$ then Φ is discontinuous at every point (here we identify elements of $N$ with constant functions from $N$ to $N$ ). The existence of a discontinuous functional implies $(\exists^{2})$ by [12, Proposition 3.7] of Kohlenbach. □

Thus, for example, there is no model of ${RCA}_{0}^{ω}$ in which $C_{inj}$ holds and every element of $2^{N}$ is computable.
4. Bounding calculations of type 1 functions

This section contains several technical lemmas related to the range of a function $f : N \to N$ . Each function of this type has a number of auxiliary functions related to its range. The most obvious is the characteristic function for the range. We write $ρ (f, g)$ as shorthand for the formula asserting that g is the characteristic function for the range of f. More formally, $\begin{matrix} (2) & ρ (f, g) is (\forall n) [(\exists m) (f (m) = n) \leftrightarrow g (n) > 0] . \end{matrix}$ A bounding function can also be used to compute the range of f. We write $β (f, g)$ for the formula asserting that g is such a bounding function. Formally, $\begin{matrix} (3) & β (f, g) is (\forall n) [(\exists m) (f (m) = n) \leftrightarrow (\exists t ⩽ g (n)) (f (t) = n)] . \end{matrix}$

The results below address the problem of converting between the characteristic function for the range of a function and a bounding function for the range, and the amount of uniformity present in the conversion. In the second-order setting, principles asserting the existence of characteristic functions and the existence of bounding functions are interchangeable, as shown by the following two results.

Proposition 4.1 ( ${RCA}_{0}$ ).

For all $f : N \to N$ , $(\exists g) ρ (f, g) \leftrightarrow (\exists h) β (f, h)$ .

Proof.
Working in ${RCA}_{0}$ , suppose g is a characteristic function for the range of a function f. Then $h (n) = (μ t) (g (n) = 0 \lor f (t) = n)$ is the desired bounding function and exists by recursive comprehension.

Now suppose that h is a bounding function for the range of f. The characteristic function $g : N \to N$ can be defined by the formula $\begin{matrix} g (n) = \{\begin{matrix} 1, & if (\exists t ⩽ h (n)) (f (t) = n), \\ 0, & otherwise, \end{matrix} \end{matrix}$ and hence g exists by recursive comprehension. □

The relationship between characteristic and bounding functions is uniform in the sense that ${RCA}_{0}$ proves the sequential extension of the previous result.
Proposition 4.2 ( ${RCA}_{0}$ ).

For every sequence ${⟨ f_{i} ⟩}_{i \in N}$ of functions from $N$ to $N$ , we have $\begin{matrix} (\exists {⟨ g_{i} ⟩}_{i \in N}) (\forall n) ρ (f_{n}, g_{n}) \leftrightarrow (\exists {⟨ h_{i} ⟩}_{i \in N}) (\forall n) β (f_{n}, h_{n}) . \end{matrix}$

Proof.
We will write ${⟨ f_{i} ⟩}_{i \in N}$ as a function of two variables, so $f (i, n) = f_{i} (n)$ . Adapting the proof of the preceding result, write $\begin{matrix} h (i, n) = (μ t) (g (i, n) = 0 \lor f (i, t) = n) \end{matrix}$ and $\begin{matrix} g (i, n) = \{\begin{matrix} 1, & if (\exists t ⩽ h (i, n)) (f (i, t) = n), \\ 0, & otherwise, \end{matrix} \end{matrix}$ to translate the sequences of auxiliary functions in ${RCA}_{0}$ . □

Third order arithmetic can formalize “translating functionals” of type 2 to convert between characteristic functions and bounding functions for ranges. Principles asserting the existence of the translating functionals provide additional examples of Skolemized uniformity, distinct from the sequential uniformity often considered in second-order settings.

As shown below, the existence of a translating functional from bounding functions to characteristic functions can be proved in ${RCA}_{0}^{ω}$ . However, the reverse translation functional requires stronger assumptions. Thus the interchangeability of the two sorts of auxiliary functions witnessed in the second-order setting by the previous two propositions does not extend to Skolemized functional formulations in third order arithmetic.
Proposition 4.3 ( ${RCA}_{0}^{ω}$ ).

There is a functional $T_{β \to ρ}$ of type $1 \to 1$ that translates bounding functions into characteristic functions for ranges. That is, $\begin{matrix} (\exists T_{β \to ρ}) (\forall f) (\forall g) [β (f, g) \to ρ (f, T_{β \to ρ} (f, g))] . \end{matrix}$

Proof.
Working in ${RCA}_{0}^{ω}$ , by $QF - {AC}^{1, 0}$ there is a functional Y from $N^{< N} \times N^{< N} \times N$ to ${0, 1}$ such that $Y (f, g, n) = 1$ if and only if $(\exists t ⩽ g (n)) [f (t) = n]$ . Note that the defining formula is quantifier free because the bounded quantifier can be rewritten using a primitive recursive functional. The desired functional $T_{β \to ρ} (f, g)$ is then $\begin{matrix} T_{β \to ρ} (f, g) = λ n . Y (f, g, n) . \end{matrix}$ □
Proposition 4.4 ( ${RCA}_{0}^{ω}$ ).

The following are equivalent:

$(\exists^{2})$ .

There is a functional $T_{ρ \to β}$ of type $1 \to 1$ that translates characteristic functions for ranges into bounding functions. That is: $\begin{matrix} (\forall f) (\forall g) [ρ (f, g) \to β (f, T_{ρ \to β} (f, g))] . \end{matrix}$

Proof.
To prove that (1) implies (2), assume ${RCA}_{0}^{ω} + (\exists^{2})$ . The base system ${RCA}_{0}^{ω}$ suffices to prove the existence of the functional χ which takes the (type 1 code for the) pair $(f, n)$ and maps it to the function $f_{n} : N \to 2$ satisfying $f_{n} (t) = 0 \leftrightarrow f (t) = n$ . By [12, Proposition 3.9] of Kohlenbach, $(\exists^{2})$ implies the existence of Feferman’s μ functional satisfying the formula $\begin{matrix} (\forall f) [(\exists x) (f (x) = 0) \to f (μ (f)) = 0] . \end{matrix}$ The function $T_{β \to ρ} (f, g) = μ (χ (f, n))$ is the desired bounding function, and exists by composition.

In the proof of the preceding implication, the principle $(\exists^{2})$ is sufficiently strong that we can discard the given characteristic function and calculate the bounding function directly from f and $\exists^{2}$ . We now show we can calculate $\exists^{2}$ from any translation functional $T_{ρ \to β}$ in the reverse direction.

To prove that (2) implies (1), suppose $T_{ρ \to β}$ is a translation functional as described in (2). We will show that this functional is not $ε - δ$ continuous in the usual sense (see [12, Definition 3.5] of Kohlenbach).

We can view inputs f and g as a single sequence $⟨ f (0), g (0), f (1), g (1) \dots ⟩$ and use the usual Baire space topology. The functional $T_{ρ \to β}$ is defined for every input of two type 1 arguments, including inputs f and g for which g is not a characteristic function for the range of f. For example, let $f_{1} : N \to N$ satisfy $f_{1} (n) = 1$ for all n. Let $g_{2} : N \to N$ satisfy $g_{2} (0) = g_{2} (1) = 1$ and $g_{2} (n) = 0$ otherwise. Then $g_{2}$ is not a correct characteristic function for $f_{1}$ . However, $T_{ρ \to β} (f_{1}, g_{2}) = h$ for some totally defined type 1 function h, and $h (0) = b$ for some value b.

Suppose by way of contradiction that $T_{ρ \to β}$ is $ε - δ$ continuous. Then for every pair $(f, g)$ in some neighborhood N of $(f_{1}, g_{2})$ we must have $T_{ρ \to β} (f, g) (0) = b$ . Let $f_{2} : N \to 2$ be a function that is 1 for every $t ⩽ b$ , outputs a sufficient number of ones so that $(f_{2}, g_{2})$ is in the neighborhood N, and is eventually constantly zero. Then $g_{2}$ is a correct characteristic function for $f_{2}$ , so $ρ (f_{2}, g_{2})$ holds. However, $T_{ρ \to β} (f_{2}, g_{2}) (0) = b$ . Thus $T_{ρ \to β} (f_{2}, g_{2})$ is not a bounding function for $f_{2}$ because $(\exists t) [f_{2} (t) = 0]$ but $(\forall t ⩽ T_{ρ \to β} (f_{2}, g_{2}) (0)) [f_{2} (t) \neq 0]$ . Thus $β (f_{2}, T_{ρ \to β} (f_{2}, g_{2}))$ fails. This contradicts the implication given in item (2) of the proposition. Thus $T_{ρ \to β}$ must not be $ε - δ$ continuous. By [12, Proposition 3.7] of Kohlenbach, $(\exists^{2})$ follows via Grilliot’s trick. □

Let R be the Weihrauch problem taking a type 1 function as an input and yielding output consisting of the characteristic function of the range of the input. Let B be the Weihrauch problem that outputs bounding functions as described above. Ideas from the proof of Proposition 4.1 can be adapted to show that R and B are weakly Weihrauch equivalent, and strongly Weihrauch incomparable. Summarizing, analyses based on sequential second-order statements, Skolemized higher-order statements, and Weihrauch reducibility yield different results. This indicates that there are three distinct notions of uniformity considered here.
5. Realizers for omniscience principles

The principle $(\exists^{2})$ is closely related to a certain formulation of the limited principle of omniscience. The Weihrauch problem $LPO$ asks for a realizer that determines whether an infinite sequence of natural numbers contains a zero. Indeed, the definition of $(\exists^{2})$ could be rewritten as $\begin{matrix} (\exists^{2}) : (\exists R_{LPO}) (\forall f^{1}) [R_{LPO} (f) = 0 \leftrightarrow (\exists n) (f (n) = 0)] \end{matrix}$ to emphasize $(\exists^{2})$ asserts the existence of a realizer for this problem,

The Weihrauch problem $LLPO$ , related to the lesser limited principle of omniscience, asks for a realizer to identify a parity (even or odd) on which a sequence of numbers is zero, assuming either that all even positions are zero or all odd positions are zero. We will use a principle asserting the existence of a realizer for $LLPO$ : $\begin{matrix} (LLPO) : (\exists R_{LLPO} ⩽ 1) (\forall f^{1}) ([(\forall n) (f (2 n) = 0) \lor (\forall n) (f (2 n + 1) = 0)] \to (\forall n) [f (2 n + R_{LLPO} (f)) = 0]) . \end{matrix}$ Often it is more convenient to work with an equivalent form that asks for the parity of the first location where a sequence is zero, if there is such a location: $\begin{matrix} (LLPOmin) : (\exists R_{LLPOmin}) (\forall f^{1}) (\forall n) [f (n) = 0 \to R_{LLPOmin} (f) \equiv_{mod 2} (μ t ⩽ n) (f (t) = 0)] . \end{matrix}$

For example, suppose $f = ⟨ 1, 0, 1, 0, 0 \dots ⟩$ denotes the infinite sequence consisting of 1, 0, 1 followed by all zeros. Then $R_{LPO} (f) = 1$ because the sequence contains a 0; $R_{LLPO} (f) = 1$ because $f (2 n + 1) = 0$ for all n; and $R_{LLPOmin} (f) = 1$ because the first zero occurs in position 1, which is odd. For the sequence $g = ⟨ 1, 1, 0, 0, \dots ⟩$ , $R_{LPO} (g) = 1$ ; $R_{LLPOmin} = 0$ because the first zero occurs at position 2, which is even; and the value of $R_{LLPO}$ is not determined by its defining formula.

One motivation of $LLPOmin$ is that its value is determined for every sequence that includes a zero. The next proposition shows that $LLPO$ and $LLPOmin$ are equivalent for our purposes. For Weihrauch problems $P$ and $Q$ expressible in the language of ${RCA}_{0}^{ω}$ , we say that ${RCA}_{0}^{ω}$ proves $P ⩽_{sW} Q$ if ${RCA}_{0}^{ω}$ proves there are functionals $φ, ψ : N^{N} \to N^{N}$ such that, for every realizer $R_{Q}$ of $Q$ , the functional $ψ \circ R_{Q} \circ φ$ is a realizer of $P$ .

Proposition 5.1.
${RCA}_{0}^{ω}$ proves that the problems $LLPO$ and $LLPOmin$ are strongly Weihrauch equivalent, and that the principles $(LLPO)$ and $(LLPOmin)$ are equivalent.
Proof.
First, assume R is a realizer for $LLPOmin$ . Define a pre-processing function $h : N \to N$ such that $h (n) = 0$ if $n \neq 0$ and $h (0) = 1$ . Define a post-processing function $w (n) = 1 - (n mod 2)$ . Then $S = w \circ R \circ h$ is a realizer for $LLPO$ .

To see this, assume g is an instance of $LLPO$ . If g is identically zero, then whichever value in ${0, 1}$ is produced by S is acceptable. If g is not identically zero, then $h \circ g$ is zero on exactly the inputs where g is nonzero. Thus $R (h \circ g)$ is the parity of the first location where g is nonzero, and $w \circ R (h \circ g)$ is the parity for which g is always zero. This shows $LLPO ⩽_{sW} LLPOmin$ .

Conversely, suppose S is a realizer for $LLPO$ . Define a pre-processing function $J : N^{N} \to N^{N}$ such that, for $f \in N^{N}$ , $\begin{matrix} J (f) (n) = \{\begin{matrix} 1, & if (\exists m < n) (f (m) = 0), \\ f (n), & otherwise . \end{matrix} \end{matrix}$ Thus $J (f)$ and f agree through the first zero of f, but afterwards $J (f)$ takes only the value 1. Hence there is at most one input k for which $h (J (f)) (k)$ is nonzero, and if there is such a k then it is the least input for which $f (k) = 0$ . This means that $h (J (f))$ is in the domain of $LLPO$ , and $S (h (J (f)))$ produces the parity of k. Thus $S \circ (h \circ J)$ is a realizer for $LLPOmin$ . We have shown $LLPOmin ⩽_{sW} LLPO$ .

The pre-processing and post-processing functionals in this argument can all be formed in ${RCA}_{0}^{ω}$ , which can verify the correctness of the argument. None of the post-processing functions require access to the original instance of a problem. Hence ${RCA}_{0}^{ω}$ proves that $LLPO$ or $LLPOmin$ are strongly Weihrauch equivalent.

Concatenation of the pre-processing and post-processing functionals with any $LLPO$ realizer yields an $LLPOmin$ realizer, so the principle $(LLPO)$ implies the principle $(LLPOmin)$ . The converse follows in a similar fashion. □

Results of Weihrauch analysis include $LLPO <_{W} LPO$ and the parallelized form $\hat{LLPO} <_{W} \hat{LPO}$ . See Weihrauch [19, §4] and Brattka and Gherardi [2, Theorem 7.13] for proofs. Consequently, the following result may initially be surprising. The underlying difference is that Weihrauch reducibility requires a single reduction that works for all realizers; the argument below breaks into cases depending on the behavior of the realizer.
Proposition 5.2 ( ${RCA}_{0}^{ω}$ ).

$(LLPO)$ implies $(\exists^{2})$ .

Proof.
Working in ${RCA}_{0}^{ω}$ , by Proposition 5.1, it is sufficient to assume the existence of $R = R_{LLPOmin}$ as provided by $(LLPOmin)$ , and prove $(\exists^{2})$ holds.

Let $f = ⟨ 1, 1, 1 \dots ⟩$ be the infinite sequence of ones. Our goal is to show that R is sequentially discontinuous at f. We will construct a sequence $⟨ g_{n} ⟩$ such that ${lim}_{n \to \infty} g_{n} = f$ and for each n, $R (g_{n})$ disagrees with $R (f)$ . In particular, if $R (f) = 1$ , we want $R (g_{n}) = 0$ for all n, so we define $g_{n}$ as a sequence of $2 + 2 n$ ones followed by all zeros. On the other hand, if $R (f) = 0$ , we want $R (g_{n}) = 1$ for all n, so we define $g_{n}$ as a sequence of $1 + 2 n$ ones followed by all zeros. Summarizing, for each n and m we have $\begin{matrix} g_{n} (m) = \{\begin{matrix} 1, & if m < 1 + R (f) + 2 n, \\ 0, & otherwise . \end{matrix} \end{matrix}$ Note that ${RCA}_{0}^{ω}$ proves the existence of the sequence $⟨ g_{n} ⟩$ , that ${lim}_{n \to \infty} g_{n} = f$ , and that for all n, $R (g_{n}) \neq R (f)$ . Thus R is sequentially discontinuous and $(\exists^{2})$ follows by [12, Proposition 3.7] of Kohlenbach.

The proof of Kohlenbach’s proposition is based on the proof of Lemma 1 of Grilliot [5]. We append that argument here to give a direct derivation of $(\exists^{2})$ from $(LLPOmin)$ . Let the function f and the sequence $⟨ g_{n} ⟩$ be defined as above. The system ${RCA}_{0}^{ω}$ suffices to prove the existence of the operator $J : N^{N} \to 2^{N}$ defined for $h : N \to N$ and $j \in N$ by $\begin{matrix} J (h) (j) = \{\begin{matrix} 1, & if (\forall x ⩽ j) [h (x) \neq 0], \\ g_{i}, & if i ⩽ j \land i = (μ t) [h (t) = 0] . \end{matrix} \end{matrix}$ Note that $J (h) = f$ if $(\forall x) [h (x) \neq 0]$ . On the other hand, if i is the least value for which $h (i) = 0$ , then $J (h) = g_{i}$ . Consequently, for all $h : N \to N$ , $R (J (h)) = R (f)$ if and only if $(\forall x) [h (x) \neq 0]$ . Thus $R_{LPO} (h) = 1 - | R (J (h)) - R (f) |$ , so the existence of $R_{LPO}$ follows by ${RCA}_{0}^{ω}$ . □
Theorem 5.3 ( ${RCA}_{0}^{ω}$ ).

The following are equivalent:

$(\exists^{2})$ .

$(LLPO)$ .

Proof.
To show that (1) implies (2), as noted in Proposition 2.1, [12, Proposition 3.9] of Kohlenbach shows that the principle $(\exists^{2})$ proves the existence of Feferman’s μ functional which satisfies: $\begin{matrix} (\forall f) [(\exists x) (f (x) = 0) \to [f (μ (f)) = 0 \land (\forall t < μ (f)) (f (t) \neq 0)]] \end{matrix}$ The remainder function $rm (n, 2)$ yielding the remainder of dividing n by 2 is primitive recursive. Thus ${RCA}_{0}^{ω}$ proves the existence of the composition functional $rm (μ (f), 2)$ , which satisfies the definition of $(LLPO)$ .

The converse was proved as Proposition 5.2 above. □

For an alternative proof of the forward implication of Theorem 5.3, we can use a formalized Weihrauch reducibility result. The next two results illustrate this process. The following proposition converts formal Weihrauch reducibility to proofs of implications of Skolemized functional existence principles.
Proposition 5.4.
If $P$ and $Q$ are problems and $(P)$ and $(Q)$ are the associated Skolemized functional existence principles, then ${RCA}_{0}^{ω}$ proves $\begin{matrix} P ⩽_{W} Q \to [(Q) \to (P)] . \end{matrix}$
Proof.
Working in ${RCA}_{0}^{ω}$ , suppose $P ⩽_{W} Q$ and $(Q)$ hold. Let φ and ψ be the functionals witnessing $P ⩽_{W} Q$ and let $R_{Q}$ witness $(Q)$ . The system ${RCA}_{0}^{ω}$ proves the existence of the composition $ψ (R_{Q} (φ (x)), x)$ , which can be directly shown to realize the principle $(P)$ . □

Next, we prove the formalized Weihrauch reducibility result corresponding to the forward implication of Theorem 5.3.
Proposition 5.5.
${RCA}_{0}^{ω}$ proves $LLPO ⩽_{sW} LPO$ .
Proof.
We again work with $LLPOmin$ in place of $LLPO$ . Let $φ : N^{N} \to 2^{N}$ be the pre-processing functional defined by: $\begin{matrix} φ (h) (n) = \{\begin{matrix} 1, & if (\forall t ⩽ n) (h (t) > 0), \\ 1, & if (\exists t ⩽ n) (h (t) = 0) and the least such t is odd, \\ 0, & if (\exists t ⩽ n) (h (t) = 0) and the least such t is even. \end{matrix} \end{matrix}$ Note that $φ (h)$ is the sequence of all ones except when the first zero in the range of h occurs in an even location. Define the post-processing functional $ψ (h, n) = n$ . If $R_{LPO}$ is a realizer for $LPO$ , then $ψ (h, R_{LPO} (φ (h))$ is a realizer for $LLPO$ . Because ψ makes no use of h, this shows that $LLPOmin ⩽_{sW} LPO$ . Applying Proposition 5.1, we see that $LLPO ⩽_{sW} LPO$ . □

As mentioned before, the forward implication of Theorem 5.3 follows immediately from Propositions 5.4 and 5.5. The next result uses Theorem 5.3 to give a short proof of one direction of Proposition 3.4 of Kohlenbach [10], showing that a uniform version of weak König’s lemma is equivalent to $(\exists^{2})$ . This equivalence is also included in [12, Proposition 3.9] of Kohlenbach. Kohlenbach emphasizes the uniformity provided by the functional by using $(UWKL)$ to denote the principle $(WKL)$ appearing in the next proposition. We will apply the proposition in the analysis of Banach’s Theorem for $N$ in the next section. (For a discussion of uniform $WWKL$ see Theorem 3.2 of Sakamoto and Yamazaki [17].) Proposition 5.6 ( ${RCA}_{0}^{ω}$ ).

The following are equivalent:

$(\exists^{2})$ .

$(WKL)$ There is a functional $WKL : N^{N} \to 2^{N}$ such that if T is a code for an infinite tree in $2^{N}$ , then $WKL (T)$ is an infinite path in T.

Proof.
As noted in the proof of Proposition 3.4 of Kohlenbach [10], the proof that (1) implies (2) follows from the fact that, given the functional $\exists^{2}$ , primitive recursion can define a functional which selects an infinite branch of an infinite binary tree. For a short proof of the converse, it suffices to show that $(WKL)$ implies $(LLPOmin)$ . Consider an instance $f : N \to 2$ for $LLPOmin$ . Let ${⟨ 1 ⟩}_{n}$ denote the sequence of n ones. Define the $0 - 1$ tree $T_{f}$ by:
Only sequences of the form $0^{⌢} {⟨ 1 ⟩}_{n}$ and $1^{⌢} {⟨ 1 ⟩}_{n}$ are in $T_{f}$ ,

$0^{⌢} {⟨ 1 ⟩}_{n} \in T_{f}$ if and only if either $(\forall t ⩽ n) [f (t) \neq 0]$ or $(μ t ⩽ n) [f (t) = 0]$ is even, and

$1^{⌢} {⟨ 1 ⟩}_{n} \in T_{f}$ if and only if either $(\forall t ⩽ n) [f (t) \neq 0]$ or $(μ t ⩽ n) [f (t) = 0]$ is odd.
${RCA}_{0}^{ω}$ can prove the existence of a functional φ that maps each f to $T_{f}$ . For each f, the first element of $WKL (φ (f))$ is an $LLPOmin$ solution for f. □

6. Banach’s theorem on $N$

This section reformulates Theorems 1.3 and 1.4 as higher-order functional existence statements. In particular, Theorem 6.8 shows that, in the Skolemized higher-order setting, the bounded version is equivalent to the unbounded version. This collapse mimics that of the uniform principle $(WKL)$ . Our discussion begins with the formulation of the bounded principle and its proof from $(WKL)$ .

Definition 6.1.
A bounded Banach functional ${bB}_{N}$ on $N$ is defined as follows. For injective functions $f_{0} : N \to N$ and $f_{1} : N \to N$ with bounding functions $b_{0}$ and $b_{1}$ , ${bB}_{N} (f_{0}, f_{1}, b_{0}, b_{1})$ is a bijective function $h : N \to N$ such that for all $m, n \in N$ , $h (m) = n$ implies $f_{0} (m) = n$ or $f_{1} (n) = m$ . As usual, the parenthesized expression $({bB}_{N})$ denotes the principle asserting the existence of a bounded Banach functional for $N$ .
Proposition 6.2 ( ${RCA}_{0}^{ω}$ ).

$(WKL)$ implies $({bB}_{N})$ .

Proof.
We work in ${RCA}_{0}^{ω}$ . For bounded injections $\vec{f} = ⟨ f_{0}, f_{1}, b_{0}, b_{1} ⟩$ , we will describe the computation of a related tree $T_{\vec{f}}$ so that any infinite path through $T_{\vec{f}}$ defines an injection h satisfying Banach’s theorem. If p is an infinite path through $T_{\vec{f}}$ , the bijection h will be defined by: $\begin{matrix} h (n) = \{\begin{matrix} f_{0} (n), & if p (n) = 0, \\ (μ t ⩽ b_{1} (n)) (f_{1} (t) = n), & if p (n) = 1 . \end{matrix} \end{matrix}$ A finite sequence $σ \in 2^{< N}$ is included in $T_{\vec{f}}$ if it satisfies the following four conditions, (i)–(iv), each ensuring an aspect of the back-and-forth construction of the bijection h.

First, if there is an $m < length (σ)$ which is not in the range of $f_{1}$ , we ensure that $h (m) = f_{0} (m)$ .
If $m < length (σ)$ and $(\forall t ⩽ b_{1} (m)) [f_{1} (t) \neq m]$ then $σ (m) = 0$ .
Next, if m is $f_{1} (t)$ for some t and t is not in the range of $f_{0}$ , we set $h (m) = t$ in the following fashion.
If $m < length (σ)$ , there is a $t ⩽ b_{1} (m)$ such that $f_{1} (t) = m$ , and $(\forall s ⩽ b_{0} (t)) [f_{0} (s) \neq t]$ , then $σ (m) = 1$ .
The next clause ensures that h is injective.
If $m, n < length (σ)$ , $σ (m) = 0$ , and $σ (n) = 1$ , then $f_{1} (f_{0} (m)) \neq n$ .
This final clause ensures that h is surjective.
If $m, n < length (σ)$ , $σ (m) = 0$ , and $σ (n) = 1$ , then $f_{1} (f_{0} (n)) \neq m$ .
The sequences satisfying the clauses are closed under initial segments, so $T_{\vec{f}}$ is a tree. The second-order proof of the bounded Banach theorem in ${WKL}_{0}$ (Theorem 1.4) shows that $T_{\vec{f}}$ is infinite. Note that the construction of $T_{\vec{f}}$ eventually halts for arbitrary choices of $\vec{f}$ , even if $f_{0}$ and $f_{1}$ are not injections or if $b_{0}$ or $b_{1}$ gives incorrect bounding information. Thus ${RCA}_{0}^{ω}$ proves the existence of a functional mapping $\vec{f}$ to $T_{\vec{f}}$ . Whenever $T_{\vec{f}}$ is infinite, $WKL (\vec{f})$ yields an infinite path. Concatenating these functionals with the one computing the bijection h as described at the beginning of the proof yields the desired Banach functional. □

The preceding proposition differs from the second-order analog (Theorem 1.3) in the formulation of the bounding functions. The original second-order version was formulated with characteristic functions for the ranges of the injections. However, in the calculation of $T_{\vec{f}}$ , the use of an incorrect characteristic function could result in an unbounded nonterminating search, causing the functional mapping $\vec{f}$ to $T_{\vec{f}}$ to be undefined on some inputs. This difficulty could be circumvented by using the fact that the uniform principle $(WKL)$ implies $(\exists^{2})$ , but the argument presented here uses a single application of $(WKL)$ .

Our proof of the unbounded version of Banach’s Theorem for $N$ from $(\exists^{2})$ uses a proposition relating $(\exists^{2})$ to the existence of bounding functions.
Definition 6.3.
The functional $b : N^{N} \to N^{N}$ maps any function $f : N \to N$ to a bounding function $b (f)$ for f. In the notation of from formula (3), for all f we have $β (f, b (f))$ . As usual, the parenthesized expression $(b)$ denotes the principle asserting the existence of a bounding functional.
Lemma 6.4 ( ${RCA}_{0}^{ω}$ ).

$(\exists^{2})$ implies $(b)$ .

Proof.
${RCA}_{0}^{ω}$ proves the existence of a functional $z : N^{N} \times N \to 2^{N}$ where $z (f, n) = g$ satisfies $g (m) = 0$ if and only if $f (m) = n$ . By Proposition 2.1, $(\exists^{2})$ proves the existence of Kohlenbach’s $μ_{0}$ . By composition and λ-abstraction, there is a functional $b (f)$ mapping f to the bounding function $μ_{0} (z (f, n))$ . □

The next definition formulates an unbounded form of Banach’s theorem on $N$ . Using the principle $(b)$ , the unbounded form can be derived from the bounded form.
Definition 6.5.
A Banach functional on $N$ , denoted $B_{N}$ , is defined as follows. For injective functions $f_{0} : N \to N$ and $f_{1} : N \to N$ , $B_{N} (f_{0}, f_{1})$ is a bijective function $h : N \to N$ such that for all $m, n \in N$ , $h (m) = n$ implies $f_{0} (m) = n$ or $f_{1} (n) = m$ . As usual, the parenthesized expression $(B_{N})$ denotes the principle asserting the existence of a Banach functional for $N$ .
Proposition 6.6 ( ${RCA}_{0}^{ω}$ ).

$(\exists^{2})$ implies $(B_{N})$ .

Proof.
Working in ${RCA}_{0}^{ω}$ , assume $(\exists^{2})$ . By Proposition 5.6, we have $(WKL)$ , so by Proposition 6.2, we have $({bB}_{N})$ . By Lemma 6.4, we have the functional $b$ mapping functions to associated bounding functions. The composition functional $bB (f_{0}, f_{1}, b (f_{0}), b (f_{1}))$ satisfies $(B_{N})$ . □

The next proposition essentially shows that the principle $(\exists^{2})$ can be deduced from the restricted form of Banach’s theorem for $N$ .
Proposition 6.7 ( ${RCA}_{0}^{ω}$ ).

$({bB}_{N})$ implies $(LLPO)$ .

Proof.
Assume ${RCA}_{0}^{ω}$ and $({bB}_{N})$ . Our goal is to prove the existence of the functional $LLPOmin$ . Let $g : N \to N$ and define bounded injections $f_{0}$ and $f_{1}$ as follows.

Figure 1 illustrates the construction of $f_{0}$ and $f_{1}$ for three choices of g. In general, for even inputs like $n = 2 m$ , let $f_{0} (n) = n + 2$ and $f_{1} (n) = n$ . For $n = 1$ , let $f_{0} (1) = 0$ and $f_{1} (1) = 1$ . The appearance of 0 in the range of g affects the definitions of $f_{0}$ and $f_{1}$ on other odd values. Suppose that $n = 2 m + 3$ . If $(\forall t ⩽ n - 2) [g (t) \neq 0]$ , then let $f_{0} (n) = n - 2$ and $f_{1} (n) = n$ . If $(\exists t ⩽ n - 2) [g (t) = 0]$ , write $s = (μ t) [g (t) = 0]$ . If s is even, then let $\begin{matrix} f_{0} (n) = \{\begin{matrix} n - 2, & if s = n - 3, \\ n, & if s < n - 3, \end{matrix} \end{matrix}$ and let $f_{1} (n) = n + 2$ . If s is odd, then let $\begin{matrix} f_{0} (n) = \{\begin{matrix} n - 2, & if s = n - 2, \\ n, & if s < n - 2, \end{matrix} \end{matrix}$ and $\begin{matrix} f_{1} (n) = \{\begin{matrix} n, & if s = n - 2, \\ n + 2, & if s < n - 2 . \end{matrix} \end{matrix}$

In Fig. 1, $f_{0}$ is represented by solid arrows and $f_{1}$ by dashed arrows. Extending the chains to the left and right, each number has an exiting arrow, so both $f_{0}$ and $f_{1}$ are total. No number has two entering arrows, so $f_{0}$ and $f_{1}$ are injective.

Figure 1.
Construction for Proposition 6.6. (a): $f_{0}$ (solid) and $f_{1}$ (dashed) when 0 is not in the range of g. (b): $f_{0}$ (solid) and $f_{1}$ (dashed) when $g (2) = 0$ . (c): $f_{0}$ (solid) and $f_{1}$ (dashed) when $g (3) = 0$ .

Figure 1(a) corresponds to the situation when 0 does not appear in the range of g. Any bijection h satisfying Banach’s theorem must either consist of all the (inverses of the) dashed arrows or all the solid arrows. In this situation, $h (1)$ may be 0 or 1.

Figure 1(b) corresponds to the case when $g (2) = 0$ is the first zero in the range of g. In this case, 5 must be in the domain of h, so $h (5) = f_{0} (5) = 3$ . The only bijection satisfying Banach’s theorem consists of solid arrows to the left of 5, so $h (1) = 0$ .

Figure 1(c) is for the case when $g (3) = 0$ is the first zero in the range of g. Here 5 must be in the range of h, so $h (5) = f_{1}^{- 1} (5) = 5$ . The only bijection satisfying Banach’s theorem consists of (inverses of the) dashed arrows to the left of 5, and so $h (1) = 1$ . If 0 first appears in the range of g at an even value, the figure for $f_{0}$ and $f_{1}$ will be a shifted version of the second figure. Odd values yield a shifted version of the third figure.

Because $f_{0} (n)$ is never less than $n - 2$ , $b_{0} (n) = n + 2$ is a bounding function for $f_{0}$ . Similarly, $f_{1} (n)$ is never less than n, so $b_{1} (n) = n$ is a bounding function for $f_{1}$ . Routine verification shows that for any choice of g, $f_{0}$ and $f_{1}$ will be injections bounded by $b_{0}$ and $b_{1}$ . Suppose that h is any bijection satisfying Banach’s theorem for $f_{0}$ , $f_{1}$ , $b_{0}$ , and $b_{1}$ . If the first 0 in the range of g occurs at an even value, then $h (1) = 0$ . If it occurs at an odd value, then $h (1) = 1$ . If 0 is not in the range of g, then $h (1)$ may be either 0 or 1. The system ${RCA}_{0}^{ω}$ proves the existence of the functional mapping g to the bounded injections ${\vec{f}}_{g} = ⟨ f_{1}, f_{1}, b_{0}, b_{1} ⟩$ as defined above. The functional ${bB}_{N} ({\vec{f}}_{g})$ yields the bijection h for ${\vec{f}}_{g}$ . Consequently, the functional mapping g to ${bB}_{N} ({\vec{f}}_{g}) (1)$ (which equals $h (1)$ ) is $LLPOmin (g)$ . □

Concatenating the preceding arguments yields the desired equivalence theorem and concludes the section.
Theorem 6.8 ( ${RCA}_{0}^{ω}$ ).

The following are equivalent:

$(\exists^{2})$ .

$(B_{N})$ .

$({bB}_{N})$ .

Proof.
Proposition 6.6 shows that (1) implies (2). Because $({bB}_{N})$ is a restriction of $(B_{N})$ , (2) implies (3) is immediate. Theorem 5.3 and Proposition 6.7 show that (3) implies (1). □
7. Banach’s theorem on compact spaces

Our next goal is to analyze the strength of Banach’s theorem restricted to uniformly continuous functions on complete separable metric spaces. We formalize complete separable metric spaces imitating Simpson [18, II.5]. The space $\hat{A}$ is the collection of rapidly converging sequences of elements of an underlying (countable) set A. The metric is a function $d : A \times A \to R$ , extended to $\hat{A}$ by defining $d ({⟨ a_{i} ⟩}_{i \in N}, {⟨ a_{i}^{'} ⟩}_{i \in N}) = {⟨ d (a_{i}, a_{i}^{'}) ⟩}_{i \in N}$ . As in Definition III.2.3 of Simpson [18], a space is compact if there is an infinite sequence of finite sequences of points of $\hat{A}$ of the form $⟨ ⟨ x_{i, j} : i ⩽ n_{j} ⟩ : j \in N ⟩$ , such that for all $z \in \hat{A}$ and $j \in N$ , there is an $i ⩽ n_{j}$ such that $d (x_{i, j}, z) < 2^{- j}$ .

Uniform continuity can be witnessed by a modulus of uniform continuity as formalized in Definition IV.2.1 of Simpson [18]. The function $h : N \to N$ is a modulus of uniform continuity for f if for all k, $| x - y | < 2^{- h (k)}$ implies $| f (x) - f (y) | < 2^{- k}$ . If $h_{f}$ is a modulus of uniform continuity for f and $h_{g}$ is a modulus of uniform continuity for g, then h defined by $h (n) = max {h_{f} (n), h_{g} (n)}$ is a modulus of uniform continuity for f and g. Consequently, a joint modulus can be used to simplify some statements.

Kohlenbach [12] defines two equivalent forms of continuity for functionals of type $1 \to 1$ . First, $F^{1 \to 1}$ is everywhere sequentially continuous if ([12, Definition 3.3]): $\begin{matrix} (\forall g^{1}) (\forall ⟨ g_{n} ⟩) [lim_{n \to \infty} g_{n} = g \to lim_{n \to \infty} F (g_{n}) = F (g)] . \end{matrix}$ Second, $F^{1 \to 1}$ is everywhere $ε - δ$ continuous if ([12, Definition 3.5]): $\begin{matrix} (\forall g^{1}) (\forall k) (\exists n) (\forall h^{1}) [d (g, h) < 2^{- n} \to d (F (g), F (h)) < 2^{- k}] . \end{matrix}$ This second definition is similar to familiar textbook definitions of continuity for total functions. The use of n and k reduces the type of the quantifiers corresponding to δ and ε. Proposition 3.6 of Kohlenbach [12] proves in ${RCA}_{0}^{ω}$ that F is everywhere sequentially continuous if and only if F is everywhere $ε - δ$ continuous.

For the reader’s convenience, we repeat the following portion of [12, Proposition 3.7] of Kohlenbach, a very useful tool for proving reversals.

Proposition 7.1 ([12, Proposition 3.7]).

The following are equivalent over ${RCA}_{0}^{ω}$ :

$(\exists^{2})$ .

There is a functional which is not everywhere sequentially continuous.

There is a functional which is not everywhere $ε - δ$ continuous.

For uniformly continuous functionals on compact complete separable metric spaces, it is possible to find ranges using only $(\exists^{2})$ . Indeed, the next two lemmas show that for Cantor space the existence of ranges is equivalent, a higher-order analog of Lemma III.1.3 of Simpson [18]. (Results in the next section show how to reformulate the following results without an explicit modulus of uniformity. See Theorem 8.3.)

Lemma 7.2 ( ${RCA}_{0}^{ω} + (\exists^{2})$ ).

Suppose X is a compact complete separable metric space. There is functional R such that if $f : X \to X$ is a function with modulus of uniform continuity h, $R (f, h)$ is the characteristic function of the range of f. That is, for all $y \in X$ , $R (f, h) (y) \in {0, 1}$ and $R (F, h) (y) = 1$ if and only if $(\exists x \in X) [f (x) = y]$ .

Proof.
Working in ${RCA}_{0}^{ω}$ , let X be as hypothesized, with the compactness of X witnessed by $⟨ ⟨ x_{i, j} : i ⩽ n_{j} ⟩ : j \in N ⟩$ . Consider a function $f : X \to X$ with modulus of uniform continuity h. Informally, a value $y \in X$ is in the range of f if and only if for every m there is an x with $d (F (x), y) < 2^{- m}$ . By uniform continuity and compactness, such an x exists if and only if there is an $i ⩽ n_{h (m)}$ such that $d (f (x_{i, h (m)}), y) < 2^{- m}$ . In ${RCA}_{0}^{ω}$ , for $f : X \to X$ and $h : N \to N$ , we may define $\begin{matrix} K (f, h, y, m) = \{\begin{matrix} 1, & if (\exists i ⩽ n_{h (m)}) [d (f (x_{i, h (m)}), y) < 2^{- m}] \\ 0, & otherwise. \end{matrix} \end{matrix}$ Viewing K as a function in m with parameters f, h, and y, in $(\exists^{2})$ we may define $R (f, h) (y) = φ (K (F, h, y, m))$ . Informally, by the definition of φ, $R (f, h) (y) = 1$ if and only if for all m there is an x with $d (f (x), y) < 2^{- m}$ . Note that the calculation of $R (f, h)$ eventually halts even if f is not continuous or h is incorrect.

To complete our proof, we must verify in ${RCA}_{0}^{ω} + (\exists^{2})$ our informal claim that for each continuous function f with modulus of uniform continuity h, $R (f, h)$ is the characteristic function for the range of f. First, if $R (f, h) (y) = 1$ , then there is a sequence $⟨ x_{i_{m}}^{'} ⟩$ such that for every m, $d (f (x_{i_{m}}^{'}), y) < 2^{- m}$ . The principle $(\exists^{2})$ implies ${ACA}_{0}$ which implies the Bolzano–Weierstrass theorem (see Theorem III.2.7 of Simpson [18]), so we can thin $⟨ x_{i_{m}}^{'} ⟩$ to a sequence converging to some $x \in X$ . By sequential continuity of f, we have $f (x) = y$ .

Second, if $R (f, h) (y) = 0$ , then for some natural number m, we must have $(\forall i ⩽ n_{h (m)}) [d (f (x_{i, h (m)}, y) ⩾ 2^{- m}]$ . Suppose by way of contradiction that $f (x) = y$ . Choose $i ⩽ n_{h (m)}$ such that $d (x, x_{i, h (m)}) < 2^{- h (m)}$ . Because f is uniformly continuous, $d (f (x_{i, h (m)}), f (x)) < 2^{- m}$ . Concatenating inequalities, we have $\begin{matrix} 2^{- m} ⩽ d (f (x_{i, h (m)}), y) = d (f (x_{i, h (m)}), f (x)) < 2^{- m}, \end{matrix}$ a contradiction. Thus, $R (f, h) (y) = 0$ implies $(\forall x \in X) [f (x) \neq y]$ , completing the proof. □
Lemma 7.3 ( ${RCA}_{0}^{ω}$ ).

The following are equivalent:

$(\exists^{2})$ .

If X is a compact complete separable metric space, then there is functional R such that if $f : X \to X$ is a function with modulus of uniform continuity h, $R (f, h)$ is the characteristic function of the range of f.

There is functional R such that if $f : 2^{N} \to 2^{N}$ is a function with modulus of uniform continuity h, $R (f, h)$ is the characteristic function of the range of f.

Proof.
We will work in ${RCA}_{0}^{ω}$ . By Lemma 7.2, item (1) implies item (2). Item (3) is a special case of item (2), so we need only show that item (3) implies item (1).

In ${RCA}_{0}^{ω}$ , we can prove the existence of the function that maps an arbitrary function $f : N \to N$ to an element of Cantor space $f^{'} : N \to 2$ so that, for all n, $f^{'} (n) = 1$ if and only if $f (n) > 0$ . In terms of the function from the definition of $(\exists^{2})$ , $R_{LPO} (f) = R_{LPO} (f^{'})$ . ${RCA}_{0}^{ω}$ can also prove the existence of the transformation $S : 2^{N} \to 2^{N}$ such that for all $f : N \to 2$ , $S (f) (n) = 0$ if $(\forall m ⩽ n) [f (m) \neq 0]$ and $S (f) (n) = 1$ otherwise. Let $C$ denote the set of functions from $2^{N}$ to $2^{N}$ . ${RCA}_{0}^{ω}$ proves the existence of the function $T : 2^{N} \to C$ which maps each $f \in 2^{N}$ to the constant function in $C$ that takes the value $S (f)$ . For each f, because $T (f)$ is a constant function, the constant 0 function on $N$ , denoted by $z (n) \equiv 0$ , is a modulus of uniform continuity for $T (f)$ . (Any function could be used as a modulus.) For any $f \in N^{N}$ , z is in the range of $T (f^{'})$ if and only if 0 is not in the range of $f^{'}$ , and this occurs if and only if $R_{LPO} (f) = 1$ . Using the functional from item (3), we have $R_{LPO} (f) = R (T (f^{'}), z) (z)$ , so item (3) implies $(\exists^{2})$ . □

Our proof of Banach’s theorem in compact metric spaces requires a functional that can calculate the inverse of a given function. The next two lemmas show that $(\exists^{2})$ is sufficient and also necessary for this task.
Lemma 7.4 ( ${RCA}_{0}^{ω} + (\exists^{2})$ ).

Suppose X is a compact complete separable metric space. There is a functional I such that if $f : X \to X$ is a function with modulus of uniform continuity h, then $I (f, h)$ is a function that selects elements from the pre-image of f. That is, for all $y \in X$ , if there is an p such that $f (p) = y$ , then $f (I (f, h) (y)) = y$ . In particular, if f is injective, then the restriction of $I (f, h)$ to the range of f is the inverse of f.

Proof.
Suppose that the compactness of X is witnessed by the sequence of finite sequences $⟨ ⟨ x_{i, j} : i ⩽ n_{j} ⟩ : j \in N ⟩$ . Thus for all $z \in X$ , there is an $x_{i, j}$ in $⟨ x_{i, j} : i ⩽ n_{j} ⟩$ such that $d (x_{i, j}, z) < 2^{- j}$ . Given a function f with a modulus of uniform continuity h, for each y we will calculate a rapidly converging subsequence $p = ⟨ p_{m} : m \in N ⟩$ such that if y is in the range of f then $f (p) = y$ . We will argue that this calculation is sufficiently uniform that the desired functional I can be found using ${RCA}_{0}^{ω} + (\exists^{2})$ .

Fix $f : X \to X$ with modulus of uniform continuity h, so that if $d (t_{1}, t_{2}) < 2^{- h (k)}$ then $d (f (t_{1}), f (t_{2})) < 2^{- k}$ . Increasing h if necessary, we may assume that $h (k) ⩾ k + 3$ for all k. Using the witness points for compactness, if y is in the range of f, then for all j we have $(\exists k ⩽ n_{h (j)}) [d (f (x_{k, h (j)}, y) < 2^{- j}]$ .

Given f, h, and y as above, we can define the desired $p = ⟨ p_{m} : m \in N ⟩$ . If y is not in the range of f, let $p = y$ . If y is in the range of f construct $⟨ p_{m} : m \in N ⟩$ as follows. Let $p_{m} = x_{i, h (m)}$ where $i ⩽ n_{h (m)}$ is the least integer such that:
$d (f (x_{i, h (m)}), y) < 2^{- m}$ ,

$(\forall j > m) (\exists k ⩽ n_{h (j)}) [d (f (x_{k, h (j)}, y) < 2^{- j} \land d (x_{k, h (j)}, x_{i, h (m)}) < 2^{- m - 2}]$ , and

if $m > 0$ , then $d (p_{m - 1}, x_{i, h (m)}) ⩽ 2^{- m}$ .
The third clause ensures that $p = ⟨ p_{m} : m \in N ⟩$ is a rapidly converging Cauchy sequence. By Proposition 3.6 of Kohlenbach [12], $(\exists^{2})$ proves that f is sequentially continuous, so the first clause shows that $f (p) = y$ . Informally, the second clause guarantees that each $p_{m}$ is sufficiently close to a pre-image of y that the construction can continue. We verify this next.

To initialize the construction, we must find $p_{0}$ . Suppose $f (t_{0}) = y$ . Because $h (2) ⩾ 0 + 3$ we can fix an $i ⩽ n_{h (0)}$ with $d (x_{i, h (0)}, t_{0}) < 2^{- 3}$ . Because h is a modulus of uniform continuity, $d (f (x_{i, h (0)}), y) = d (f (x_{i, h (0)}), f (t_{0})) < 2^{- 0}$ , so clause (1) is satisfied. For any $j > 0$ , there is a $k ⩽ n_{h (j)}$ such that $d (x_{k, h (j)}, t_{0}) < 2^{- h (j)} < 2^{- 3}$ , and so $d (f (x_{k, h (j)}, y) = d (f (x_{k, h (j)}), f (t_{0})) < 2^{- j}$ . For such a j and k, $\begin{matrix} d (x_{k, h (j)}, x_{i, h (0)}) ⩽ d (x_{k, h (j)}, t_{0}) + d (x_{i, h (0)}, t_{0}) < 2^{- 3} + 2^{- 3} = 2^{- 2}, \end{matrix}$ so clause (2) is also satisfied. The third clause is vacuously true. We have shown that for some i, $x_{i, h (0)}$ satisfies all three clauses. Let $i_{0}$ be the least such i, and set $p_{0} = x_{i_{0}, h (0)}$ .

Suppose $p_{m - 1}$ has been chosen satisfying all three clauses. By clause (2) for $p_{m - 1}$ , we can find a sequence of points $⟨ t_{m_{j}} : j \in N ⟩$ such that for every j, $d (f (t_{m_{j}}), y) < 2^{- j}$ and $d (t_{m_{j}}, p_{m - 1}) < 2^{- (m - 1) - 2} = 2^{- m - 1}$ . In Theorem III.2.7, Simpson [18] proves the generalization of the Bolzano–Weierstrass theorem for compact metric spaces in ${ACA}_{0}$ , so it is also a theorem of ${RCA}_{0}^{ω} + (\exists^{2})$ . Consequently, there is a subsequence of $⟨ t_{m_{j}} : j \in N ⟩$ converging to a value $t_{m}$ with $f (t_{m}) = y$ and $d (t_{m}, x_{m - 1}) ⩽ 2^{- m - 1}$ . Choose $i ⩽ n_{h (m)}$ so that $d (x_{i, h (m)}, t_{m}) < 2^{- h (m)} < 2^{- m - 3}$ . Clause (1) holds for $x_{i, h (m)}$ because h is a modulus of uniform continuity and $f (t_{m}) = y$ . For any $j > m$ , there is a $k ⩽ n_{h (j)}$ such that $d (x_{k, h (j)}, t_{m}) < 2^{- h (j)} ⩽ 2^{- j - 3}$ and so $d (f (x_{k, h (j)}), y) < 2^{- j}$ . For such a j and k, $\begin{matrix} d (x_{k, h (j)}, x_{i, h (m)}) ⩽ d (x_{k, h (j)}, t_{0}) + d (x_{i, h (m)}, t_{0}) < 2^{- j - 3} + 2^{- m - 3} < 2^{- m - 2}, \end{matrix}$ so clause (2) holds for $x_{i, h (m)}$ . Finally, $\begin{matrix} d (p_{m - 1}, x_{i, h (m)}) < d (p_{m - 1}, t_{m}) + d (x_{i, h (m)}, t_{m}) < 2^{- m - 1} + 2^{- m - 3} < 2^{- m} . \end{matrix}$ We have shown that all three clauses hold for some choice of i, so let $i_{m}$ be the least such i and set $p_{m} = x_{i_{m}, h (m)}$ . This concludes the argument that our construction never halts, yielding the desired pre-image $p = ⟨ p_{m} : m \in N ⟩$ .

It remains to show that ${RCA}_{0}^{ω} + (\exists^{2})$ suffices to prove the existence of the functional I from the statement of the lemma. Suppose we are given f with modulus h and a value y from the metric space. By Lemma 7.2, $R (f, h)$ is the characteristic function for the range of f. If y is not in the range of f, output y. Otherwise, begin constructing p, searching for an $x_{i, h (m)}$ satisfying clauses (1), (2), and (3) above. By $(\exists^{2})$ , we may use a realizer for $LPO$ to check if clause (2) holds. As argued above, when y is in the range, this process calculates the desired pre-image of y. Summarizing, ${RCA}_{0}^{ω} + (\exists^{2})$ proves the existence of the function mapping f, h, and y to the desired value. Applying λ-abstraction yields $I (f, h)$ . □

The use of $(\exists^{2})$ in the previous lemma is necessary, as shown by the following reversal.
Lemma 7.5 ( ${RCA}_{0}^{ω}$ ).

The following are equivalent:

$(\exists^{2})$ .

If X is a compact complete separable metric space, then there is a function I such that if $f : X \to X$ is a function with modulus of uniform continuity h, then $I (f, h)$ is a function that selects elements from the pre-image of f.

There is a function I such that if $f : 2^{N} \to 2^{N}$ is a function with modulus of uniform continuity h, then $I (h, f)$ is a function that selects elements from the pre-image of f.

Proof.
We will work in ${RCA}_{0}^{ω}$ . By Lemma 7.4, item (1) implies item (2). Item (3) is a special case of item (2), so we need only show that item (3) implies item (1). By Proposition 5.2, it suffices to show that (3) implies $(LLPO)$ .

Given an input $w : N \to 2$ for $LLPOmin$ , we will show how to construct a function f with modulus of uniform continuity h such that information about the pre-image of f as provided by $I (f, h)$ in item (3) can be used to calculate $LLPOmin$ for w. In particular, we will control the pre-image of the constant 0 function, denoted $\vec{0} \in 2^{N}$ . If the first t where $w (t) = 0$ is even, we require $f^{- 1} (\vec{0}) = {\vec{0}}$ . If the first t such that $w (t) = 0$ is odd, we require $f^{- 1} (\vec{0}) = {\vec{1}}$ . If 0 is not in the range of w, $f^{- 1} (\vec{0})$ will be the set ${\vec{0}, \vec{1}}$ .

Now we can specify the behavior of f. Let $x : N \to 2$ be an element of $2^{N}$ . Evaluating f at x yields a function $f (x)$ , which also maps $N$ into 2 and is defined as follows.
$f (x) (0) = 0$ .

For $n > 0$ , $f (x) (n)$ is defined by two cases:

if $n - 1$ is not the least t such that $w (t) = 0$ then $\begin{matrix} f (x) (n) = \{\begin{matrix} x (n), & if x (0) = 0, \\ 1 - x (n), & if x (0) = 1 . \end{matrix} \end{matrix}$

if $n - 1$ is the least t such that $w (t) = 0$ then $\begin{matrix} f (x) (n) = \{\begin{matrix} x (0), & if n - 1 is even, \\ 1 - x (0), & if n - 1 is odd . \end{matrix} \end{matrix}$

Routine arguments verify that the pre-image of f satisfies the requirements listed above. Also, if the sequences x and y agree in the first n values, the sequences $f (x)$ and $f (y)$ also agree in the first n values. Thus, the function $h (n) = n$ is a modulus of uniform continuity for f. The construction of f from w is sufficiently uniform that ${RCA}_{0}^{ω}$ proves the existence of a function g mapping each $w \in 2^{N}$ to its associated function f.

Let I be the function described in item (3) of the statement of the lemma, and let $h (n) = n$ be the identity function on $N$ . The for any $w \in 2^{N}$ , $I (g (w), h) (\vec{0})$ is (an element of $2^{N}$ ) equal to $\vec{0}$ if the first 0 in the range of w occurs at an even value, and $\vec{1}$ if the first 0 occurs at an odd value. The sequences coding elements of $2^{N}$ output by I are rapidly converging sequences of finite approximations to $\vec{0}$ or $\vec{1}$ . By the definition of the metric on $2^{N}$ , the first entry in the third finite approximation for any sequence equal to $\vec{0}$ will be 0, and similarly the value 1 can be extracted from any sequence equal to $\vec{1}$ . Thus $I (g (w), h) (0)$ uniformly calculates $LLPOmin$ for w. □

The previous results allow us to formulate and analyze some restrictions of Banach’s theorem. For compact complete separable metric spaces, a functional form of Banach’s theorem restricted to uniformly continuous functions is equivalent to the functional existence principle $(\exists^{2})$ . Note that if f and g have moduli of uniform continuity $h_{f}$ and $h_{g}$ , then h defined by $h (n) = max {h_{f} (n), h_{g} (n)}$ is a modulus of uniform continuity for both f and g. As a notational convenience, we will use common moduli of uniformity for pairs of functions.
Definition 7.6.
For a complete separable metric space X, a Banach functional $B_{X}$ is defined as follows. For injective functions $f : X \to X$ and $g : X \to X$ with a common modulus of uniformity h, $B_{X} (f, g, h)$ is a bijective function $H : X \to X$ such that for all $x \in X$ , $H (x) = f (x)$ or $g (H (x)) = x$ . The parenthesized expression $(B_{X})$ denotes the principle asserting the existence of a Banach functional for X.

Emulating Proposition 6.6, the next result proves a version of Banach’s theorem for compact metric spaces using $(\exists^{2})$ . The reversals and a summary appear in a second result.
Lemma 7.7 ( ${RCA}_{0}^{ω}$ ).

$(\exists^{2})$ implies that if X is a compact metric space, then $(B_{X})$ .

Proof.
Assume ${RCA}_{0}^{ω}$ and $(\exists^{2})$ . Suppose X is a complete separable metric space and that $⟨ ⟨ x_{i, j} : i ⩽ n_{j} ⟩ : j \in N ⟩$ witnesses that X is compact. Let f and g be injections of X into X with a common modulus of uniform continuity h. Apply Lemma 7.2 to find the range functionals $R (f, h)$ and $R (g, h)$ . Apply Lemma 7.4 to find pre-image selectors $I (f, h)$ and $I (g, h)$ . Because f and g are injections, the restrictions of these functions to the ranges of f and g are inverse functions. Consequently, we will use the shorthand notation $f^{- 1}$ and $g^{- 1}$ . Note that the pre-image selectors $f^{- 1}$ and $g^{- 1}$ are defined for all inputs from X, and that if (for example) y is in the range of f, then $f (f^{- 1} (y)) = y$ . Our goal is to construct the bijection H in the statement of $(B_{X})$ . This is achieved by a back-and-forth construction, alternately iterating applications of $g^{- 1}$ and $f^{- 1}$ , and basing the value of H on the terminating condition of this process.

First we construct a functional that alternately applies $g^{- 1}$ and $f^{- 1}$ . Using primitive recursion, define $S (x, n)$ by $S (x, 0) = x$ and for $n ⩾ 0$ , $S (x, 2 n + 1) = g^{- 1} (S (x, 2 n))$ and $S (x, 2 n + 2) = f^{- 1} (S (x, 2 n + 1))$ . Calculating a few values yields $S (x, 0) = x$ , $S (x, 1) = g^{- 1} (x)$ , $S (x, 2) = f^{- 1} (g^{- 1} (x))$ , and $S (x, 3) = g^{- 1} (f^{- 1} (g^{- 1} (x)))$ . As noted above, $f^{- 1}$ and $g^{- 1}$ are total, so $S (x, n)$ is defined for all x and all n.

A traditional back-and-forth construction using partial inverse functions might halt if, for example, x was not in the range of g, or if $g^{- 1} (x)$ was not in the range of f, and so on. Define the function $P : X \times N \to {0, 1}$ by $P (x, 0) = 1$ and for $n ⩾ 0$ , $P (x, 2 n + 1) = R (g, h) (S (x, 2 n))$ and $P (x, 2 n + 2) = R (f, h) (S (x, 2 n + 1))$ . Consider the initial stages of the back-and-forth process displayed in the following table.

If x is not in the range of g then $P (x, 1) = 0$ . If $g^{- 1} (x)$ is not in the range of f, then $P (x, 2) = 0$ . In general, the least n with $P (x, n) = 0$ will be the stage where the traditional back-and-forth process based on partial inverse functions will halt. If the back-and-forth process does not halt, then $P (x, n) = 1$ for all n. Writing $P_{x} (n)$ for $P (x, n)$ , we may view $P_{x} (n)$ as a function from $N$ into ${0, 1}$ . Apply φ as provided by $(\exists^{2})$ , and we have $φ (P_{x} (n)) = 0$ if the back-and-forth process halts and $φ (P_{x} (n)) = 1$ if the process never halts.

By $(\exists^{2})$ and Theorem 5.3, we may also use $R_{LLPOmin}$ , a realizer for $LLPOmin$ . Define the functional $T (x)$ by $\begin{matrix} T (x) = \{\begin{matrix} 1, & if φ (P_{x} (n)) = 1, \\ R_{LLPOmin} (P_{x}), & if φ (P_{x} (n)) = 0 . \end{matrix} \end{matrix}$ Finally, define the bijection $H (x)$ by $\begin{matrix} H (x) = \{\begin{matrix} f (x), & if T (x) = 1, and \\ g^{- 1} (x), & if T (x) = 0 . \end{matrix} \end{matrix}$ One can argue that H is the desired bijection by the usual arguments. Briefly, consider the following diagram representing images and pre-images of an element x from X.

Each element of the lower copy of X appears in at least one bipartite subgraph of the sort pictured. Also, for each y in the upper copy of X, we know $y = g^{- 1} (g (y))$ , so each element in the upper copy of X appears in at least one bipartite subgraph. Because f and g are injective, each element appears in exactly one bipartite subgraph. The choice of the values of $H (x)$ ensure that if the bipartite graph ends on the left, the left most vertex is either in the lower copy of X and in the domain of H, or in the upper copy of X and in the range of H. Thus H is a bijection of X into itself, satisfying the requirements of $(B_{X})$ . □

This section concludes with proofs of two reversals for instances of the previous lemma, summarizing the results for Banach’s theorem on compact metric spaces in the following theorem.
Theorem 7.8 ( ${RCA}_{0}^{ω}$ ).

The following are equivalent:

$(\exists^{2})$ .

If X is a compact metric space, then $(B_{X})$ .

$(B_{[0, 1]})$ .

$(B_{2^{N}})$ .

Proof.
The previous lemma proves that item (1) implies item (2). Item (3) and item (4) are special cases of item (2), so we can complete the proof by reversing (3) and (4) to (1). For the first reversal, suppose $B_{[0, 1]} (f, g, h)$ is the Banach functional for $[0, 1]$ . Consider the injections f and g defined by $f (x) = g (x) = x / 2$ . Each x in $[0, 1]$ is represented by a rapidly converging sequence of rationals, and dividing each element of the sequence by 2 yields a rapidly converging sequence representing $x / 2$ . Thus ${RCA}_{0}^{ω}$ proves that f and g are defined and total. The identity function $h (k) = k$ is a modulus of uniform continuity for f and g. Suppose $H = B_{[0, 1]} (f, g, h)$ is the bijection satisfying Banach’s theorem for f and g. Consider $x = \frac{1}{2}$ and the sequence $x_{n} = \frac{1}{2} + \frac{1}{2^{n}}$ . For each n, $x_{n}$ is not in the range of g, so $H (x_{n}) = f (x_{n}) = \frac{x_{n}}{2} = \frac{1}{4} + \frac{1}{2^{n + 1}}$ . Thus, ${lim}_{n \to \infty} H (x_{n}) = \frac{1}{4}$ . The functional H is bijective, so 1 is in the range of H. Fix x with $H (x) = 1$ . By the Banach theorem, $H (x) = f (x)$ or $H (x) = g^{- 1} (x)$ . Because 1 is not in the range of F, $H (x) = g^{- 1} (x)$ . Thus $1 = g^{- 1} (x)$ , so $x = \frac{1}{2}$ and $H (\frac{1}{2}) = 1$ . Summarizing, $\begin{matrix} H (lim_{n \to \infty} x_{n}) = H (\frac{1}{2}) = 1 \neq \frac{1}{4} = lim_{n \to \infty} H (x_{n}) . \end{matrix}$ Thus H is not sequentially continuous at $x = \frac{1}{2}$ , and $(\exists^{2})$ follows by Proposition 7.1.

For the final reversal, suppose $B_{2^{N}} (f, g, h)$ is the Banach functional for Cantor space. Consider the padding function $P (x)$ that adds a zero after each entry in a binary input string. Formally, $P (x) (n) = x (m)$ if $n = 2 m$ , and $P (x) (n) = 0$ otherwise. For example, $\begin{matrix} P (⟨ 1, 0, 1, 1 \dots ⟩) = ⟨ 1, 0, 0, 0, 1, 0, 1, 0 \dots ⟩ . \end{matrix}$ ${RCA}_{0}^{ω}$ proves that $P (x)$ is defined and total, and that the identity function $h (k) = k$ is a modulus of uniform continuity for $P (x)$ . Let $f (x)$ and $g (x)$ both be $P (x)$ . Let $H = B_{2^{N}} (f, g, h)$ be the bijection satisfying Banach’s theorem for f and g. For each n, let $σ_{n}$ consist of n copies of the string 10, followed by 11, followed by zeros. The double 1 ensures that $σ_{n}$ is not in the range of $g (x) = P (x)$ . Thus, for each n, $H (σ_{n}) = f (σ_{n}) = P (σ_{n})$ , which consists of n copies of the string 1000 followed by 1010, followed by zeros. Thus ${lim}_{n \to \infty} H (σ_{n})$ is the string 1000 repeated infinitely. On the other hand, ${lim}_{n \to \infty} σ_{n}$ is $⟨ 1, 0, 1, 0 \dots ⟩$ . The string $⟨ 1, 1, 1 \dots ⟩$ is not in the range of $f (x)$ , so $H (g (⟨ 1, 1, 1 \dots ⟩)) = ⟨ 1, 1, 1 \dots ⟩$ . Because $g (⟨ 1, 1, 1 \dots ⟩) = ⟨ 1, 0, 1, 0 \dots ⟩$ , we have $H ({lim}_{n \to \infty} σ_{n}) = H (⟨ 1, 0, 1, 0 \dots ⟩) = ⟨ 1, 1, 1 \dots ⟩$ . Thus $H ({lim}_{n \to \infty} σ_{n}) \neq {lim}_{n \to \infty} H (σ_{n})$ , so H is not sequentially continuous at $x = ⟨ 1, 0, 1, 0 \dots ⟩$ . The principle $(\exists^{2})$ follows by Proposition 7.1, completing the reversal and the proof of the theorem. □

We note that the functional R in Lemma 7.2, the functional I in Lemma 7.5, and the functional B in Theorem 7.8 are constructed uniformly in a code for the space X. Hence these functionals could, in principle, be defined with X as a parameter. This is another layer of uniformity in the constructions, although noting the parameter explicitly complicates the notation. It would be interesting to know how changing the representation of a fixed space affects the functionals I and B.
8. Moduli of uniform continuity

This section introduces a function that computes moduli of uniform continuity. Functions of this sort are not new to the computability literature. For example, the fan functional described by Normann and Tait [15] computes the modulus of uniform continuity for continuous functions on $2^{N}$ . As shown below, the strength of the existence of the function lies below $(\exists^{2})$ , allowing us to streamline the definition of Banach functionals and Theorem 7.8.

Definition 8.1.
Suppose X is a compact complete separable metric space and Y is a complete separable metric space. The principle $(M_{X, Y})$ asserts the existence of a function M such that if $f : X \to Y$ is continuous, then $M (f)$ is a modulus of uniform continuity for f.

Near the end of his article, Kohlenbach [12] presents a functional form of Brouwer’s intuitionistic fan theorem, denoted by $(MUC)$ . He notes that $(M_{[0, 1], R})$ is a consequence of $(MUC)$ , $(MUC)$ is conservative over ${WKL}_{0}$ for second-order sentences, and $(MUC)$ is inconsistent with $(\exists^{2})$ . Because $(MUC)$ proves $(M_{[0, 1], R})$ , the principle $(M_{[0, 1], R})$ is also conservative over ${WKL}_{0}$ for second-order sentences. The next lemma shows that unlike $(MUC)$ , the principle $(M_{[0, 1], R})$ and similar principles for other spaces are consequences of $(\exists^{2})$ .
Lemma 8.2 ( ${RCA}_{0}^{ω}$ ).

If X and Y are complete separable metric spaces and X is compact, then $(\exists^{2})$ implies $(M_{X, Y})$ .

Proof.
Let X be a compact complete separable metric space with compactness witnessed by the sequence of sequences $⟨ ⟨ x_{i, j} : i ⩽ n_{j} ⟩ : j \in N ⟩$ . Let Y be a complete separable metric space. We will use d to denote the metric in both spaces. For $f : X \to Y$ we can define a prospective value of a modulus of uniform continuity for f at m by setting $(M (f)) (m)$ equal to the least n such that: $\begin{matrix} (4) & (\forall x_{i, j}) (\forall x_{i^{'}, j^{'}}) [d (x_{i, j}, x_{i^{'}, j^{'}}) < 2^{- n} \to d (f (x_{i, j}), f (x_{i^{'}, j^{'}})) < 2^{- m - 1}] \end{matrix}$ Informally, $M (f)$ is a function from $N$ to $N$ that resembles a modulus of uniform continuity on the compactness witnesses for X. First we will show that ${RCA}_{0}^{ω} + (\exists^{2})$ suffices to prove the existence of the function M. Then we will verify that if f is continuous, then $M (f)$ is a modulus of uniform continuity for f.

Working in ${RCA}_{0}^{ω} + (\exists^{2})$ , let X and Y be as above, and suppose $f : X \to Y$ . Recalling the reverse mathematical formalization of inequalities in the reals, the formulas $d (x_{i, j}, x_{i^{'}, j^{'}}) < 2^{- n}$ and $d (f (x_{i, j}), f (x_{i^{'}, j^{'}})) > 2^{- m - 1}$ are $Σ_{1}^{0}$ . Thus ${RCA}_{0}^{ω}$ proves the existence of a function $a (f, m, n, t)$ which is 0 if t codes a witness that there are $x_{i, j}$ and $x_{i^{'}, j^{'}}$ such that $d (x_{i, j}, x_{i^{'}, j^{'}}) < 2^{- n}$ and $d (f (x_{i, j}), f (x_{i^{'}, j^{'}})) > 2^{- m - 1}$ , and is 1 otherwise. Note that formula (4) holds if $a (f, m, n, t)$ is 1 for all t, and fails if there is a t such that $a (f, m, n, t)$ is 0. As noted in Section 5, $(\exists^{2})$ implies the existence of the function $R_{LPO}$ . The λ notation $λ t . a (f, m, n, t)$ denotes the function that maps each $t \in N$ to the value $a (f, m, n, t)$ . Applying λ-abstraction (which is a consequence of ${RCA}_{0}^{ω}$ [12]) and $(\exists^{2})$ , we can prove the existence of the function $b (f, m, n) = R_{LPO} (λ t . a (f, m, n, t))$ . Note that for all f, m, and n, $b (f, m, n) = 1$ if formula (4) holds and $b (f, m, n) = 0$ otherwise. By Proposition 2.1, $(\exists^{2})$ proves the existence of Feferman’s μ, so by $(\exists^{2})$ and an additional application of λ-abstraction, we can prove the existence of the function $c (f, m) = μ (1 - λ n . b (f, m, n))$ . Note that for each f and m, if there is an n such that formula (4) holds, then $c (f, m)$ is the least such n. If there is no such n, for example if f is discontinuous, then $c (f, m)$ still yields some value, but no useful information. By λ-abstraction, ${RCA}_{0}^{ω} + (\exists^{2})$ proves the existence of $M (f) = λ m . c (f, m)$ . For every $f : X \to Y$ , $M (f)$ yields a function from $N$ to $N$ .

It remains to show that if f is continuous then $M (f)$ is a modulus of uniform continuity for f. Fix a continuous $f : X \to Y$ and $m \in N$ . Let $n = M (f) (m)$ . Suppose that $u, v \in X$ satisfy $d (u, v) < 2^{- n}$ . Choose $δ < 2^{- n} - d (u, v)$ . Because f is continuous and $⟨ ⟨ x_{i, j} : i ⩽ n_{j} ⟩ : j \in N ⟩$ is dense in X, we can find an $x_{i, j}$ such that $d (x_{i, j}, u) < δ / 2$ and $d (f (x_{i, j}), f (u)) < 2^{- m - 2}$ . Similarly, find $x_{i^{'}, j^{'}}$ such that $d (x_{i^{'}, j^{'}}, v) < δ / 2$ and $d (f (x_{i^{'}, j^{'}}), f (v)) < 2^{- m - 2}$ . By the triangle inequality, $\begin{matrix} d (x_{i, j}, x_{i^{'}, j^{'}}) ⩽ d (x_{i, j}, u) + d (u, v) + d (v, x_{i^{'}, j^{'}}) < δ / 2 + d (u, v) + δ / 2 < 2^{- n} . \end{matrix}$ Because $d (x_{i, j}, x_{i^{'}, j^{'}}) < 2^{- n}$ , and because $(M (f)) (m) = n$ , formula (4) holds, so $d (f (x_{i, j}), f (x_{i^{'}, j^{'}})) < 2^{- m - 1}$ . By the triangle inequality, $\begin{matrix} d (f (u), f (v)) & < d (f (u), f (x_{i, j})) + d (f (x_{i, j}, f (x_{i^{'}, j^{'}})) + d (f (x_{i^{'}, j^{'}}), f (v)) \\ < 2^{- m - 2} + 2^{- m - 1} + 2^{- m - 2} = 2^{- m} . \end{matrix}$ Summarizing, when f is continuous and $M (f) (m) = n$ , if $d (u, v) < 2^{- n}$ then $d (f (u), f (v) < 2^{- m}$ . Thus $M (f)$ is a modulus of uniform continuity for f. □

The principle $(M_{X, Y})$ allows us to reformulate many of the results in the preceding section. For example, Theorem 7.8 can be simplified as follows, stripping all reference to moduli of uniform continuity.
Theorem 8.3 ( ${RCA}_{0}^{ω}$ ).

The principle $(\exists^{2})$ is equivalent to the statement that for every compact complete separable metric space X, there is a function $B_{X}^{'}$ that maps each pair of injections from X to X to a bijection satisfying Banach’s theorem.

Proof.
Assuming $(\exists^{2})$ , by Lemma 8.2 we may use the principle $(M_{X, X})$ to find a function M that calculates moduli of uniform continuity for f and g. The pointwise maximum function $max (M (f), M (g))$ is a joint modulus of uniform continuity for f and g. If $B_{X} (f, g, m)$ is the function provided by Theorem 7.8 part (2), then the function defined by $B_{X}^{'} (f, g) = B_{X} (f, g, max (M (f), M (g)))$ is the desired Banach function. The converse is immediate from Theorem 7.8. □

Because $(M_{[0, 1], R})$ is a consequence of $(MUC)$ , the principle $(M_{[0, 1], R})$ does not imply $(\exists^{2})$ . That is, this restriction of the converse of Lemma 8.2 is not true. The next two results show that like $(MUC)$ , the second-order theorems of $(M_{[0, 1], R})$ are exactly those of ${WKL}_{0}$ . As part of that proof, the next lemma allows us to change representations of functions, with the eventual goal of applying a traditional reverse mathematics result to show that $(M_{[0, 1], R})$ implies ${WKL}_{0}$ . (The following lemma for functions from Baire space to $N$ appears as Proposition 4.4 in Kohlenbach’s [11] contribution to the Feferman volume.)
Lemma 8.4 ( ${RCA}_{0}^{ω}$ ).

Suppose X and Y are complete separable metric spaces. Suppose that Φ is a code for a totally defined continuous function as described in Definition II.6.1 of Simpson [ 18 ]. Then there is a function $f : X \to Y$ such that for all n, a, r, b, and s, if $(n, a, r, b, s) \in Φ$ then $d (f (a), b) ⩽ s$ .

Proof.

Working in ${RCA}_{0}^{ω}$ , suppose X, Y, and Φ are as above. Fix $x \in X$ . Because x is in the domain of the function defined by Φ, for each m we can find $(n, a, r, b, s) \in Φ$ (occurring first in some fixed enumeration of quintuples) such that $d (x, a) < r$ and $s < 2^{- m - 1}$ . Set $f (x) (m) = b$ . The sequence $⟨ f (x) (m) : m \in N ⟩$ is a rapidly converging sequence of elements of Y converging to the desired value of $f (x)$ . Applying $QF - {AC}^{1, 0}$ , the system ${RCA}_{0}^{ω}$ proves the existence of f. (Note that different representations of $x \in X$ may yield different representations for $f (x)$ , though the function values will be equal in the space X.)

We now verify the last sentence of the lemma. Suppose $(n, a, r, b, s) \in Φ$ . Let $ε > 0$ and choose m so that $2^{- m - 1} < min {ε / 2, s}$ . Let $(n^{'}, a^{'}, r^{'}, b^{'}, s^{'}) \in Φ$ be the quintuple witnessing the value for $f (a) (m)$ . Then $d (a, a^{'}) < r^{'}$ and $s^{'} < 2^{- m - 1} < ε / 2$ . Let $r_{0} = min {r, r^{'} - d (a, a^{'})}$ . Then the ball $B (a, r_{0})$ is a subset of $B (a, r)$ , and is also a subset of $B (a^{'}, r^{'})$ . Applying property (2) of Simpson’s Definition II.6.1, we have $(a, r_{0}) Φ (b, s)$ and $(a, r_{0}) Φ (b^{'}, s^{'})$ . By property (1) of Simpson’s definition, $d (b, b^{'}) ⩽ s + s^{'} < s + ε / 2$ . By the choice of m, $d (b^{'}, f (a)) ⩽ 2^{- m} < ε / 2$ . By the triangle inequality $d (f (a), b) < s + ε$ . Because ε was an arbitrary positive value, $d (f (a), b) ⩽ s$ . □

The preceding lemma allows us to completely characterize the second-order theory of $(M_{[0, 1], R})$ .

Proposition 8.5.

The second-order theorems of ${RCA}_{0}^{ω} + (M_{[0, 1], R})$ are exactly the same as those of ${WKL}_{0}$ .

Proof.

As noted before, $(M_{[0, 1], R})$ is a consequence of Kohlenbach’s $(MUC)$ , and so any second-order theorem provable using $(M_{[0, 1], R})$ is provable in ${WKL}_{0}$ . It remains to show that $(M_{[0, 1], R})$ implies ${WKL}_{0}$ . By Theorem IV.2.3 of Simpson [18], it suffices to show that if f is a continuous function (coded by Φ) on $[0, 1]$ , then f is uniformly continuous. Suppose Φ codes a continuous function on $[0, 1]$ . By Lemma 8.4, ${RCA}_{0}^{ω}$ proves that there is a function $f : [0, 1] \to R$ matching the values of the coded function. Applying $(M_{[0, 1], R})$ , the function $M (f)$ is a modulus of uniform continuity for f, and so also for the function coded by Φ. Thus Φ codes a uniformly continuous function on $[0, 1]$ . □

For an alternative proof of Proposition 8.5, one could emulate the proof of Proposition 3.15 of Kohlenbach [12], applying the extensional model $ECF$ of the hereditarily continuous functionals.

We conclude by pointing out the potential and limitations of this section. The principle $(M_{[0, 1], R})$ can be viewed as a higher-order analogue of ${WKL}_{0}$ . A number of Skolemized forms of statements equivalent to ${WKL}_{0}$ may be equivalent to $(M_{[0, 1], R})$ over ${RCA}_{0}^{ω}$ . (But not all, as witnessed by Kohlenbach’s $UWKL$ . See Proposition 5.6.) However, $(M_{[0, 1], R})$ may not be the only reasonable candidate for a ${WKL}_{0}$ analogue. For example, reformulating $(M_{X, Y})$ for other spaces or different representations of continuous functions may affect the strength of the principle. There may be combinatorial principles (less affected by the details of formalization) that prove the same second-order sentences as ${WKL}_{0}$ . As noted in the last page of Kohlenbach’s article [12], the strength of these statements is related to the provability of the equivalence of their underlying second-order sentences over intuitionistic base systems.

References

Banach, Un théorème sur les transformations biunivoques, Fundamenta Mathematicae 6 (1924), 236–239. doi:10.4064/fm-6-1-236-239.

Brattka and

Gherardi, Weihrauch degrees, omniscience principles and weak computability, J. Symb. Log. 76(1) (2011), 143–176. doi:10.2178/jsl/1294170993.

D.D.

Dzhafarov and

Mummert, Reverse Mathematics – Problems, Reductions, and Proofs, Theory and Applications of Computability, Springer, Cham, 2022, ©[2022], p. xix+488. ISBN 978-3-031-11366-6; 978-3-031-11367-3. doi:10.1007/978-3-031-11367-3.

Feferman, Theories of finite type related to mathematical practice, in: Handbook of Mathematical Logic, Stud. Logic Found. Math., Vol. 90, North-Holland, Amsterdam, 1977, pp. 913–971. doi:10.1016/S0049-237X(08)71126-1.

T.J.

Grilliot, On effectively discontinuous type-2 objects, J. Symb. Log. 36 (1971), 245–248. doi:10.2307/2270259.

Hilbert and

Bernays, Grundlagen der Mathematik. Vol. II, J. W. Edwards, Ann Arbor, Michigan, 1944, p. xii+498. doi:10.1007/978-3-642-86896-2.

J.L.

Hirst, Combinatorics in subsystems of second order arithmetic, PhD thesis, The Pennsylvania State University, 1987. http://gateway.proquest.com/openurl?url_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:dissertation&res_dat=xri:pqdiss&rft_dat=xri:pqdiss:8728018.

J.L.

Hirst, Marriage theorems and reverse mathematics, in: Logic and Computation, Pittsburgh, PA, 1987, Contemp. Math., Vol. 106, Amer. Math. Soc., Providence, RI, 1990, pp. 181–196. doi:10.1090/conm/106/1057822.

Hunter, Higher-order reverse topology, PhD thesis, The University of Wisconsin–Madison, 2008. ISBN 978-0549-63366-2. http://gateway.proquest.com/openurl?url_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:dissertation&res_dat=xri:pqdiss&rft_dat=xri:pqdiss:3314296.

10.

Kohlenbach, On uniform weak König’s lemma, Commemorative Symposium Dedicated to Anne S. Troelstra (Noordwijkerhout, 1999) (2002), 103–116, ISSN 0168-0072. doi:10.1016/S0168-0072(01)00077-X.

11.

Kohlenbach, Foundational and mathematical uses of higher types, in: Reflections on the Foundations of Mathematics, Stanford, CA, 1998, Lect. Notes Log., Vol. 15, Assoc. Symbol. Logic, Urbana, IL, 2002, pp. 92–116. doi:10.1201/9781439863763.

12.

Kohlenbach, Higher order reverse mathematics, in: Reverse Mathematics 2001, Lect. Notes Log., Vol. 21, Assoc. Symbol. Logic, La Jolla, CA, 2005, pp. 281–295. doi:10.1017/9781316755846.018.

13.

Normann and

Sanders, On robust theorems due to Bolzano, Weierstrass, Jordan, and Cantor, J. Symb. Log. (2022), 1–51 (03 October, 2022). Volume data pending. doi:10.1017/jsl.2022.71.

14.

Normann and

Sanders, On the uncountability of

R

, J. Symb. Log. 87(4) (2022), 1474–1521. doi:10.1017/jsl.2022.27.

15.

Normann and

Tait, On the computability of the fan functional, in: Feferman on Foundations, Outst. Contrib. Log., Vol. 13, Springer, Cham, 2017, pp. 57–69. doi:10.1007/978-3-319-63334-3.

16.

J.B.

Remmel, On the effectiveness of the Schröder–Bernstein theorem, Proc. Amer. Math. Soc. 83(2) (1981), 379–386. doi:10.1090/S0002-9939-1981-0624936-X.

17.

Sakamoto and

Yamazaki, Uniform versions of some axioms of second order arithmetic, MLQ Math. Log. Q. 50(6) (2004), 587–593. doi:10.1002/malq.200310122.

18.

S.G.

Simpson, Subsystems of Second Order Arithmetic, 2nd edn, Perspectives in Logic, Cambridge University Press, Cambridge; Association for Symbolic Logic, Poughkeepsie, NY, 2009, p. xvi+444. ISBN 978-0-521-88439-6. doi:10.1017/CBO9780511581007.

19.

Weihrauch, The TTE-interpretation of three hierarchies of omniscience principles, Informatik Berichte 130(September) (1992), https://ub-deposit.fernuni-hagen.de/receive/mir_mods_00001147?lang=de.

Banach’s theorem in higher-order reverse mathematics

Abstract

Keywords

1. Introduction

Theorem 1.1 (Banach).

Theorem 1.4 ([8, Theorem 4.2]).

2. Formal theories

Proposition 4.1 ( RCA 0 ).

Proof. Proposition 6.6 shows that (1) implies (2). Because ( bB N ) is a restriction of ( B N ) , (2) implies (3) is immediate. Theorem 5.3 and Proposition 6.7 show that (3) implies (1). □ 7. Banach’s theorem on compact spaces

Proposition 7.1 ([12, Proposition 3.7]).

Lemma 7.2 ( RCA 0 ω + ( ∃ 2 ) ).

References

Proposition 4.1 ( ${RCA}_{0}$ ).

Proof.
Proposition 6.6 shows that (1) implies (2). Because $({bB}_{N})$ is a restriction of $(B_{N})$ , (2) implies (3) is immediate. Theorem 5.3 and Proposition 6.7 show that (3) implies (1). □
7. Banach’s theorem on compact spaces

Lemma 7.2 ( ${RCA}_{0}^{ω} + (\exists^{2})$ ).