Principle 2.14 ( ${\mathsf {CB}}{\mathbb N}$ ).

A countable set $A\subset {\mathbb R}$ is strongly countable if there exists a sequence $(x_{n})_{n\in {\mathbb N}}$ of pairwise distinct reals such that $(\forall n\in {\mathbb N})(x_{n}\in A)$ .

Proof Immediate from $[{\mathsf {CB}}{\mathbb N}+{\mathsf {cocode}}_{1}]\leftrightarrow {\mathsf {cocode}}_{0}$ and Theorems 2.5 and 2.10.

Proof The proof of [Reference Normann and Sanders73, Theorem 3.28] discusses a model $\textbf {Q}^{*}$ of ${\mathsf {Z}}_{2}^{\omega }+\neg {\mathsf {NBI}}$ , which implies that ${\mathsf {Z}}_{2}^{\omega }$ cannot prove ${\mathsf {NBI}}$ (or ${\mathsf {cocode}}_{1}$ ). This model is defined in [Reference Normann and Sanders73, Definition 2.28] and its properties are based on [Reference Normann and Sanders73, Lemma 2.16 and Theorem 2.17]. Here, we will explain the properties of $\textbf {Q}^{*}$ essential for the proof of our theorem, namely that this model satisfies ${\mathsf {CB}}{\mathbb N}+{\mathsf {IND}}_{0}$ . For the proofs of (most of) these properties, we refer to [Reference Normann and Sanders73].

First of all, the construction of the model is based on Kleene-computability relative to the functionals $\mathsf {S}^2_k$ , where $\mathsf {S}^2_k$ is the characteristic function of some complete $\Pi ^1_k$ -subset of ${\mathbb N}^{\mathbb N}$ . Using the Löwenheim–Skolem theorem, we let $A \subseteq {\mathbb N}^{\mathbb N}$ be a countable set such that all $\Pi ^1_k$ -formulas are absolute for A for all k. We let $(g_k)_{k \in {\mathbb N}}$ be an enumeration of A and we let $A_k$ be the set of functions computable in $\mathsf {S}^2_k$ and $\{g_0 , \ldots ,g_{k-1}\}$ . The key properties are that $A_k \subsetneq A_{k+1} \subsetneq A$ and that $A_{k+1}$ contains an enumeration of $A_k$ for each k.

Secondly, we let $\textbf {Q}[1] = A$ be the elements of the model of pure type 1. The definition of $\textbf {Q}[2]$ is as follows: If $F:A \rightarrow {\mathbb N}$ we let $F \in \textbf {Q}[2]$ if there is a $k_0$ such that for all $k \geq k_0$ , the restriction of F to $A_k$ is partially computable in $\mathsf {S}^2_k$ and $\{g_0 , \ldots , g_{k-1}\}$ . No uniformity is required. On top of this, we close $\textbf {Q}[1]$ and $\textbf {Q}[2]$ under Kleene computability hereditarily for each pure type. As proved in [Reference Normann and Sanders73], this will not add new elements of type 1 or type 2 to the structure. Finally, we use a canonical extension to interpretations of all finite types. The resulting type structure, named $\textbf {Q}^*$ in [Reference Normann and Sanders73], is a model of ${\mathsf {Z}}_2^{\omega }$ and satisfies our weak induction axioms ${\mathsf {IND}}_{0}$ and ${\mathsf {IND}}_{1}$ . Indeed, the models are constructed as computational closures, implying that for any sequence $ f_0 , \ldots , f_n$ of elements in the model, the coded sequence $(f_0 , \ldots , f_n)$ is also in the model, and the two induction axioms ${\mathsf {IND}}_{0}$ and ${\mathsf {IND}}_{1}$ readily follow.

Thirdly, having witnessed the construction of the model $\textbf {Q}^*$ , we now show that it satisfies that all infinite subsets of ${\mathbb N}^{\mathbb N}$ are strongly countable. In particular, we have that ${\mathsf {CB}}{\mathbb N}$ holds in $\textbf {Q}^{*}$ . To this end, fix some arbitrary $B \in \textbf {Q}[2]$ that is (the characteristic function of) an infinite subset of $A = \textbf {Q}[1]$ . We have established in the proof of [Reference Normann and Sanders73, Theorem 3.26] that $\textbf {Q}[2]$ contains a bijection $\phi :\textbf {Q}[1] \rightarrow {\mathbb N}$ with the extra property that $\phi _k$ , the restriction of $\phi $ to $A_k$ , is partially computable in $\mathsf {S}^2_k$ and $g_0 , \ldots , g_{k-1}$ . We do not need the explicit construction of $\phi $ : it suffices to split the argument for finding a bijection from B to ${\mathbb N}$ in two cases, as follows.

