Proof. Let $\langle \cdot , \cdot \rangle \colon \mathbb {N} \times \mathbb {N} \to \mathbb {N}$ be a computable bijection and for each $i \in \mathbb {N}$ fix a listing $(x^i_n)_{n \in \mathbb {N}}$ of the elements of $P_i$ . We define simultaneously for each i a linear order $\trianglelefteq _i$ which extends $\preceq _i$ and is $\preceq _i$ computable. We proceed by stages. Suppose we are at stage $s = \langle i,m \rangle $ : we want to stipulate the $\lhd _i$ comparabilities of $x^i_m$ . For each $\langle i,n \rangle < s$ , if there is $\langle i,n' \rangle < s$ such that $x^i_{n'} \prec _i x^i_m$ and $x^i_n \lhd _i x^i_{n'}$ then we put $x^i_n \lhd _i x^i_m$ . Otherwise we put $x^i_m \lhd _i x^i_n$ .

Then for each i each relation $\trianglelefteq _i$ extends the corresponding $\preceq _i$ and for any $x,y \in P_i$ such that $x \ne y$ , either $x \lhd _i y$ or $y \lhd _i x$ . Moreover, $\trianglelefteq _i$ is still a poset and it is computable from $\preceq _i$ as required.

Proof. If $(P, \preceq )$ is a chain, then $\{ \preceq \}$ is a realization.

Assume that $(P, \preceq )$ is not a chain and let $a,b \in P$ be such that $a \mid b$ . We extend $(P, \preceq )$ to another poset $(P, \preceq _a^b)$ in the following way: for each $x,y \in P$ we stipulate that $x \preceq _a^b y$ if and only if either $x \preceq y$ or $x \preceq a \wedge b \preceq y$ . Notice that such relation exists in $\mathsf {RCA}_0$ , ${\preceq } \subseteq {\preceq _a^b}$ and $a \preceq _a^b b$ . It is straightforward to check that $(P, \preceq _a^b)$ is a poset.

By Theorem 2.3, for each $a,b \in P$ such that $a \mid b$ , there exists a linearization $\trianglelefteq _a^b$ of $(P, \preceq _a^b)$ . It is clear that if $x \mid y$ then $x \ntrianglelefteq _y^x y$ , so that $\{\trianglelefteq _a^b: a,b \in P, a \mid b\}$ realizes $(P, \preceq )$ .

Proof. Let P and R be the disjoint unions, respectively, of $(P_i)_{i \in \mathbb {N}}$ and $(R_i)_{i \in \mathbb {N}}$ . Then R is an acyclic relation on the set P and we can apply 4 of Theorem 2.5 to get a partial order $(P, \preceq )$ which extends R. Each restriction of $\preceq $ to $P_i$ is a partial order extending $R_i$ .

Proof. To prove that $\dim (F_n) \ge n$ it suffices to show that for every linearization $\trianglelefteq $ of $F_n$ there exists at most one $k<n$ such that $b_k \trianglelefteq a_k$ . In fact, if $b_k \trianglelefteq a_k$ and $b_{k'} \trianglelefteq a_{k'}$ for $k \ne k'$ , then

$$ \begin{align*}b_{k'} \trianglelefteq a_{k'} \trianglelefteq b_k \trianglelefteq a_k \trianglelefteq b_{k'},\end{align*} $$

and by antisymmetry of $\trianglelefteq $ we obtain $a_k = a_{k'} = b_k = b_{k'}$ , a contradiction.

For the converse it suffices to define a realization consisting of exactly n linearizations. For each $i < n$ let $\trianglelefteq _i$ be the following linearization of $F_n$ :

$$ \begin{align*} a_0 \trianglelefteq_i \ldots \trianglelefteq_i a_{i-1} \trianglelefteq_i a_{i+1} \trianglelefteq_i &\ldots \trianglelefteq_i a_{n-1} \trianglelefteq_i b_i \trianglelefteq_i \\ &\trianglelefteq_i a_i \trianglelefteq_i b_{n-1} \trianglelefteq_i \ldots b_{i+1} \trianglelefteq_i b_{i-1} \trianglelefteq_i \ldots \trianglelefteq_i b_0. \end{align*} $$

Each $\trianglelefteq _i$ exists in $\mathsf {RCA}_0$ by $\boldsymbol \Sigma ^{0}_{0}$ -comprehension. We claim that $\{\trianglelefteq _0, \ldots , \trianglelefteq _{n-1}\}$ realizes $F_n$ . If $x \mid y$ we need to find some i such that $x \ntriangleleft _i y$ . If $x=a_j$ and $y=a_k$ for $j \ne k$ it holds that $a_j \ntriangleleft _j a_k$ . If $x=b_j$ and $y = b_k$ for $j \ne k$ it holds that $b_j \ntriangleleft _k b_k$ . If $x=b_j$ and $y = a_j$ it holds that $b_j \ntriangleleft _k a_j$ for any $k \ne j$ . Finally, if $x=a_j$ and $y = b_j$ it holds that $a_j \ntriangleleft _j b_j$ .

We conclude that $\{\trianglelefteq _0, \ldots , \trianglelefteq _{n-1}\}$ realizes $F_n$ and so $\dim (F_n) = n$ .

Proof. If $n = 2$ the result is trivial so we may assume $n> 2$ . For each $k < n$ , the existence of i is trivial since $a_k \mid b_k$ .

To prove uniqueness suppose, without loss of generality, that $b_{n-1} \trianglelefteq _{n-1} a_{n-1}$ and $b_{n-1} \trianglelefteq _{n-2} a_{n-1}$ . Then, by the first argument in the proof of Theorem 2.9, the set of restrictions of $\{\trianglelefteq _0, \ldots , \trianglelefteq _{n-3}\}$ to $F_{n-1}$ realizes $F_{n-1}$ , against Theorem 2.9 itself.

Proof. The implication from (1) to (2) is a straightforward application of $\mathsf {WKL}_0$ and the details are left to the reader, while (3) is an easy consequence of (dim2).

We now deal with the implication from (3) to (1) and exploit item 2 of Theorem 2.5. Let $f,g$ be 1–1 functions with disjoint ranges: we want to show that there exists a set A such that $\operatorname {ran}(f) \subseteq A$ and $A \cap \operatorname {ran}(g) = \emptyset $ . We construct a poset $(P^k,\preceq )$ (recall that $k \geq 3$ is fixed) that will be used for many reversals in Section 4. Let

$$ \begin{align*}P^k=\{x^i,y^i:i \in \mathbb{N}\} \cup \{c_j^r,d_j^r: j < k-1, r \in \mathbb{N}\} \cup \{p_j^s,q_j^s: j < k-1, s \in \mathbb{N}\}.\end{align*} $$

To partially order $P^k$ we start with a level function $\ell : P \rightarrow \mathbb {N}$ defined by

$$ \begin{align*}\ell (z) = \begin{cases} i & \text{if } z=x^i,y^i; \\ f(r) & \text{if } z=c_j^r,d_j^r; \\ g(s) & \text{if } z=p_j^s,q_j^s. \end{cases} \end{align*} $$

Notice that $\mathsf {RCA}_0$ suffices to prove the existence of $\ell $ . For every n let $P^k_n = \{z \in P^k: \ell (z)=n\}$ : we say that $P^k_n$ is a level of $P^k$ . Since f is 1–1, $c^r_j$ and $d^{r'}_h$ belong to the same level if and only if $r = r'$ , and the same holds for $p^s_j$ and $q^{s'}_h$ . Furthermore we have $\ell (c^r_j) \neq \ell (p^s_h)$ for all r, s, j, and h.

We define the strict partial order $\prec $ by setting for each $u, v \in P$ :

• • if $\ell (u) < \ell (v)$ then $u \prec v$ ;

• • if $\ell (u) = \ell (v) = m$ then $u \prec v$ if and only if one of the following six alternatives holds:

  $$ \begin{align*}{2} u =x^m,\, v = d^r_j,\, f(r) =m & \quad\qquad u =p^s_j,\, v=x^m,\, g(s)=m\\ u =c^r_j,\, v =y^m,\, f(r) =m & \quad\qquad u =y^m,\, v=q^s_j,\, g(s)=m\\ u =c^r_j,\, v=d^r_{j'},\, j \ne j',\, f(r) =m & \quad\qquad u =p^s_j,\, v=q^s_{j'},\, j \ne j',\, g(s)=m. \end{align*} $$

To check that $(P^k,\preceq )$ is a partial order, notice that asymmetry is trivial, while transitivity is immediate when the elements belong to different levels (because the levels are linearly ordered by $\preceq $ as the natural numbers) and follows easily in the other case because no level has chains of length $3$ .

If $m \notin \operatorname {ran}(f) \cup \operatorname {ran}(g)$ then $P^k_m = \{x^m, y^m\}$ is an antichain. If $f(r)=m$ the level $P^k_m$ is a copy of $F_k$ where $\{x^m,c^r_0,\ldots ,c^r_{k-2}\}$ is the set of the $a_i$ ’s while $\{y^m,d^r_0,\ldots ,d^r_{k-2}\}$ is the set of the $b_i$ ’s (recall the notation of Definition 2.8). The figure below illustrates level m:

Similarly, if $g(s)=m$ the level $P^k_m$ is a copy of $F_k$ where $\{y^m,p^s_0,\ldots ,p^s_{k-2}\}$ is the set of the $a_i$ ’s while $\{x^m,q^s_0,\ldots ,q^s_{k-2}\}$ is the set of the $b_i$ ’s. The figure below illustrates level m in this case:

Notice that in $\mathsf {RCA}_0$ we can realize each level with k linearizations and the levels are linearly ordered. If Q is a finite subset of $P^k$ then Q intersects finitely many $P^k_m$ and, using bounded $\boldsymbol \Sigma ^{0}_{1}$ -comprehension which is available in $\mathsf {RCA}_0$ , we know how to realize each of these levels. Hence $\dim (Q,\preceq ) \leq k$ and by (3) we have $\dim (P^k,\preceq ) \le k$ . Let $\{\trianglelefteq ^*_i : i < k\}$ be a set of linearizations which realizes $(P^k,\preceq )$ . Notice that for each $i < k$ , the restriction of $\trianglelefteq ^*_i$ to the level $P^k_m$ is a linearization of $(P^k_m, \preceq )$ and the set of these restrictions realizes $(P^k_m, \preceq )$ . We already noticed that $P^k_m$ is either an antichain of two elements or a copy of $F_k$ . By Lemma 2.10 if $m \in \operatorname {ran}(f)$ then $|\{i < k : y^m \trianglelefteq ^*_i x^m\}| =1$ while if $m \in \operatorname {ran}(g)$ then $|\{i < k : y^m \trianglelefteq ^*_i x^m\}| =k-1$ . If $m \notin \operatorname {ran}(f) \cup \operatorname {ran}(g)$ we only know that $1 \le |\{i < k : y^m \trianglelefteq ^*_i x^m\}| \le k-1$ . If we let

$$ \begin{align*}A = \{m : |\{i < k : y^m \trianglelefteq^*_i x^m\}| =1 \}\end{align*} $$

we have $\operatorname {ran}(f) \subseteq A$ and $A \cap \operatorname {ran}(g) = \emptyset $ , as desired.

Proof. For each $i \in \mathbb {N}$ define $R_i^0$ and $R_i^1$ over $P_i$ as follows:

$$ \begin{align*} x R_i^0 y & \text{ if and only if } x \mid y \land x \in C_i^0 \land y \notin C_i^0;\\ x R_i^1 y & \text{ if and only if } x \mid y \land x \notin C_i^1 \land y \in C_i^1. \end{align*} $$

We claim that each $R_i = {\preceq _i} \cup R_i^0 \cup R_i^1$ is acyclic. Assume that

$$ \begin{align*}x_0 R_i x_1 R_i \ldots R_i x_{m-1} R_i x_0.\end{align*} $$

Since $\preceq _i$ is transitive, we may assume that it does not occur twice consecutively. It is immediate that also each of $R_i^0$ or $R_i^1$ cannot occur twice consecutively. Since the chains are incomparable we cannot have $x_j R_i^1 x_{j+1} R_i^0 x_{j+2}$ and $x_j R_i^1 x_{j+1} {\preceq _i} x_{j+2} R_i^0 x_{j+3}$ as well.

If $R_i^1$ occurs in the cycle, up to renaming its elements, we may assume that $x_0 R_i^1 x_1 \preceq _i x_2 \ldots $ and then $R_i^0$ does not occur. Therefore $\preceq _i$ and $R_i^1$ alternate in the cycle and this entails that m is even. Hence, the cycle has the form

$$ \begin{align*}x_0 R_i^1 x_1 {\preceq_i} \ldots R_i^1 x_{m-1} {\preceq_i} x_0.\end{align*} $$

For each $j < \frac {m}{2}$ we have that $x_{2j} \notin C_i^1$ while $x_{2j+1} \in C_i^1$ . We claim that for each $j < \frac {m}{2}-1$ , $x_{2j+1} \preceq _i x_{2j+3}$ . Indeed $x_{2j+1} \preceq _i x_{2j+2}$ and $x_{2j+2} \mid x_{2j+3}$ . Since $x_{2j+1}, x_{2j+3} \in C_i^1$ it must be $x_{2j+1} \preceq _i x_{2j+3}$ . Thus $x_1 \preceq _i x_{m-1} \preceq _i x_0$ , contradicting $x_0 \mid x_1$ .

If $R_i^1$ does not occur in the cycle, then $R_i^0$ does and an analogous argument leads to a contradiction, completing the proof of the claim.

By Corollary 2.6, which is the step where we use $\mathsf {WKL}_0$ , and by Theorem 2.3 the relations $(R_i)_{i \in \mathbb {N}}$ can be extended to linear orders $(\trianglelefteq _i)_{i \in \mathbb {N}}$ which have the prescribed properties.

Proof. Lemma 4.2 proves that (1) implies (2).

For the converse let $f,g$ be 1–1 functions with disjoint ranges and let $P=\{z\} \cup \{x_n,a_n,b_n : n \in \mathbb {N}\}$ . We define a partial order $\preceq $ on P as follows:

• • $a_i \preceq a_j$ if and only if $i < j$ ;

• • $b_i \preceq b_j$ if and only if $j < i$ ;

• • $x_n \preceq a_i$ if and only if $\exists j < i+1\, f(j) = n$ ;

• • $b_i \preceq x_n$ if and only if $\exists j < i+1\, g(j) = n$ .

Let $C_0 = \{a_n : n \in \mathbb {N}\}$ and $C_1 = \{b_n : n \in \mathbb {N}\}$ which are incomparable chains. By (2) let $\trianglelefteq $ be a linearization of $\preceq $ that puts $C_0$ at the bottom and $C_1$ at the top of P. The set $\{n : x_n \trianglelefteq z\}$ separates $\operatorname {ran}(f)$ and $\operatorname {ran}(g)$ .

Proof. Let $(P, \preceq )$ be a poset, fix $n> 1,$ and a set of pairwise incomparable chains $C_i \subseteq P$ for $i < n$ . Let $C = \bigcup _{i < n} C_i$ . Our goal is to prove that $\dim (P, \preceq ) \le \dim (P \setminus C, \preceq ) + n$ .

Fix m and a set of linearizations $\{\trianglelefteq _0, \ldots , \trianglelefteq _{m-1}\}$ realizing $P \setminus C$ . We construct a set of $m+n$ linear orders which realizes P.

For each $i < m$ let ${\preceq _i^*} = {\preceq } \cup {\trianglelefteq _i}$ . We claim that each $\preceq _i^*$ is acyclic. Towards a contradiction, let $x_0, \ldots , x_{\ell -1}$ be such that

$$ \begin{align*}x_0 \preceq_i^* x_1 \preceq_i^* \ldots \preceq_i^* x_{\ell-1} \preceq_i^* x_0.\end{align*} $$

Since both $\preceq $ and $\trianglelefteq _i$ are transitive relations we may assume that $\ell $ is even

$$ \begin{align*}x_0 \preceq x_1 \trianglelefteq_i \ldots \preceq x_{\ell-1} \trianglelefteq_i x_0.\end{align*} $$

Since $\trianglelefteq _i$ is a relation over $P \setminus C$ , it follows that for each $j < \ell \, x_j \in P \setminus C$ . By the fact that $\trianglelefteq _i$ extends $\preceq $ on its domain, we may replace each occurrence of $\preceq $ with $\trianglelefteq _i$ obtaining a cycle with respect to $\trianglelefteq _i$ , a contradiction.

By Corollary 2.6 and Theorem 2.3 each $\preceq _i^*$ can be extended to a linear order $\trianglelefteq _i^*$ .

Next we build n further linearizations to deal with the chains $C_i$ for $i < n$ . We apply Lemma 4.2 to the n pairs of chains $C_{[j]_n}, C_{[j+1]_n}$ for $j < n$ , where $[j]_n$ is the residue class of j modulo n. We obtain a sequence of linear orders $(\trianglelefteq ^*_{m+j})_{j < n}$ , each extending $(P, \preceq )$ and such that $\trianglelefteq ^*_{m+j}$ puts $C_{[j]_n}$ at the bottom and $C_{[j+1]_n}$ at the top of P.

We are left to prove that the set $\{\trianglelefteq ^*_0, \ldots , \trianglelefteq ^*_{m+n-1}\}$ realizes $(P,\preceq )$ . As we noticed in Section 2 it suffices to prove that for each $x,y \in P$ such that $x \mid y$ , there exists $i < m+n$ such that $x \ntrianglelefteq ^*_i y$ :

1. (1) if $x \in C_i$ then $\trianglelefteq ^*_{m + [i-1]_n}$ , which puts $C_i$ at the top of P, works;

2. (2) if $y \in C_i$ then $\trianglelefteq ^*_{m + [i]_n}$ , which puts $C_i$ at the bottom of P, works;

3. (3) if $x,y \in P \setminus C$ then recall that $\{\trianglelefteq _0, \ldots , \trianglelefteq _{m-1}\}$ realizes $P \setminus C$ ; hence there exists $i < n$ such that $x \ntrianglelefteq _i y$ and consequently $\trianglelefteq ^*_i$ , which extends $\trianglelefteq _i$ , works.

Therefore $\dim (P, \preceq ) \le \dim (P \setminus C, \preceq ) + n$ .

Proof. Let $(P, \preceq )$ be a poset and $C \subseteq P$ a chain. Then, applying Theorem 4.4 with $n = 2$ , $C_0 = C,$ and $C_1 = \emptyset $ , we have $\dim (P,\preceq ) \le \dim (P \setminus C, \preceq )+2$ .

Proof. Let $(P, \preceq )$ be a poset. For $i < n$ let $C_i \subseteq P$ be chains and $C = \bigcup _{i < n} C_i$ . We need to prove that $\dim (P, \preceq ) \le \dim (P \setminus C, \preceq ) + 2n$ .

Fix m and a set of linearizations $\{\trianglelefteq _0, \ldots , \trianglelefteq _{m-1}\}$ which realizes $(P \setminus C, \preceq )$ . We construct a set of $m+2n$ linear orders which realizes $(P,\preceq )$ .

For each $i < m$ we extend $\trianglelefteq _i$ to a linearization $\trianglelefteq ^*_i$ of $(P, \preceq )$ as we did in Theorem 4.4.

We then apply Lemma 4.2 to the poset P and to the $2n$ pairs of chains $C_i, \emptyset $ and $\emptyset , C_i$ for $i < n$ . We obtain linearizations $\{\trianglelefteq ^*_{m+j}\}_{j < 2n}$ such that if $j < 2n$ is even (resp. odd) then $\trianglelefteq ^*_{m+j}$ is the linearization of P that puts $C_{\frac {i}{2}}$ at the bottom (resp. that puts $C_{\frac {i-1}{2}}$ at the top).

Showing that the set $\{\trianglelefteq ^*_0, \ldots , \trianglelefteq ^*_{m+2n-1}\}$ realizes $(P,\preceq )$ is similar to the analogous proof in Theorem 4.4.

Proof. Theorem 4.4 proves that (1) implies (2), while Theorem 4.6 shows that (1) implies (4). (2) implies (3), and (4) implies (5) are obvious (notice that $\mathsf {DBi_{1}}$ and $\mathsf {DBc_{1}}$ coincide). The proof of Corollary 4.5 shows that (3) implies (5). Therefore we are left to prove that (5) implies (1).

Let $f,g$ be 1–1 functions with disjoint ranges: we want to show that there exists a set A such that $\operatorname {ran}(f) \subseteq A$ and $A \cap \operatorname {ran}(g) = \emptyset $ . We consider the poset $P^4$ , which is the case $k=4$ of the poset defined in the proof of Theorem 2.11.

If $m \notin \operatorname {ran}(f) \cup \operatorname {ran}(g)$ then $P^4_m = \{x^m, y^m\}$ is an antichain. If $f(r)=m$ or $g(s)=m$ , then the level $P^4_m$ is one of the two copies of $F_4$ below:

Albeit we can realize each level with at most four linearizations, in $\mathsf {RCA}_0$ we cannot define a set of four linearizations of $\preceq $ that realize $\dim (P^4, \preceq )$ . Indeed, to do so we need to know whether $m \in \operatorname {ran}(f)$ (in which case Lemma 2.10 implies that three of the linearizations need to put $x^m$ below $y^m$ ) or $m \in \operatorname {ran}(g)$ (in which case three of the linearizations need to put $x^m$ above $y^m$ ).

Let $C = \{c^r_1,d^r_2,p^s_1,q^s_2: r,s \in \mathbb {N}\}$ and notice that it is a chain. We now consider the poset $(P^4 \setminus C, \preceq )$ . If $m \in \operatorname {ran}(f)$ or $m \in \operatorname {ran}(g)$ then $P^4_m \setminus C$ has one of the following forms:

We claim that $\dim (P^4 \setminus C, \preceq ) = 2$ . First notice that for each m we have that $x^m,y^m \notin C$ and $x^m \mid y^m$ . Therefore $\dim (P^4 \setminus C,\preceq ) \ge 2$ . We now exhibit two linearizations $\trianglelefteq _0$ and $\trianglelefteq _1$ that realize $(P^4 \setminus C, \preceq )$ . We define $\trianglelefteq _0$ by:

• • if $u \preceq v$ then $u \trianglelefteq _0 v$ ;

• • $x^m \trianglelefteq _0 y^m$ ;

• • for each r if $f(r) = m$ then $x^m \trianglelefteq _0 c^r_2 \trianglelefteq _0 d^r_0 \trianglelefteq _0 c^r_0 \trianglelefteq _0 d^r_1 \trianglelefteq _0 y^m$ ;

• • for each s if $g(s) = m$ then $p^s_0 \trianglelefteq _0 p^s_2 \trianglelefteq _0 x^m \trianglelefteq _0 y^m \trianglelefteq _0 q^s_1 \trianglelefteq _0 q^s_0$ .

In a similar fashion, we define $\trianglelefteq _1$ :

• • if $u \preceq v$ then $u \trianglelefteq _1 v$ ;

• • $y^m \trianglelefteq _1 x^m$ ;

• • for each r if $f(r) = m$ then $c^r_0 \trianglelefteq _1 c^r_2 \trianglelefteq _1 y^m \trianglelefteq _1 x^m \trianglelefteq _1 d^r_1 \trianglelefteq _1 d^r_0$ ;

• • for each s if $g(s) = m$ then $y^m \trianglelefteq _1 p^s_2 \trianglelefteq _1 q^s_0 \trianglelefteq _1 p^s_0 \trianglelefteq _1 q^s_1 \trianglelefteq _1 x^m$ .

To prove that $\trianglelefteq _0$ and $\trianglelefteq _1$ realize the poset, we need to show that if $u \mid v$ then either $u \ntrianglelefteq _0 v$ or $u \ntrianglelefteq _1 v$ . Since $u \mid v$ implies $\ell (u) = \ell (v)$ there are at most $16$ cases, that are easily checked.

Now, (5) implies that $\dim (P^4, \preceq ) \le 4$ and, as in the proof of Theorem 2.11, a set separating the ranges of f and g is $\{m : |\{i < 4 : y^m \trianglelefteq ^*_i x^m\}| =1 \}$ .

Proof. The forward direction is proved in Theorem 4.4.

For the backward direction, given f and g we consider the same poset $(P^4, {\preceq })$ of the proof of Theorem 4.7. Let $C_0$ be the chain called C in that proof and let $C_1 = C_2 = \emptyset $ (viewed as a chain). The poset $(P^4 \setminus (C_0 \cup C_1 \cup C_2), {\preceq })$ coincides with $(P^4 \setminus C, \preceq )$ and has dimension $2$ . By $\mathsf {DBi_{3}}$ we get that $\dim (P^4,{\preceq }) \le 5$ and we can fix a set $\{\trianglelefteq _0, \trianglelefteq _1, \trianglelefteq _2, \trianglelefteq _3, \trianglelefteq _4\}$ of linearizations which realizes $(P^4, {\preceq })$ .

If $f(r) = m$ for some r, then three distinct linearizations have to deal with the incomparabilities $c^r_0 \mid d^r_0$ , $c^r_1 \mid d^r_1$ , and $c^r_2 \mid d^r_2$ in $P^4_m$ . This means that if $m \in \operatorname {ran}(f)$ then $|\{i < 5 : y^m \trianglelefteq ^*_i x^m\} | \le 2$ . Analogously if $m \in \operatorname {ran}(g)$ then $| \{i < 5 : y^m \trianglelefteq ^*_i x^m\} | \ge 3$ . Therefore we can define the separator set A as the set of $m \in \mathbb {N}$ such that $| \{i < 5 : y^m \trianglelefteq ^*_i x^m\} | \le 2$ .

Proof. Theorem 4.6 shows one implication, so we deal with the converse.

If $n = 1$ then $\mathsf {DBc_{1}}$ is $\mathsf {DBi_{1}}$ and the implication was proved in Theorem 4.7. So fix $n> 1$ and as usual let $f,g$ be 1–1 functions with disjoint ranges and consider the poset $P^{2n+2}$ , which is the case $k=2n+2$ of the poset defined in the proof of Theorem 2.11.

If $m \notin \operatorname {ran}(f) \cup \operatorname {ran}(g)$ then $P^{2n+2}_m = \{x^m, y^m\}$ is an antichain. If $f(r)=m$ or $g(s)=m$ , then the level $P^{2n+2}_m$ is one of the two copies of $F_{2n+2}$ below:

For $1 \le i \le n$ consider the chain $C_i = \{c^r_{2i}, d^r_{2i-1}, p^s_{2i}, q^s_{2i-1}: r,s \in \mathbb {N}\}$ . Let $C = \bigcup _{i = 1}^n C_i$ . If $m \in \operatorname {ran}(f)$ or $m \in \operatorname {ran}(g)$ then $P^{2n+2}_m \setminus C$ has one of the following forms:

We claim that $\dim (P^{2n+2} \setminus C, \preceq ) = 2$ . First notice that $P^{2n+2} \setminus C$ is not a chain and so $\dim (P^{2n+2} \setminus C, \preceq ) \ge 2$ . Hence it suffices to exhibit two linearizations $\trianglelefteq _0$ and $\trianglelefteq _1$ that realize $(P^{2n+2} \setminus C, \preceq )$ . We define $\trianglelefteq _0$ in the following way:

• • if $z_1 \preceq z_2$ then $z_1 \trianglelefteq _0 z_2$ ;

• • $x^m \trianglelefteq _0 y^m$ ;

• • for each r if $f(r) = m$ then

  $$ \begin{align*}x^m \trianglelefteq_0 c^r_{2n-1} \trianglelefteq_0 \ldots \trianglelefteq_0 c^r_1 \trianglelefteq_0 d^r_0 \trianglelefteq_0 c^r_0 \trianglelefteq_0 d^r_2 \trianglelefteq_0 \ldots \trianglelefteq_0 d^r_{2n} \trianglelefteq_0 y^m;\end{align*} $$

• • for each s if $g(s) = m$ then

  $$ \begin{align*}p^s_0 \trianglelefteq_0 \ldots \trianglelefteq_0 p^s_{2n-1} \trianglelefteq_0 x^m \trianglelefteq_0 y^m \trianglelefteq_0 q^s_{2n} \trianglelefteq_0 \ldots \trianglelefteq_0 q^s_0.\end{align*} $$

In a similar fashion, we define $\trianglelefteq _1$ :

• • if $z_1 \preceq z_2$ then $z_1 \trianglelefteq _1 z_2$ ;

• • $y^m \trianglelefteq _1 x^m$ ;

• • for each r if $f(r) = m$ then

  $$ \begin{align*}c^r_0 \trianglelefteq_1 \ldots \trianglelefteq_1 c^r_{2n-1} \trianglelefteq_1 y^m \trianglelefteq_1 x^m \trianglelefteq_1 d^r_{2n} \trianglelefteq_1 \ldots \trianglelefteq_1 d^r_0;\end{align*} $$

• • for each s if $g(s) = m$ then

  $$ \begin{align*}y^m \trianglelefteq_0 p^s_{2n-1} \trianglelefteq_0 \ldots \trianglelefteq_0 p^s_1 \trianglelefteq_0 q^s_0 \trianglelefteq_0 p^s_0 \trianglelefteq_0 q^s_2 \trianglelefteq_0 \ldots \trianglelefteq_0 q^s_{2n} \trianglelefteq_0 y^m.\end{align*} $$

It is easy to verify that $\trianglelefteq _0$ and $\trianglelefteq _1$ realize $(P^{2n+2} \setminus C, \preceq )$ .

By $\mathsf {DBc_{n}}$ we know that $\dim (P^{2n+2}, \preceq ) \le 2n + 2$ and the set separating the ranges of f and g is defined as $A = \{m : |\{i < 2n+2 : y^m \trianglelefteq ^*_i x^m\}| =1 \}$ as in the proof of Theorem 2.11.

Proof. Theorem 4.4 shows one implication, so we deal with the converse.

We already proved the reversal for $n<4$ in Theorem 4.7 and Corollary 4.8. The proof we are about to give works for $n \ge 3$ . As usual let f and g be 1–1 functions with disjoint ranges. Let

$$ \begin{align*}P=\{x^i,y^i: i \in \mathbb{N}\} \cup \{c^r_j, d^r_j : j < n, r \in \mathbb{N}\} \cup \{p^s_j, q^s_j : j < n, s \in \mathbb{N}\}\end{align*} $$

and define $\ell : P \rightarrow \mathbb {N}$ as in Theorem 2.11. As before, we let $P_m$ be the level of elements z such that $\ell (z) = m$ .

For each $z_1, z_2 \in P$ we stipulate the following:

• • If neither $z_1$ nor $z_2$ is a $d^r_j$ or a $q^s_k$ , then $z_1 \prec z_2$ if and only if either $\ell (z_1) < \ell (z_2)$ or $z_1 = c^r_j$ and $z_2 = y^{f(r)}$ or $z_1 = p^r_j$ and $z_2 = x^{f(r)}$ (this case coincides with what we did in the previous proofs).

• • If $z_1 = d^r_j$ then $z_1 \prec z_2$ if and only if $z_2=d^k_j$ for some k such that $f(r) < f(k)$ or $z_2=q^s_j$ for some s such that $f(r) < g(s)$ (namely, $z_2$ is a $d^k_j$ or a $q^s_j$ for the same j of $z_1$ and belongs to some higher level). If $z_1 = q^s_j$ the definition is analogous.

• • If $z_2 = d^r_j$ then $z_1 \prec z_2$ if and only if $z_1$ is either $x^{f(r)}$ or $c^r_i$ for $i \ne j$ or $\ell (z_1) < f(r)$ and if $z_1$ is a $d^v_i$ or a $q^s_i$ then $i = j$ . If $z_2=q^s_j$ the definition is analogous, replacing $x^m$ with $y^m$ and $c^r_i$ with $p^s_i$ .

Each level $P_m$ is either an antichain of two elements or a copy of $F_{n+1}$ . The difference with the previous constructions lies in the comparabilities between different levels as shown in the figure below, where we are assuming that $f(r) = l$ and $g(s) = m$ . We highlight with a dashed line some of the comparabilities between $d^r_i$ ’s and $q^s_j$ ’s: notice that $d^r_0 \nprec p^s_0$ even though $\ell (d^r_0) < \ell (p^s_0)$ .

The verification that we defined a poset is tedious but straightforward.

For each $j < n$ consider the chain $C_j=\{d^r_j, q^s_j: r,s \in \mathbb {N}\}$ . By definition of $\preceq $ these chains are incomparable. Let $C= \bigcup _{j<n} C_j$ and consider the poset $(P \setminus C, \preceq )$ . If $m \in \operatorname {ran}(f)$ or $m \in \operatorname {ran}(g)$ then $P_m \setminus C$ has one of the following forms:

It is easy to check that $\dim (P \setminus C, {\preceq }) = 2$ . By $\mathsf {DBi_{n}}$ we have that $\dim (P, {\preceq }) \le n+2$ and we can fix a set $\{\trianglelefteq ^*_0, \ldots , \trianglelefteq ^*_{n+1}\}$ of $n+2$ linearizations which realizes $(P, {\preceq })$ . If $m \in \operatorname {ran}(f)$ , then it must be $| \{i < n+2 : y^m\trianglelefteq ^*_i x^m\} | \le 2$ and analogously, if $m \in \operatorname {ran}(g)$ , then it must be $| \{i < n+2 : y^m \trianglelefteq ^*_i x^m\} | \ge n$ . Since we are supposing $n \ge 3$ , the set of $m \in \mathbb {N}$ such that $| \{i < n : y^m \trianglelefteq ^*_i x^m\} | \le 2$ separates $\operatorname {ran}(f)$ and $\operatorname {ran}(g)$ .

Proof. Suppose first that there exists a separator element $b \in L$ . If $b \in F$ then let $B = \{x \in L : x \lhd b\}$ , otherwise let $B = \{x \in L : x \trianglelefteq b\}$ . Then B exists in $\mathsf {RCA}_0$ and has the desired properties.

If there are no separator elements, let $B = \{x \in L : \exists i \in I (x \trianglelefteq i) \}$ . By hypothesis $x \in B$ if and only if $\forall f \in F (x \lhd f)$ . Therefore, B can be defined by $\Delta ^0_1$ comprehension and again has the required properties.

Proof. For the forward direction, let $(P, \preceq )$ be a poset. Let $x_0 \in P$ and let $\{\trianglelefteq _0, \ldots , \trianglelefteq _{n-1}\}$ be a realization of $(P \setminus \{x_0\}, \preceq )$ .

Let $I=\{x: x \in P \wedge x \prec x_0\}$ and $F= \{x: x \in P \wedge x_0 \prec x \}$ which exist in $\mathsf {RCA}_0$ and are, respectively, downward and upward closed in P. Notice that by transitivity $I \prec F$ and since ${\prec } \subseteq {\lhd _i}$ we have $I \lhd _i F$ for each $i < n$ . Define two linearizations $\trianglelefteq _{n-1}^0,\trianglelefteq _{n-1}^1$ of $(P, \preceq )$ starting from $\trianglelefteq _{n-1}$ by

$$ \begin{align*}I \trianglelefteq_{n-1}^0 \{x_0\} \trianglelefteq_{n-1}^0 P \setminus (\{x_0\} \cup I)\end{align*} $$

$$ \begin{align*}P \setminus (\{x_0\} \cup F) \trianglelefteq_{n-1}^1 \{x_0\} \trianglelefteq_{n-1}^1 F,\end{align*} $$

where each segment is ordered by $\trianglelefteq _{n-1}$ . Notice that $\mathsf {RCA}_0$ proves the existence of each segment and (using $I, F,$ and $\trianglelefteq _{n-1}$ as parameters) of the linear orders $\trianglelefteq _{n-1}^0$ and $\trianglelefteq _{n-1}^1$ . It is clear that $\trianglelefteq _{n-1}^0$ and $\trianglelefteq _{n-1}^1$ are linearizations of $\preceq $ . Notice that if $y \trianglelefteq _{n-1} z$ then at least one of $y \trianglelefteq ^0_{n-1} z$ and $y \trianglelefteq ^1_{n-1} z$ holds.

Next we want to extend each $\trianglelefteq _i$ for $i < n-1$ to a linearization of $(P, \preceq )$ . To this end, we apply $\mathsf {LS}^*$ to the sequence $(\trianglelefteq _i, I, F)_{i < n-1}$ to obtain, for each $i < n-1$ , a separator set $B_i$ with respect to $\trianglelefteq _i$ . Then we define linearizations $\trianglelefteq _i^*$ of $(P, \preceq )$ each extending the corresponding $\trianglelefteq _i$ by

$$ \begin{align*}B_i \trianglelefteq_i^* \{x_0\} \trianglelefteq_i^* P \setminus (\{x_0\} \cup B_i),\end{align*} $$

where each segment is ordered by $\trianglelefteq _i$ .

Finally we claim that the set $\{\trianglelefteq _0^*, \ldots , \trianglelefteq _{n-1}^0, \trianglelefteq _{n-1}^1\}$ realizes $(P, \preceq )$ . We need to prove that if $z \npreceq y$ then either $y \trianglelefteq ^0_{n-1} z$ or $y \trianglelefteq ^1_{n-1} z$ or $y \trianglelefteq _i^* z$ for some $i < n-1$ . If $y = x_0$ then $z \notin I$ and $y \trianglelefteq ^0_{n-1} z$ , while if $z = x_0$ then $y \notin F$ and $y \trianglelefteq ^1_{n-1} z$ . If neither y nor z are $x_0$ we have $y \trianglelefteq _i z$ for some $i<n$ . If $i=n-1$ we already noticed that at least one of $y \trianglelefteq ^0_{n-1} z$ and $y \trianglelefteq ^1_{n-1} z$ holds. If $i<n-1$ then, since $z \in B_i$ and $y \notin B_i$ cannot hold, we have $y \trianglelefteq _i^* z$ .

For the converse direction let $(L_j, I_j, F_j)_{j < n}$ be a sequence of linear orders with sets to be separated. First we extend each $L_j$ in $\mathsf {RCA}_0$ so that $I_j$ , $F_j$ , and $L_j \setminus (I_j \cup F_j)$ are infinite. This can be achieved by adding infinitely many new elements below $L_j$ , stipulate that they belong to $I_j$ , and adding infinitely many new elements above $L_j$ and stipulate that infinitely and coinfinitely many of them belong to $F_j$ . We still denote the new sequence by $(L_j, I_j, F_j)_{j < n}$ and notice that it suffices to find a solution for it.

Next we identify all the elements of $I_j$ (resp. $F_j$ ) throughout all the linear orders $L_j$ as follows. We may assume that the support of each $L_j$ is $\mathbb {N}$ . Let $f_j \colon \mathbb {N} \to \mathbb {N} \setminus \{0\}$ be the bijection defined as

$$ \begin{align*}f_j(y) = \begin{cases} \text{the least unused } n \equiv 0 \mod 3 & \text{if } y \in I_j; \\ \text{the least unused } n \equiv 1 \mod 3 & \text{if } y \in F_j; \\ \text{the least unused } n \equiv 2 \mod 3 & \text{otherwise.} \end{cases}\end{align*} $$

We define the linear order $\lhd _j$ on $\mathbb {N} \setminus \{0\}$ as $n \lhd _j m$ if and only if $f_j^{-1} (n)$ is below $f_j^{-1} (m)$ in $L_j$ . Since $f_j$ is a computable isomorphism, the new linear orders (which we still denote by $L_j$ ) exists in $\mathsf {RCA}_0$ . Now for each j we have $I_j = \{n> 0 : n \equiv 0 \! \mod 3\}$ and $F_j = \{n : n \equiv 1 \! \mod 3\}$ . We simply call I and F those sets. Moreover, it suffices to find a solution for the sequence $(L_j, I, F)_{j < n}$ .

We define an additional linear order $L_n$ on $\mathbb {N} \setminus \{0\}$ : we stipulate $y \lhd _n z$ if and only if either $y \equiv z \! \mod 3$ and $y < z$ (in the standard ordering of $\mathbb {N}$ ), or $y \equiv 0 \! \mod 3$ and z is not, or $y \equiv 2 \! \mod 3$ and $z \equiv 1 \! \mod 3$ . In other words in $L_n$ the elements of I are followed by the elements of $\mathbb {N} \setminus (I \cup F)$ , which in turn are followed by the elements of F.

Let $\prec $ be the binary relation on $\mathbb {N}$ obtained by taking the intersection of the $L_j$ ’s for $j < n+1$ , and then adding $0$ so that $I \prec 0 \prec F$ and $0$ is incomparable with everything else. We claim that $P = (\mathbb {N}, \prec )$ is a poset. The only non trivial facts to prove is that if $z \prec y$ and $y \prec 0$ then $z \prec 0$ , and its dual if $0 \prec y$ and $y \prec z$ then $0 \prec z$ . In the first case, by definition $y \in I$ and by construction of $L_n$ it must be $z \in I$ too. So $z \prec 0$ by definition. The dual is proved in the same way, using F in place of I.

By definition of P the sequence $(L_j)_{j<n+1}$ realizes $P \setminus \{0\}$ . By the statement, let $(L^{\prime }_j, \lhd _j')_{j < n+2}$ be a realization of P such that for $j < n\, \lhd _j = \lhd _j' \restriction \mathbb {N} \setminus \{0\}$ . Then we uniformly separate $(L_j, I_j, F_j)_{j < n}$ by setting $B^{\prime }_j = \{x \in L^{\prime }_j : x \lhd _j' 0\} \subset L_j$ .

Proof. (1) implies (2) because the existence of X is an instance of bounded $\boldsymbol \Sigma ^{0}_{2}$ comprehension which is equivalent to $\mathsf {I} \boldsymbol \Sigma ^{0}_{2}$ (Theorem 2.7).

For the converse, we show that (2) implies bounded $\boldsymbol \Sigma ^{0}_{2}$ comprehension. Let $\varphi (j)$ be a $\boldsymbol \Sigma ^{0}_{2}$ formula of the form $\exists x \, \forall y \, \psi (j,x,y)$ . For each n, we need to prove that the set $\{j < n : \varphi (j)\}$ exists. We aim to construct a finite sequence of n linear orders $(L_j, \trianglelefteq _j)_{j < n}$ , each with subsets $I_j, F_j$ to be separated. We perform the construction to satisfy the following: for each $j < n$ , $\varphi (j)$ holds if and only if the linear order $(L_j, \trianglelefteq _j)$ has a separator element. Then it is clear that the set X of (2) is the set $\{j < n : \varphi (j) \}$ .

Fix $j < n$ . The linear order $(L_j, \trianglelefteq _j)$ has domain $\mathbb {N}$ , $I_j = \{m \in \mathbb {N} : m \equiv 0 \! \mod 3\}$ and $F_j = \{m \in \mathbb {N} : m \equiv 1 \! \mod 3\}$ . We stipulate that $\forall l \in I_j \, \forall m \in F_j \, (l \lhd _j m)$ , $\forall l,m \in I_j \, (l \lhd _j m \leftrightarrow l < m),$ and $\forall l,m \in F_j \, (l \lhd _j m \leftrightarrow m < l)$ (where $<$ denotes the standard ordering of $\mathbb {N}$ ). Since $I_j$ has no maximum and $F_j$ has no minimum, a separator element must belong to the set $Z_j = \{m \in \mathbb {N} : m \equiv 2 \! \mod 3\}$ . We also stipulate that $\forall l \in Z_j \, \forall m \in F_j \, (l \lhd _j m)$ and $\forall l,m \in Z_j \, (l \lhd _j m \leftrightarrow l < m)$

We design a strategy to define the comparabilities of the elements of $I_j$ and $Z_j$ in such a way to ensure that $\varphi (j)$ holds if and only if there is a separator element for $L_j, I_j, F_j$ . In other words, as long as x appears to witness $\varphi (j)$ , the strategy keeps $3x+2$ above all elements of $I_j$ . We proceed by stages: at stage s we stipulate (at least) the comparabilities between each element of $Z_j$ and $3s \in I_j$ . The strategy keeps parameters $x_j^s$ for all $j < n$ to mark the current possible existential witness for $\varphi (j)$ . We start by setting $x_j^0 = 0$ for all $j < n$ .

Stage s. For each $j < n$ if $\forall y \le s \, \psi (j,x_j^s,y)$ holds, then we stipulate that $\forall m \ge x_j \, (3s \lhd _j 3m + 2)$ and let $x_j^{s+1} = x_j^s$ . On the other hand, if $\exists y \le s \, \neg \psi (j,x_j^s,y)$ holds, then we stipulate that $\forall t \ge s \, (3x_j^s + 2 \lhd _j 3t)$ and $\forall m> x_j^s (3s \lhd _j 3m + 2)$ . In this second case, we let $x_j^{s+1} = x_j^s+1$ .

This completes the construction of the linear orders $(L_j, \trianglelefteq _j)_{j < n}$ .

We are left to prove that for $j < n$ , $\varphi (j)$ holds if and only if the linear order $(L_j, \trianglelefteq _j)$ has a separator element. For the forward direction, fix $j < n$ such that $\varphi (j)$ holds. Let $\overline {x}$ be such that $\forall y \, \psi (j,\overline {x},y)$ holds. By construction for each s we stipulated that $3s \lhd _j 3 \overline {x} +2$ . We conclude that $\overline {x}$ is a separator element for $L_j, I_j, F_j$ .

Conversely, suppose that for $j < n\, \neg \varphi (j)$ holds. Since $\forall x \, \exists y \, \neg \psi (j,x,y)$ holds, by $\mathsf {I} \boldsymbol \Sigma ^{0}_{1}$ we have that $\forall x \, \exists s \, (x = x^s_j)$ . Fix z large enough so that $\exists y \le z \, \neg \psi (j,x,y)$ and $\exists s \le z \, (x = x_j^s)$ . Then $3 x + 2 \lhd _j 3 z$ . Since x was arbitrary, there is no separator element for $L_j, I_j, F_j$ .

Proof. Let $(M,S) \vDash \mathsf {RCA}_0+\neg \mathsf {B} \boldsymbol \Sigma ^{0}_{2}$ . By the failure of $\mathsf {B} \boldsymbol \Sigma ^{0}_{2}$ there exists $k \in M$ and $f \in S$ with $f \colon M \rightarrow k$ such that for each $i < k$ , $f^{-1} (i)$ is finite. Let $X \in S$ be such that f is $\Delta _1(X)$ and let $(\Phi ^X_e)_{e \in M}$ be an enumeration of the X-computable functions of the model (regarded as $\{0,1\}$ -valued for convenience). We write $\Phi ^X_{e,s}$ to denote $\Phi ^X_e$ after s stages of the computation.

We construct by stages a $\Delta _1(X)$ -instance $Z = (L_j, I_j, F_j)_{j < k}$ of $\mathsf {LS}^*$ such that for each $e \in M$ , if $f(e) = j$ then $\Phi ^X_e$ is not a separator set for $L_j, I_j, F_j$ . The support of each $L_j$ is M. The construction keeps parameters $\delta ^s_e$ for $e,s \in M$ and $x^s_j$ for $j < k$ and $s \in M$ : here s highlights that we are talking about the value of the parameter at the beginning of stage s. Analogously, we denote by $L_j^s, I_j^s, F_j^s$ the finite approximations of $L_j, I_j, F_j$ at the beginning of stage s. We start by setting $\delta ^0_e = 0$ , $x^0_j = 0$ , $L_j^0 = \{x^0_j\},$ and $I_j^0 = F_j^0 = \emptyset $ . At each stage we add finitely many elements to $L_j$ , define the comparabilities involving the new elements, and decide which of them belong to $I_j$ or $F_j$ .

For each $e \in M$ we want to satisfy the requirement $\mathsf {R}_e$ consisting of the disjunction of the following clauses where $f(e) = j$ :

1. (1) $\Phi ^X_e(x,j) \uparrow $ for some $x \in M$ ;

2. (2) $\Phi ^X_e(x,j) \downarrow = 0$ for some $x \in I_j$ ;

3. (3) $\Phi ^X_e(x,j) \downarrow = 1$ for some $x \in F_j$ ;

4. (4) $\Phi ^X_e(x,j) \downarrow = 1$ and $\Phi ^X_e(y,j) \downarrow = 0$ for some $x,y \in L_j$ with $y \lhd _j x$ (here $\lhd _j$ denotes the order relation on $L_j$ ).

Notice that if $\mathsf {R}_e$ is satisfied, then $\Phi ^X_e$ is not the characteristic function of a separator set for $L_j,I_j,F_j$ . We set $\delta ^s_e = 1$ if at stage s we are sure that $\mathsf {R}_e$ is satisfied, no matter what happens at later stages.

Stage s. For every $j < k$ check if for some $e \in f^{-1}(j) \cap [0,s)$ , $\Phi ^X_{e,s} (x^s_j, j) \downarrow $ and $\delta ^s_e = 0$ . Let $z^s_j$ and $w^s_j$ be the least elements of M not in $L^s_j$ .

If no such e is found, set $x_j^{s+1} = x_j^s$ , $L_j^{s+1} = L_j^s \cup \{z^s_j, w^s_j\}$ , $I_j^{s+1} = I_j^s \cup \{z^s_j\}$ , $F_j^{s+1} = F_j^s \cup \{w^s_j\}$ and put $z^s_j$ below every element of $L^s_j$ and $w^s_j$ above every element of $L^s_j$ .

Otherwise let e be least such that $\Phi ^X_{e,s} (x^s_j, j) \downarrow $ and $\mathsf {R}_e$ is not yet satisfied. The existence of a minimal e is ensured by $\mathsf {I} \boldsymbol \Sigma ^{0}_{0}$ . We say that $\mathsf {R}_e$ acts at this stage and we set $\delta ^{s+1}_e=1$ .

If $\Phi ^X_{e,s} (x^s_j, j) \downarrow = 0$ , put $x_j^s \lhd _j z^s_j \lhd _j w^s_j$ . We also stipulate that $z^s_j$ and $w^s_j$ are below all the elements of $L^s_j$ that were above $x^s_j$ . Then we set $x^{s+1}_j = w^s_j$ , $L_j^{s+1} = L_j^s \cup \{z^s_j, w^s_j\}$ , $I_j^{s+1} = I_j^s \cup \{z^s_j\}$ , and $F_j^{s+1} = F_j^s$ .

If $\Phi ^X_{e,s} (x^s_j, j) \downarrow = 1$ , put $w_j^s \lhd _j z^s_j \lhd _j x^s_j$ . We also stipulate that $z^s_j$ and $w^s_j$ are above all the elements of $L^s_j$ that were below $x^s_j$ . Then we set $x^{s+1}_j = w^s_j$ , $L_j^{s+1} = L_j^s \cup \{z^s_j, w^s_j\}$ , $I_j^{s+1} = I_j^s$ , and $F_j^{s+1} = F_j^s \cup \{z^s_j\}$ .

When we finish all the $j < k$ , for each e such that $\delta _e^{s+1}$ is still undefined, we set $\delta _e^{s+1} = \delta ^s_e$ and we move to the next stage. This completes the construction.

We need to prove that each requirement $\mathsf {R}_e$ is satisfied. First notice that $\delta _e^{s+1} \neq \delta _e^s$ for at most one s (the only stage when $\mathsf {R}_e$ act): when such s exists we denote it by $s_e$ .

We claim that for each $j < k$ there exists a stage s and $x \in M$ such that for each stage $t> s$ , $x^t_j = x^s_j$ . Suppose that this is not the case and let j be such that for every stage s and every x, there is a stage $t> s$ with $x^t_j \ne x^s_j$ . Fix a generic s. Then by $\mathsf {I} \boldsymbol \Sigma ^{0}_{0}$ there exists a least stage $t> s$ such that $x^s_j \ne x^t_j$ and we call $t_s$ this stage. By minimality, $x^{t_s-1}_j = x^s_j$ and some requirement $\mathsf {R}_e$ for $e \in f^{-1}(j) \cap [0,t_s)$ has to act, otherwise $x^{t_s}_j = x^{t_s-1}_j$ . By construction, only one requirement acts and we call $e_s$ its index. Moreover, each requirement acts at most once during the construction (exactly when $\delta _e^{s+1}$ becomes $1$ ) and so for each $s' < s$ , $e_{s'} \ne e_s$ . It follows that the function $s \to e_s$ is an X computable injection from M to $f^{-1}(j)$ which contradicts the assumption that $f^{-1}(j)$ is finite and the claim is proved.

Now we show that each requirement $\mathsf {R}_e$ is satisfied. If $\Phi ^X_e$ does not converge on some input $(x, f(e))$ , we meet clause (1). So suppose that $\Phi ^X_e$ converges on all such inputs. To ease the notation, let $f(e) = j$ . By the claim, there exists a stage s such that for all $t \ge s$ , $x^s_j = x^t_j$ . Since $\Phi ^X_e (x^s_j,j) \downarrow $ , if $\delta ^s_e = 0$ then for some $t \ge s$ either $\mathsf {R}_e$ or some higher priority requirement must act at stage t. It follows that $x^{t+1}_j$ is updated to a new value, which contradicts the claim that it already stabilized at stage s. It follows that $\delta ^s_e = 1$ , which means that $\mathsf {R}_e$ already acted at a previous stage, say $u_e$ . This means that $\Phi ^X_{e,u_e}(x^{u_e}_j,j) \downarrow $ and e is the least, so it is the one to act. If $\Phi ^X_{e,u_e}(x^{u_e}_j,j) \downarrow = 0$ then we stipulated $x^{u_e}_j \lhd _j z^{u_e}_j$ and we put $z^{u_e}_j \in I_j$ . In this case, either $\Phi ^X_e(z^{u_e}_j,j) \downarrow = 0$ and meet clause (2), or $\Phi ^X_e(z^{u_e}_j,j) \downarrow = 1$ and we meet clause (4). The proof in the case $\Phi ^X_{e,u_e}(x^{u_e}_j,j) \downarrow = 1$ is analogous: if $\Phi ^X_e(z^{u_e}_j,j) \downarrow = 1$ we meet clause (3), while if $\Phi ^X_e(z^{u_e}_j,j) \downarrow = 0$ we meet clause (4).

We conclude that the X-computable instance $(L_j, I_j, F_j)_{j < k}$ of $\mathsf {LS}^*$ has no $\Delta _1(X)$ -solution, because for each index e, the X-computable function $\Phi ^X_e$ fails to be a separator set for $L_{f(e)}, I_{f(e)}, F_{f(e)}$ .

Proof. Let $(M,S) \vDash \mathsf {RCA}_0+\neg \mathsf {I} \boldsymbol \Sigma ^{0}_{2}$ . We may also assume $(M,S) \vDash \mathsf {B} \boldsymbol \Sigma ^{0}_{2}$ , otherwise Theorem 5.7 immediately yields the thesis. All these hypothesis imply, by [Reference Chong and Wong9, Subsection 2.2], that for some $X \in S$ there are a $\Sigma ^0_2(X)$ -definable proper cut $I \subset M$ bounded by some $k \in M$ and a $\Sigma ^0_2(X)$ -definable strictly increasing cofinal function $f \colon I \rightarrow M$ . Let $(f_s)_{s \in M}$ be a $\Delta ^0_1(X)$ -sequence of functions such that for each $s \in M$ the map $f_s \colon k \rightarrow M$ is non decreasing, for each $x < k$ the map $s \mapsto f_s(x)$ is non decreasing, and for $x \in I\, \lim _{s \rightarrow \infty } f_s(x) = f(x)$ .

Let $(\Phi ^X_e)_{e \in M}$ be an enumeration of the X-computable functions of the model (regarded as $\{0,1\}$ -valued for convenience). We write $\Phi ^X_{e,s}$ to denote $\Phi ^X_e$ after s stages of the computation.