• • If $B \subseteq A_k$ for some k, then B is enumerable in $A_{k'}$ for some $k'> k$ (property of the model $\textbf {Q}^*$ ), and the inverse can be found directly.

• • In the ‘otherwise’ case, we construct an increasing sequence of functionals $ \psi _k: (B \cap A_k)\rightarrow {\mathbb N}$ as being equal to the restriction of $\phi $ to $B \cap A_k$ except at finitely many points; we use the finite set of exceptions to make $\psi :=\lim _{k\rightarrow \infty }\psi _{k}$ surjective. Now, for infinitely many k we have that $B \cap (A_{k+1} \setminus A_k) \neq \emptyset $ . At each stage where this is the case, and where the range of $A_k \cap B$ under $\psi _k$ is a proper subset of the range of $A_k$ under $\phi $ , we define $\psi _{k+1}$ as follows.

  • – Choose one element f in $B \cap (A_{k+1} \setminus A_k)$ . Let n be the least element in the range of $A_k$ under $\phi $ that is not in the range of $B \cap A_k$ under $\psi _k$ , and define $\psi _{k+1}(f) := n$ .

  • – We let $\psi _{k+1}$ be equal to $\phi $ on the rest of $B \cap (A_{k+1} \setminus A_k)$ , noticing that the injectivity of $\phi $ ensures that the value n used above will not be in the range of $A_{k+1} \setminus A_k$ under $\phi $ , so injectivity is preserved.

  Since B and $\phi $ are elements in $\textbf {Q}[2]$ and $\psi $ differs from the restriction of $\phi $ to B at only finitely many points in each $A_k$ , it follows that $\psi \in \textbf {Q}[2]$ .

The previous case distinction finishes the proof.

Principle 2.18 ( ${\mathsf {CB}}{\mathbb N}^{+}$ ).

Assume $A\subset [0,1]$ satisfies the following:

• • There is $F:[0,1]\rightarrow {\mathbb N}$ injective on A.

• • There is $(x_{n})_{n\in {\mathbb N}}$ consisting of pairwise distinct reals with $(\forall n\in {\mathbb N})(x_{n}\in A)$ .

Then there is $H:[0,1]\rightarrow {\mathbb N}$ which is bijective on A and such that for $x\in A$ either $H(x)=F(x) $ or $x= x_{H(x)}$ .

Proof We prove ${\mathsf {CB}}{\mathbb N}^{+}\rightarrow {\mathsf {BOOT}}_{C}^{-}$ and note that [Reference Normann and Sanders73, Theorem 3.23] yield $\Pi _{2}^{1}\text {-}\mathsf {CA}_{0}$ via $\Pi _{1}^{1}\text {-}{\mathsf {CA}}_{0}^{\omega }$ . Let $Y^{2}$ be such that $(\forall n\in {\mathbb N})(\exists \mbox { at most one }f\in 2^{{\mathbb N}}) (Y(f, n)=0)$ . Let $f_{0}$ be the constant zero function and define $A\subset {\mathbb N}\times 2^{{\mathbb N}}$ as follows:

$$\begin{align*}(m, f)\in A\leftrightarrow (\exists n\in {\mathbb N})[ (m=2n+1\wedge Y(n, f)=0) \vee (m=2n\wedge f=f_{0}) ]. \end{align*}$$

Modulo coding, we can view A as a subset of $2^{{\mathbb N}}$ . Define $F: A\rightarrow {\mathbb N}$ and $G:{\mathbb N}\rightarrow A$ as follows: $F\big ((k,f)\big ) := k$ and let $G(n): = (2n,f_{0})$ . Both functions are injective, so let $H : A \rightarrow {\mathbb N}$ be a canonical witness as in ${\mathsf {CB}}{\mathbb N}^{+}$ . Now consider the following:

(2.6) $$ \begin{align} (\exists f\in 2^{{\mathbb N}})(Y(f, n)=0)\leftrightarrow [H\big(2(2n+1),f_{0}\big) =2( 2n + 1)]. \end{align} $$

To prove (2.6), assume the left-hand side of (2.6) for fixed $n\in {\mathbb N}$ . Then there is $f\in 2^{{\mathbb N}}$ such that $(2n+1,f) \in A$ . Since this $(2n+1,f)$ is not in the range of G, we must have that $H(2n+1,f) = F(2n+ 1,f) = 2n + 1$ and $G(2n + 1) = (2(2n + 1),f_{0})$ . Since the case that $H(2(2n+1),f_{0}) = 2n+1$ (the inverse of G) violates that H is injective, we must have that $H(2(2n + 1), f_{0}) = 2(2n + 1)$ . Now assume the left-hand side of (2.6) is false for fixed $n\in {\mathbb N}$ . Then there is no $f\in 2^{{\mathbb N}}$ such that $F(f)=2n+1$ . Since there is an $m\in {\mathbb N}$ and a $g\in 2^{{\mathbb N}}$ such that $(m,g) \in A$ and $H(m,g) = 2n+1$ , we must have used the $G^{-1}$ -part of H and have that $m = 2(2n+1)$ and $g = f_0$ . This contradicts that $H (2(2n + 1), f_0 ) = 2(2n + 1)$ .

Proof The proof of Theorem 2.19 establishes the reverse direction over ${\mathsf {ACA}}_{0}^{\omega }$ . For the forward direction, we have ${\mathsf {BOOT}}_{C}^{-}\leftrightarrow {\mathsf {cocode}}_{0}$ over ${\mathsf {RCA}}_{0}^{\omega }$ by [Reference Sanders88, Theorem 3.6]. Now let A, F, and $(x_n)_{n \in {\mathbb N}}$ be as in the antecedent of Principle 2.18. The enumeration of A provided by ${\mathsf {cocode}}_0$ reduces the existence of a canonical witness for F and $(x_n)_{n \in {\mathbb N}}$ to the existence of a canonical witness for certain injections $f,g:{\mathbb N} \rightarrow {\mathbb N}$ . For the latter, the standard proofs of the Cantor–Bernstein theorem can be formalised in ${\mathsf {ACA}}_0$ , yielding the required canonical witness.

Principle 2.21. A non-enumerable and closed set in ${\mathbb R}$ has a limit point.

Principle 2.22 ( ${\mathsf {ccc}}$ ).

Let $A\subset {\mathbb R}^{2}$ be such that for any non-identical intervals $(a, b)$ and $(c, d)$ in A, the intersection is empty. Then A can be enumerated.

Principle 2.23 ( ${\mathsf {cloq}}$ ).

A countable linear ordering $(X, \preceq _{X})$ for $X\subset {\mathbb R}$ is order-isomorphic to a subset of ${\mathbb Q}$ .

Principle 2.24 ( ${\mathsf {cloq}}'$ ).

A countable and dense linear ordering without endpoints $(X, \preceq _{X})$ for $X\subset {\mathbb R}$ is order-isomorphic to ${\mathbb Q}$ .

Principle 2.25 ( ${\mathsf {CWO}}^{\omega }$ ).

For countable well-orders $(X, \preceq _{X}) $ and $ (Y, \preceq _{Y})$ where $X, Y\subset {\mathbb R}$ , the former order is order-isomorphic to the latter order or an initial segment of the latter order, or vice versa.

Proof Let $Y:[0,1)\rightarrow {\mathbb N}$ be an injection and use $\exists ^{2}$ to define $A\subset {\mathbb R}$ as follows:

(2.8) $$ \begin{align} x\in A \leftrightarrow (\exists n\in {\mathbb N})(n\leq x< n+1\wedge Y(x-n)=n). \end{align} $$

Intuitively, A is the set $\{z+Y(z): z\in [0,1)\}$ , although the latter need not exist (as a set) in ${\mathsf {ACA}}_{0}^{\omega }$ . Each $[m, m+1)\cap A$ has at most one element as $x, y \in \big ( [m, m+1)\cap A\big )$ implies $Y(x-m)=Y(y-m)$ by (2.8) and hence $x=_{{\mathbb R}}y$ by the injectivity of Y. In this light, A does not have a limit point, while this set is trivially closed.

Towards a contradiction, we now show that A is non-enumerable. Suppose $(x_{n})_{n\in {\mathbb N}}$ lists all elements of A, i.e., $(\forall x\in A)(\exists n\in {\mathbb N})(x=_{{\mathbb R}}x_{n})$ . Since we have $x\in A\leftrightarrow (Y(x- \lfloor x\rfloor )=\lfloor x\rfloor )$ for non-negative $x\in {\mathbb R}$ , the sequence $(x_{n}-\lfloor x_{n}\rfloor )_{n\in {\mathbb N}}$ lists all elements of $[0,1]$ . Indeed, for $y_{0}\in [0,1]$ , $(y_{0}+Y(y_{0}))\in A$ by definition and suppose $x_{n_{0}}=_{{\mathbb R}}y_{0}+Y(y_{0})$ . Hence, $\lfloor x_{n_{0}}\rfloor =Y(y_{0})$ , and hence $y_{0}=x_{n_{0}}-\lfloor x_{n_{0}}\rfloor $ . A sequence listing the reals in $[0,1)$ yields a contradiction by [Reference Simpson97, II.4.7].

Proof Let $B\subset [0,1]$ be a countable set, i.e., there exists $Y:[0,1]\rightarrow {\mathbb N}$ such that Y is injective on B. Without loss of generality, we may assume ${\mathbb Q}\cap B=\emptyset $ as Feferman’s $\mu ^{2}$ can enumerate the rationals in B. Similar to (2.8), we define the following set using $\exists ^{2}$ :

(2.9) $$ \begin{align} x\in A \leftrightarrow (\exists n\in {\mathbb N})(n\leq x< n+1\wedge Y(x-n)=n\wedge (x-n) \in B). \end{align} $$

Since Y is an injection on B, $[m, m+1)\cap A$ has at most one element for $m\in {\mathbb N}$ . Thus, A is a closed subset with no limit point. By the contraposition of Principle 2.21, there is a sequence $(x_{n})_{n\in {\mathbb N}}$ such that $x\in A\leftrightarrow (\exists n\in {\mathbb N})(x=x_{n})$ . Clearly, $(x_{n}-\lfloor x_{n}\rfloor ))_{n\in {\mathbb N}}$ yields an enumeration of B, and we are done.

Proof By Theorem 2.27, both ${\mathsf {PST}}$ and ${\mathsf {CBT}}$ imply Principle 2.21. If $\Pi _{1}^{1}\text {-}{\mathsf {CA}}_{0}^{\omega }$ could prove, e.g., ${\mathsf {PST}}$ , we would obtain $\Pi _{2}^{1}\text {-}\mathsf {CA}_{0}$ by [Reference Normann and Sanders73, Theorem 4.22]. However, $\Pi _{1}^{1}\text {-}{\mathsf {CA}}_{0}^{\omega }$ is $\Pi _{3}^{1}$ -conservative over $\Pi _{1}^{1}\text {-}{\mathsf {CA}}_{0}$ by [Reference Sakamoto and Yamazaki82, Theorem 2.2].

Principle 2.29 ( ${\mathsf {accu}}$ ).

For any closed $A\subseteq {\mathbb R}$ and $G:{\mathbb R}\rightarrow {\mathbb N}$ such that (2.10), there is $(x_{n})_{n\in {\mathbb N}}$ in A with $(\forall x\in {\mathbb R})\big (x\in A\leftrightarrow (\exists n\in {\mathbb N})(x=x_{n})\big )$ .

Principle 2.30 ( ${\mathsf {accu}}'$ ).

For any $A\subseteq {\mathbb R}$ and $G:{\mathbb R}\rightarrow {\mathbb N}$ such that (2.10), there is $(x_{n})_{n\in {\mathbb N}}$ in A with $(\forall x\in {\mathbb R})\big (x\in A\leftrightarrow (\exists n\in {\mathbb N})(x=x_{n})\big )$ .

Proof The equivalence (a) $\leftrightarrow $ (b) can be found in Theorem 2.11. We note that $\frac {1}{1+e^{x}}$ defines an injection from ${\mathbb R}$ to $(0,1)$ . Hence, using $\exists ^{2}$ , one readily extends ${\mathsf {cocode}}_{0}$ to subsets $A\subset {\mathbb R}$ .

The implication ${\mathsf {accu}}\rightarrow {\mathsf {cocode}}_{0}$ is (essentially) proved in Corollary 2.27, as the functional G as in (2.10) is readily defined in this case. To prove ${\mathsf {ccc}}\rightarrow {\mathsf {accu}}$ , let $A, G$ be as in the latter, i.e., satisfying (2.10). By the latter, we have that for $x, y\in A$ , the intersection $B(x, \frac {1}{2^{G(x)+1}})\cap B(y, \frac {1}{2^{G(y)+1}})$ is empty in case $x\ne y$ . We shall now define the set consisting of $ B(x, \frac {1}{2^{G(x)+1}})$ for $x\in A$ . To this end, define the set $B\subset {\mathbb R}^{2}$ as follows:

(2.11) $$ \begin{align}\textstyle (a, b)\in B\leftrightarrow \big[\frac{a+b}{2}\in A\wedge a=_{{\mathbb R}}\frac{a+b}{2}- \frac{1}{2^{G(\frac{a+b}{2})+1}} \wedge b=_{{\mathbb R}}\frac{a+b}{2}+ \frac{1}{2^{G(\frac{a+b}{2})+1}} \big]. \end{align} $$

Now apply ${\mathsf {ccc}}$ to the set B, which yield sequences $(a_{n})_{n\in {\mathbb N}}$ , $(b_{n})_{n\in {\mathbb N}}$ such that:

$$\begin{align*}(\forall a, b\in {\mathbb R})\big( (a, b)\in B\leftrightarrow (\exists n\in {\mathbb N})(a_{n}=a\wedge b_{n}=b)). \end{align*}$$

Then the sequence $(\frac {a_{n}+b_{n}}{2})_{n\in {\mathbb N}}$ enumerates A, and this implication is done.

For ${\mathsf {cocode}}_{0}\rightarrow {\mathsf {ccc}}$ , we first prove ${\mathsf {ccc}}_{0}$ in ${\mathsf {ACA}}_{0}^{\omega }$ . To the latter end, let $A\subset {\mathbb R}^{2}$ be as in ${\mathsf {ccc}}_{0}$ and fix some enumeration $(q_{n})_{n\in {\mathbb N}}$ of ${\mathbb Q}$ . Define $Y((a, b))$ as the least $n\in {\mathbb N}$ such that $q_{n}\in (a, b)$ if such there is, and $0$ otherwise. Clearly, Y is injective on A and the latter is countable, i.e., ${\mathsf {ccc}}_{0}$ follows inside ${\mathsf {ACA}}_{0}^{\omega }$ . Clearly, the combination ${\mathsf {cocode}}_{0}+{\mathsf {ccc}}_{0}$ implies ${\mathsf {ccc}}$ . Thus, ${\mathsf {cocode}}_{0}\rightarrow {\mathsf {ccc}}$ over ${\mathsf {ACA}}_{0}^{\omega }$ follows.

Finally, the reverse implication in ${\mathsf {accu}}\leftrightarrow {\mathsf {accu}}'$ is trivial. Now fix $A\subset {\mathbb R}$ and $G:{\mathbb R}\rightarrow {\mathbb N}$ satisfying (2.10). Then (2.11) yields a collection of open disjoint intervals in ${\mathbb R}$ . Since ${\mathsf {accu}}\rightarrow {\mathsf {ccc}}$ , this collection can be enumerated, yielding ${\mathsf {accu}}'$ .

Proof Note that ${\mathsf {ccc}}_{0}$ was proved in ${\mathsf {ACA}}_{0}^{\omega }$ in the proof of the theorem. To prove ${\mathsf {accu}}_{0}$ , note that (2.10) yields an injection to ${\mathbb Q}$ .

Proof For the second part, ${\mathsf {RCA}}_{0}^{\omega }$ proves ${\mathsf {ccc}}_{0}$ by the proof of the theorem. Applying ${\mathsf {CB}}{\mathbb N}$ to the conclusion of the former for infinite sets, one obtains ${\mathsf {ccc}}_{1}$ . The proof of ${\mathsf {ccc}}_{1}\rightarrow {\mathsf {accu}}_{1}$ follows from the proof of ${\mathsf {ccc}}\rightarrow {\mathsf {accu}}$ . Finally, the proof of Corollary 2.27 is readily adapted to ${\mathsf {accu}}_{1}\rightarrow {\mathsf {CB}}{\mathbb N}$ . For the first part, we note that ${\mathsf {accu}}_{1}$ only deals with infinite sets. To obtain the same results for finite sets $A\subset {\mathbb R}$ , consider the infinite set $B:=A\cup {\mathbb Q}$ and note that $\mu ^{2}$ can enumerate all elements in $A\cap {\mathbb Q}$ . Given an enumeration of B, one similarly obtains an enumeration of A.

Proof For ${\mathsf {cocode}}_{0}\rightarrow {\mathsf {CWO}}^{\omega }$ , use the proof that ${\mathsf {ATR}}_{0}\rightarrow {\mathsf {CWO}}$ over ${\mathsf {RCA}}_{0}$ from [Reference Simpson97, V.6.8]. Note that ${\mathsf {ACA}}_{0}^{\omega }+{\mathsf {BOOT}}_{C}^{-}$ proves ${\mathsf {ATR}}_{0}$ by [Reference Simpson97, V.5.2]. Recall that ${\mathsf {cocode}}_{0}\rightarrow {\mathsf {IND}}_{0}$ is proved in Theorem 2.7.

For $[{\mathsf {CWO}}^{\omega }+{\mathsf {IND}}_{0}]\rightarrow {\mathsf {cocode}}_{0}$ , let $Y:{\mathbb R}\rightarrow {\mathbb N}$ be injective on $A\subset [0,1]$ . In case $(\exists m\in {\mathbb N})(\forall x\in A)(Y(x)\leq m)$ , ${\mathsf {IND}}_{0}$ provides an enumeration of A as we have

$$\begin{align*}(\forall n\in {\mathbb N})(\exists \mbox{ at most one } x\in [0,1])(x\in A\wedge Y(x)=n). \end{align*}$$

Hence, we may assume $(\forall m\in {\mathbb N})(\exists x\in A)(Y(x)\geq m)$ . Now define the linear order $(A, \preceq _{A})$ via the following formula:

$$\begin{align*}x\preceq_{A} y \equiv \big[Y(y)=n_{0} \vee [ Y(x)\ne n_{0}\wedge Y(x)\leq_{{\mathbb N}}Y(y)] \big], \end{align*}$$

where $n_{0}\in {\mathbb N}$ is the least $n\in {\mathbb N}$ such that $(\exists x\in A)(Y(x)=n)$ ; this number is readily defined using ${\mathsf {IND}}_{0}$ . Let $y_{0}\in A$ be such that $Y(y_{0})=n_{0}$ . Intuitively, $(A,\preceq _{A})$ has order type $\omega +1$ , i.e., the order of ${\mathbb N}$ followed by one element. Hence, of the four different possibilities provided by the consequent of ${\mathsf {CWO}}^{\omega }$ , three lead to contradiction. Indeed, a finite initial segment of either $({\mathbb N}, \leq _{{\mathbb N}})$ or $(A, \preceq _{A})$ has only got finitely many elements (since Y is an injection), while ${\mathbb N}$ is infinite and A satisfies $(\forall m\in {\mathbb N})(\exists x\in A)(Y(x)\geq m)$ . Similarly, an order-isomorphism $W:A\rightarrow {\mathbb N}$ leads to contradiction as follows: since there is $y_{0}\in A$ such that $Y(y_{0})=n_{0}$ , there cannot be an injection from $A\setminus \{y_{0}\}$ to $\{0, 1,\dots , W(y_{0})\}$ , as the latter set is finite, while the former is not. Similarly, an order-isomorphism $Z:{\mathbb N}\rightarrow A$ yields a contradiction as any $n\geq n_{0}$ is mapped below $Z(n_{0})\in A$ (relative to $\preceq _{A}$ ), which is not possible as Y is an injection. The only remaining possibility is that ${\mathsf {CWO}}^{\omega }$ provides an order-isomorphism $Z: {\mathbb N}\rightarrow A\setminus \{y_{0}\}$ , where $A\setminus \{y_{0}\}=\{ y\in A: y \prec y_{0} \}$ is an initial segment of A. The morphism Z is then a sequence satisfying $(\forall x\in A\setminus \{y_{0}\}) (\exists n\in {\mathbb N})(Z(n)=_{{\mathbb R}}x)$ , i.e., we obtain an enumeration of A.

Proof To prove ${\mathsf {cocode}}_{0}\rightarrow {\mathsf {cloq}}$ , use the well-known ‘back-and-forth’ proof based on the enumeration of A (see [Reference Roitman78, p. 123]). By Theorem 2.11, we only need to prove ${\mathsf {cloq}}\rightarrow {\mathsf {range}}_{0}$ in ${\mathsf {ACA}}_{0}^{\omega }$ . To this end, fix $A\subset [0,1]$ and let $Y:[0,1]\rightarrow {\mathbb N}$ be countable in A. Wlog we may assume that $0, 1\not \in A$ . Now define the set $R\subset {\mathbb R}$ as follows: $y\in R$ if and only if we have either $(\exists n\in {\mathbb N})(y=_{{\mathbb R}}n)$ , or the following holds:

$$\begin{align*}(\exists q\in {\mathbb Q})(|y-q|\in A ) \wedge (\forall m\in {\mathbb N})(m<|y|<m+1\rightarrow Y(|y-q|)=m ). \end{align*}$$

Clearly, the set R is countable and $(R, \leq _{{\mathbb R}})$ is a linear order. Apply ${\mathsf {cloq}}$ to obtain $Q\subset {\mathbb Q}$ and $Z:R\rightarrow {\mathbb Q}$ such that Z is an order-isomorphism from $(R, \leq _{{\mathbb R}})$ to $(Q, \leq _{{\mathbb Q}})$ . Now consider the following formula where $n\in {\mathbb N}$ :

(2.12) $$ \begin{align} (\exists x\in A)(Y(x)=n) &\leftrightarrow (\exists y\in (n, n+1))(y\in R)\notag\\ &\leftrightarrow (\exists q\in Q)(Z(n)<_{{\mathbb Q}}q <_{{\mathbb Q}}Z(n+1)). \end{align} $$

The first equivalence holds by the definition of R, while the second equivalence follows from the fact that Z is an order-isomorphism. Since (2.12) is decidable given $(\exists ^{2})$ , ${\mathsf {range}}_{0}$ is now immediate.

Proof To prove ${\mathsf {cocode}}_{0}\rightarrow {\mathsf {cloq}}'$ , use the well-known ‘back-and-forth’ proof based on the enumeration of A (see [Reference Roitman78, p. 123]). To prove ${\mathsf {cloq}}'\rightarrow {\mathsf {range}}_{0}$ , fix $A\subset [0,1]$ and let $Y:[0,1]\rightarrow {\mathbb N}$ be countable in A. Wlog we may assume that $ A\cap {\mathbb Q}=\emptyset $ as Feferman’s $\mu ^{2}$ allows us to list the rationals in A. Now define the set $R'\subset {\mathbb R}$ as follows: $y\in R'$ if and only if we have either $(\exists q\in {\mathbb Q})(y=_{{\mathbb R}}q)$ , or the following holds:

$$\begin{align*}(\exists q\in {\mathbb Q})(|y-q|\in A ) \wedge (\forall m\in {\mathbb N})(m<_{{\mathbb R}}|y|<_{{\mathbb R}}m+1\rightarrow Y(|y-q|)=m ). \end{align*}$$

Clearly, the set $R'$ is countable and $(R', \leq _{{\mathbb R}})$ is a dense linear order without end points. Apply ${\mathsf {cloq}}'$ to obtain an order-isomorphism Z from $(R', \leq _{{\mathbb R}})$ to $({\mathbb Q}, \leq _{{\mathbb Q}})$ . Now consider the following formula where $n\in {\mathbb N}$ :

(2.13) $$ \begin{align} (\exists x\in A)(Y(x)=n) &\leftrightarrow (\exists y\in (n, n+1))(y\in R' \wedge y \mbox{ is irrational})\\ &\leftrightarrow (\exists q\in {\mathbb Q}\cap (Z(n), Z(n+1)) )(\forall r\in {\mathbb Q}\cap (n, n+1))(Z(r)\ne_{{\mathbb Q}} q ).\notag \end{align} $$

The first equivalence holds by definition while the second equivalence follows from the fact that Z is an order-isomorphism. As for the theorem, ${\mathsf {range}}_{0}$ follows.