2 Reverse mathematics background

We give a brief review of $\mathsf {RCA}_0$ , $\mathsf {WKL}_0$ , $\mathsf {ACA}_0$ , $\Pi ^1_1\text {-}\mathsf {CA}_0$ , Ramsey’s theorem for pairs, its combinatorial consequences, and the first-order schemes. For further details, we refer the reader to Simpson’s standard reference [Reference Simpson30] and to Hirschfeldt’s monograph [Reference Hirschfeldt15].

We work in the two-sorted language of second-order arithmetic $0$ , $1$ , $<$ , $+$ , $\times $ , $\in $ , where variables x, y, z, etc. typically range over the first sort, thought of as natural numbers, and variables X, Y, Z, etc. typically range over the second sort, thought of as sets of natural numbers. As usual, the symbol $\mathbb {N}$ denotes the first-order part of whatever structure is under consideration.

The axioms of the base system $\mathsf {RCA}_0$ (for recursive comprehension axiom) are as follows:

• • A first-order sentence expressing that $(\mathbb {N}; 0, 1, <, +, \times )$ forms a discretely ordered commutative semi-ring with identity.

• • The $\Sigma ^0_1$ induction scheme (denoted $\mathsf {I}\Sigma ^0_{1}$ ), which consists of the universal closures (by both first- and second-order quantifiers) of all formulas of the form

  $$ \begin{align*} \bigl(\varphi(0) \;\wedge\; \forall n \, (\varphi(n) \;\rightarrow\; \varphi(n+1))\bigr) \;\rightarrow\; \forall n \, \varphi(n), \end{align*} $$
  where $\varphi $ is $\Sigma ^0_1$ .

• • The $\Delta ^0_1$ comprehension scheme, which consists of the universal closures (by both first- and second-order quantifiers) of all formulas of the form

  $$ \begin{align*} \forall n \, \bigl(\varphi(n) \;\leftrightarrow\; \psi(n)\bigr) \;\rightarrow\; \exists X \, \forall n \, \bigl(n \in X \;\leftrightarrow\; \varphi(n)\bigr), \end{align*} $$
  where $\varphi $ is $\Sigma ^0_1$ , $\psi $ is $\Pi ^0_1$ , and X is not free in $\varphi $ .

The “ $0$ ” in “ $\mathsf {RCA}_0$ ” refers to the restriction of the induction scheme to $\Sigma ^0_1$ formulas. $\mathsf {RCA}_0$ suffices to implement the usual bijective encodings of pairs of numbers, finite sequences of numbers, finite sets of numbers, and so on. See [Reference Simpson30, Section II.2] for details on how this is done. For example, we may encode a function $f \colon \mathbb {N} \rightarrow \mathbb {N}$ by its graph $\{\langle m, n \rangle : f(m) = n\}$ . We may also encode the set $\mathbb {N}^{<\mathbb {N}}$ of all finite sequences of natural numbers and the set $2^{<\mathbb {N}}$ of all finite binary sequences. For $\sigma , \tau \in \mathbb {N}^{<\mathbb {N}}$ and $f \colon \mathbb {N} \rightarrow \mathbb {N}$ , let $|\sigma |$ denote the length of $\sigma $ ; let $\tau \preceq \sigma $ denote that $\tau $ is an initial segment of $\sigma $ : $|\tau | \leq |\sigma | \;\wedge \; \forall n < |\tau | \; (\tau (n) = \sigma (n))$ ; and let $\tau \preceq f$ denote that $\tau $ is an initial segment of f: $\forall n < |\tau | \; (\tau (n) = f(n))$ . For $\sigma , \tau \in \mathbb {N}^{<\mathbb {N}}$ , let $\sigma ^{\smallfrown } \tau $ denote the concatenation of $\sigma $ and $\tau $ . When $\tau = \langle n \rangle $ is a sequence of length $1$ , we usually write $\sigma ^{\smallfrown } n$ instead of $\sigma ^{\smallfrown } \langle n \rangle $ . For $f \colon \mathbb {N} \rightarrow \mathbb {N}$ , $\sigma \in \mathbb {N}^{<\mathbb {N}}$ , and $n \in \mathbb {N}$ , let $f {\restriction } n = \langle f(0), f(1), \dots , f(n-1) \rangle $ denote the initial segment of f of length n; and if $n \leq |\sigma |$ , let $\sigma {\restriction } n = \langle \sigma (0), \dots , \sigma (n-1) \rangle $ denote the initial segment of $\sigma $ of length n.

$\mathsf {RCA}_0$ also suffices to develop the basic theory of oracle Turing machines (see, for example, [Reference Simpson30, Section VII.1]). We view such machines as defining Turing functionals, and we write $\Phi (A)$ for the result of applying the functional $\Phi $ to the set A. We also write $\Phi (A)(n)$ for the value of $\Phi (A)$ on input n, if it is defined. We may relativize a Turing functional $\Phi $ to a set X, write $\Phi ^X$ to denote the relativized functional, and write $\Phi ^X(A)$ for $\Phi (X \oplus A)$ , where $X \oplus A = \{2n : n \in X\} \cup \{2n+1 : n \in A\}$ as usual. The $\Phi ^X(A)$ notation is intended to convey that X is fixed but A may vary. We may also iterate a sequence $\Phi _0, \dots , \Phi _{k-1}$ of Turing functionals. For a set A, we say that the iteration $\Phi _{k-1}(\Phi _{k-2}(\cdots \Phi _0(A)\cdots ))$ is total if $\Phi _i(\Phi _{i-1}(\cdots \Phi _0(A)\cdots ))(n)$ is defined for every $i < k$ and every n. This may be expressed by asserting that for every n, there is a sequence $\langle \sigma _0, \dots , \sigma _k \rangle $ of elements of $\mathbb {N}^{<\mathbb {N}}$ , each of length at least n, such that $\sigma _0 \preceq A$ and $\forall i < k\; \forall m < |\sigma _{i+1}|\; \bigl (\Phi _i(\sigma _i)(m) \text { halts within } |\sigma _i| \text { steps and } \sigma _{i+1}(m) = \Phi _i(\sigma _i)(m)\bigr )$ .

Define a tree to be a set $T \subseteq \mathbb {N}^{<\mathbb {N}}$ that is closed under initial segments: $\forall \sigma \, \forall \tau \, ((\sigma \in T \;\wedge \; \tau \preceq \sigma ) \;\rightarrow \; \tau \in T)$ . Say that an $f \colon \mathbb {N} \rightarrow \mathbb {N}$ is a infinite path through a tree T if every initial segment of f is in T: $\forall n \, (f {\restriction } n \in T)$ . A tree with no infinite path is called well-founded, and a tree with an infinite path is called ill-founded. Finally, a tree $T \subseteq \mathbb {N}^{<\mathbb {N}}$ is called finitely branching if for every $\sigma \in T$ there are only finitely many n with $\sigma ^{\smallfrown } n \in T$ . A tree $T \subseteq 2^{<\mathbb {N}}$ is necessarily finitely branching. All of these definitions can be made in $\mathsf {RCA}_0$ . The axioms of $\mathsf {WKL}_0$ (for weak König’s lemma) are those of $\mathsf {RCA}_0$ , plus the statement that every infinite tree $T \subseteq 2^{<\mathbb {N}}$ has an infinite path.

The axioms of $\mathsf {ACA}_0$ (for arithmetical comprehension axiom) are of those of $\mathsf {RCA}_0$ , plus the arithmetical comprehension scheme, which consists of the universal closures of all formulas of the form

$$ \begin{align*} \exists X \, \forall n \, \bigl(n \in X \;\leftrightarrow\; \varphi(n)\bigr), \end{align*} $$

where $\varphi $ is an arithmetical formula in which X is not free. To show that some statement $\varphi $ implies $\mathsf {ACA}_0$ over $\mathsf {RCA}_0$ , a common strategy is to use $\mathsf {RCA}_0 + \varphi $ to show that the ranges of injections exist as sets and appeal to the following well-known lemma.

Unlike its weak version, the full version of König’s lemma, which states that every infinite finitely branching tree $T \subseteq \mathbb {N}^{<\mathbb {N}}$ has an infinite path, is equivalent to $\mathsf {ACA}_0$ over $\mathsf {RCA}_0$ (see [Reference Simpson30, Theorem III.7.2]).

The axioms of $\Pi ^1_1\text {-}\mathsf {CA}_0$ (for $\Pi ^1_1$ comprehension axiom) are those of $\mathsf {RCA}_0$ , plus the $\Pi ^1_1$ comprehension scheme, which consists of the universal closures of all formulas of the form

$$ \begin{align*} \exists X \, \forall n \, \bigl(n \in X \;\leftrightarrow\; \varphi(n)\bigr), \end{align*} $$

where $\varphi $ is a $\Pi ^1_1$ formula in which X is not free. To show that some statement $\varphi $ implies $\Pi ^1_1\text {-}\mathsf {CA}_0$ over $\mathsf {RCA}_0$ , a useful tool is to use $\mathsf {RCA}_0 + \varphi $ to show that every ill-founded tree has a leftmost path. For functions $f,g \colon \mathbb {N} \rightarrow \mathbb {N}$ , say that g is to the left of f if $\exists n \, \bigl (g(n) < f(n) \;\wedge \; \forall i < n \; (g(i) = f(i))\bigr )$ . The leftmost path principle ( $\mathsf {LPP}$ ) states that for every ill-founded tree $T \subseteq \mathbb {N}^{<\mathbb {N}}$ , there is an infinite path f through T such that no infinite path through T is to the left of f.

A huge amount of research in reverse mathematics is devoted to understanding the strength of Ramsey’s theorem for pairs and its consequences. For a set $X \subseteq \mathbb {N}$ , let $[X]^2$ denote the set of two-element subsets of X, which may be encoded as $[X]^2 = \{\langle x, y \rangle : x, y \in X \;\wedge \; x < y\}$ . A function $c \colon [\mathbb {N}]^2 \rightarrow k$ is called a k-coloring of pairs, and an infinite set $H \subseteq \mathbb {N}$ is called homogeneous for a k-coloring of pairs c if c is constant on $[H]^2$ . Furthermore, a k-coloring of pairs c is called stable if $\lim _s c(n,s)$ exists for every n. Ramsey’s theorem for pairs and k colors ( $\mathsf {RT}^2_k$ ) states that for every k-coloring of pairs c, there is a set that is homogeneous for c. Stable Ramsey’s theorem for pairs and k colors ( $\mathsf {SRT}^2_k$ ) is the restriction of $\mathsf {RT}^2_k$ to stable k-colorings of pairs c. $\mathsf {RT}^2_{<\infty }$ abbreviates $\forall k \, \mathsf {RT}^2_k$ and $\mathsf {SRT}^2_{<\infty }$ abbreviates $\forall k \, \mathsf {SRT}^2_k$ . Likewise, a function $c \colon \mathbb {N} \rightarrow k$ is called a k-coloring of singletons, and an infinite $H \subseteq \mathbb {N}$ is called homogeneous for a k-coloring of singletons c if c is constant on H. Ramsey’s theorem for singletons and k colors ( $\mathsf {RT}^1_k$ ) states that for every k-coloring of singletons c, there is a set that is homogeneous for c. $\mathsf {RT}^1_{<\infty }$ abbreviates $\forall k \, \mathsf {RT}^1_k$ , which we think of as expressing the infinite pigeonhole principle. $\mathsf {RCA}_0$ proves $\mathsf {RT}^1_k$ for each fixed standard k, but it does not prove $\mathsf {RT}^1_{<\infty }$ .

Of the many combinatorial consequences of $\mathsf {RT}^2_2$ , we are primarily concerned with the ascending/descending sequence principle ( $\mathsf {ADS}$ ), stating that every countably infinite linear order has either an infinite ascending sequence or an infinite descending sequence, as well as its stable version $\mathsf {SADS}$ . To be precise, let $(L, <_L)$ be a linear order. A set $S \subseteq L$ is an ascending sequence if $\forall x, y \in S \; (x < y \rightarrow x <_L y)$ , and it is a descending sequence if $\forall x, y \in S \; (x < y \rightarrow y <_L x)$ . The principle $\mathsf {ADS}$ then states that for every infinite linear order $(L, <_L)$ , there is an infinite $S \subseteq L$ that is either an ascending sequence or a descending sequence. Often it is more convenient to phrase $\mathsf {ADS}$ by stating that for every infinite linear order $(L, <_L)$ , there is an infinite sequence $\langle x_n : n \in \mathbb {N} \rangle $ of elements of L such that either $x_0 <_L x_1 <_L x_2 <_L \cdots $ or $x_0>_L x_1 >_L x_2 >_L \cdots $ . $\mathsf {RCA}_0$ proves that the two phrasings of $\mathsf {ADS}$ are equivalent because it proves that any sequence $x_0, x_1, x_2, \dots $ of distinct elements of $\mathbb {N}$ can be thinned to an $<$ -increasing subsequence $x_{i_0} < x_{i_1} < x_{i_2} < \cdots $ where the set $\{x_{i_n} : n \in \mathbb {N}\}$ exists. Call a linear order $(L, <_L)$ stable if every element either has only finitely many predecessors or has only finitely many successors. $\mathsf {SADS}$ is the restriction of $\mathsf {ADS}$ to infinite stable linear orders. Closely related to $\mathsf {ADS}$ is the chain/antichain principle ( $\mathsf {CAC}$ ), which states that every infinite partial order has either an infinite chain or an infinite antichain. Figure 1 summarizes the relationships among several of the systems and principles mentioned thus far.

Figure 1 Selected principles and systems and their implications and non-implications over $\mathsf {RCA}_0$ . An arrow indicates that the source principle/system implies the target principle/system over $\mathsf {RCA}_0$ . No further arrows may be added, except those that may be inferred via transitivity. No arrows reverse. Proofs of these implications and separations may be found in [Reference Chong, Lempp and Yang6, Reference Chong, Slaman and Yang8, Reference Hirschfeldt and Shore16, Reference Hirst17, Reference Lerman, Solomon and Towsner21, Reference Liu22, Reference Patey26, Reference Seetapun and Slaman29, Reference Simpson30].

Finally, we recall the induction schemes and their cousins, to which we collectively refer as the first-order schemes.

• • The induction axiom for $\varphi $ is the universal closure of the formula

  $$ \begin{align*} \bigl(\varphi(0) \;\wedge\; \forall n \, (\varphi(n) \;\rightarrow\; \varphi(n+1))\bigr) \;\rightarrow\; \forall n \, \varphi(n). \end{align*} $$

• • The least element principle for $\varphi $ is the universal closure of the formula

  $$ \begin{align*} \exists n \, \varphi(n) \;\rightarrow\; \exists n \, \bigl(\varphi(n) \;\wedge\; \forall m < n \; \neg\varphi(m)\bigr). \end{align*} $$

• • The bounded comprehension axiom for $\varphi $ is the universal closure of the formula

  $$ \begin{align*} \forall b \, \exists X \, \forall n \, \bigl(n \in X \;\leftrightarrow\; (n < b \;\wedge\; \varphi(n))\bigr), \end{align*} $$
  where X is not free in $\varphi $ .

• • The bounding (or collection) axiom for $\varphi $ is the universal closure of the formula

  $$ \begin{align*} \forall a\, \bigl(\forall n < a \; \exists m \; \varphi(n,m) \;\rightarrow\; \exists b \; \forall n < a \; \exists m < b \; \varphi(n,m)\bigr), \end{align*} $$
  where a and b are not free in $\varphi $ .

For a class of formulas $\Gamma $ , the $\Gamma $ induction scheme ( $\mathsf {I}\Gamma $ ) consists of the induction axioms for all $\varphi \in \Gamma $ , the $\Gamma $ least element principle consists of the least element principles for all $\varphi \in \Gamma $ , the bounded $\Gamma $ comprehension scheme consists of the bounded comprehension axioms for all $\varphi \in \Gamma $ , and the $\Gamma $ bounding scheme ( $\mathsf {B}\Gamma $ ) consists of the bounding axioms for all $\varphi \in \Gamma $ . For example, $\mathsf {B}\Sigma ^0_{2}$ consists of the bounding axioms for all $\Sigma ^0_2$ formulas. Beyond $\mathsf {RCA}_0$ , we are mostly interested in $\mathsf {B}\Sigma ^0_{2}$ and $\mathsf {I}\Sigma ^0_{2}$ . The following list summarizes the relationships between the systems and principles of Figure 1 and the first-order schemes.

• • $\mathsf {ACA}_0$ proves the induction axiom, least element principle, bounded comprehension axiom, and bounding axiom for every arithmetical formula.

• • In addition to $\mathsf {I}\Sigma ^0_{1}$ , $\mathsf {RCA}_0$ proves $\mathsf {I}\Pi ^0_{1}$ , the $\Sigma ^0_1$ least element principle, the $\Pi ^0_1$ least element principle, the bounded $\Sigma ^0_1$ comprehension scheme, the bounded $\Pi ^0_1$ comprehension scheme, and $\mathsf {B}\Sigma ^0_{1}$ (see [Reference Hájek and Pudlák14, Section I.2] and [Reference Simpson30], Section II.3).

• • Neither $\mathsf {RCA}_0$ nor $\mathsf {WKL}_0$ proves $\mathsf {B}\Sigma ^0_{2}$ (see [Reference Simpson30, Sections IX.1 and IX.2]).

• • $\mathsf {RCA}_0$ proves that $\mathsf {B}\Pi ^0_{1}$ , $\mathsf {B}\Sigma ^0_{2}$ , and $\mathsf {RT}^1_{<\infty }$ are equivalent; that $\mathsf {I}\Sigma ^0_{2}$ , $\mathsf {I}\Pi ^0_{2}$ , the $\Sigma ^0_2$ least element principle, the $\Pi ^0_2$ least element principle, the bounded $\Sigma ^0_2$ comprehension scheme, and the bounded $\Pi ^0_2$ comprehension scheme are all equivalent; and that $\mathsf {I}\Sigma ^0_{2}$ implies $\mathsf {B}\Sigma ^0_{2}$ (see [Reference Hájek and Pudlák14, Section I.2], [Reference Hirst17], and [Reference Simpson30, Section II.3]).

• • $\mathsf {SADS}$ and all the systems and principles above it in Figure 1 imply $\mathsf {B}\Sigma ^0_{2}$ over $\mathsf {RCA}_0$ .

• • $\mathsf {RCA}_0 + \mathsf {RT}^2_2$ does not prove $\mathsf {I}\Sigma ^0_{2}$ [Reference Chong, Slaman and Yang9].

We emphasize that $\mathsf {B}\Sigma ^0_{2}$ and $\mathsf {RT}^1_{<\infty }$ are equivalent over $\mathsf {RCA}_0$ because we use this equivalence often and without special mention.

3 From one principle to many

We begin studying the Rival–Sands theorem for partial orders from the perspective of reverse mathematics. Typically we use $\omega $ to denote the order-type of $(\mathbb {N}, <)$ , use $\omega ^*$ to denote the order-type of its reverse, and use $\zeta $ to denote the order-type $\omega ^* + \omega $ of the integers. In some places we may write $<_{\mathbb {N}}$ , $\leq _{\mathbb {N}}$ , etc. instead of $<$ , $\leq $ , etc. to help disambiguate several orders under discussion.

We use the homogeneous terminology from Ramsey’s theorem to describe chains that are as in the conclusion to the Rival–Sands theorem for partial orders.

Every infinite subset of a $(0,\mathrm {cof})$ -homogeneous chain in a partial order is also $(0,\mathrm {cof})$ -homogeneous, but an infinite subset of a $(0,\infty )$ -homogeneous chain need not be $(0,\infty )$ -homogeneous. Rival and Sands observed that if C is a chain of order-type $\zeta $ in a partial order $(P, <_P)$ , then C is automatically $(0,\infty )$ -homogeneous for P. To wit, if $p \in P$ is comparable with some $q \in C$ , then either $p \leq _P q$ and hence p is below infinitely many elements of C, or $p \geq _P q$ and hence p is above infinitely many elements of C. Similarly, if C is a $(0,\infty )$ -homogeneous chain of order-type either $\omega $ or $\omega ^*$ , then C is automatically $(0,\mathrm {cof})$ -homogeneous. For example, if C has order-type $\omega $ and $p \in P$ is comparable with infinitely many elements of C, then either p is above all elements of C, or p is below some element of C and therefore below cofinitely many elements of C.

We also apply the $(0,\infty )$ -homogeneous and $(0,\mathrm {cof})$ -homogeneous terminology to sequences. An infinite sequence $\langle x_n : n \in \mathbb {N} \rangle $ of distinct elements in a partial order $(P, <_P)$ is $(0,\infty )$ -homogeneous if every $p \in P$ is either comparable with $x_n$ for no n or is comparable with $x_n$ for infinitely many n; and it is $(0,\mathrm {cof})$ -homogeneous if every $p \in P$ is either comparable with $x_n$ for no n or is comparable with $x_n$ for cofinitely many n. As with chains of order-type $\omega $ and $\omega ^*$ , an infinite sequence that is $(0,\infty )$ -homogeneous and either ascending or descending is automatically $(0,\mathrm {cof})$ -homogeneous, and therefore all of its infinite subsequences are $(0,\mathrm {cof})$ -homogeneous as well.

We introduce several formulations of the Rival–Sands theorem for partial orders.

Immediately, $\mathsf {RCA}_0 \vdash \forall k\, \bigl ((0,\mathrm {cof})\text {-}\mathsf {RSpo}_k \rightarrow \mathsf {RSpo}_k\bigr )$ and therefore $\mathsf {RCA}_0 \vdash (0,\mathrm {cof})\text {-}\mathsf {RSpo}_{<\infty } \rightarrow \mathsf {RSpo}_{<\infty }$ . Also, Proposition 6.5 shows that for every $k \geq 2$ , $(0,\mathrm {cof})\text {-}\mathsf {RSpo}_k$ is equivalent to the statement “Every infinite partial order of width $\leq \! k$ has a $(0,\infty )$ -homogeneous chain of order-type either $\omega $ or $\omega ^*$ .”

When working with partial orders of finite width, it often helps to decompose the partial order into a finite union of chains.

We emphasize that if a partial order P is assumed to be k-chain decomposable, then P comes along with a k-chain decomposition. Of course, we may always assume that the chains of a chain decomposition are pairwise disjoint.

Recall now Dilworth’s theorem, which in this terminology states that for every k, every partial order of width $\leq \! k$ is k-chain decomposable. Hirst [Reference Hirst17] shows that Dilworth’s theorem for countable partial orders is equivalent to $\mathsf {WKL}_0$ over $\mathsf {RCA}_0$ . He also shows that Dilworth’s theorem remains equivalent to $\mathsf {WKL}_0$ even when restricted to partial orders of width $2$ . It follows that there is a recursive partial order of width $2$ that cannot be decomposed into $2$ recursive chains. Thus Dilworth’s theorem is not available when working in $\mathsf {RCA}_0 + \mathsf {I}\Sigma ^0_{2} + \mathsf {ADS}$ because $\mathsf {RCA}_0 + \mathsf {I}\Sigma ^0_{2} + \mathsf {ADS} \nvdash \mathsf {WKL}_0$ . However, for our purposes it is not necessary to decompose a partial order of finite width into the optimal number of chains—any decomposition into finitely many chains will do. Thus we replace Dilworth’s theorem by Kierstead’s effective analog, which states that every recursive partial order of width $\leq \! k$ can be decomposed into at most $(5^k - 1)/4$ recursive chains [Reference Kierstead18]. Nowadays much better sub-exponential bounds are known for the number of recursive chains into which a recursive partial order of finite width can be decomposed [Reference Bosek and Krawczyk3].

Let $(P, <_P)$ be a partial order of width $\leq \! k$ . Kierstead’s proof is phrased as an induction on k. By unwinding the induction, the proof can be viewed as an on-line algorithm computing a sequence of partial orders $(P, <_P) = (P_0, <_{P_0}), (P_1, <_{P_1}), \dots , (P_{k-2}, <_{P_{k-2}})$ , where $P_i$ has width $\leq \! k-i$ for each $i \leq k-2$ , together with a $(5^{k-i} - 1)/4$ -chain decomposition of $(P_i, <_{P_i})$ for each $i \leq k-2$ . Kierstead himself comments along these lines following the proof of [Reference Kierstead18, Theorem 1.10]. With this view, it is possible to verify that Kierstead’s theorem is provable in $\mathsf {RCA}_0$ .

For notational ease, we work with $5^k$ -chain decompositions in place of $(5^k - 1)/4$ -chain decompositions. Again, for our purposes, any primitive recursive bound suffices.

For completeness, we mention that there is a dual version of Dilworth’s theorem, due to Mirsky, which states that every partial order of height $\leq \! k$ can be decomposed into a union of k antichains. Hirst proved that Mirsky’s theorem for countable partial orders is equivalent to $\mathsf {WKL}_0$ over $\mathsf {RCA}_0$ [Reference Hirst17]. There is also an effective analog of Mirsky’s theorem in the spirit of Theorem 3.5 [Reference Kierstead19].

We now formalize versions of $\mathsf {RSpo}$ with the assumption “width $\leq \! k$ ” replaced by “k-chain decomposable.”

We have that $\mathsf {RCA}_0 \vdash \forall k \, \bigl ((\mathsf {RSpo}^{\mathsf {CD}}_{5^k} \rightarrow \mathsf {RSpo}_k) \;\wedge \; (\mathsf {RSpo}_k \rightarrow \mathsf {RSpo}^{\mathsf {CD}}_k)\bigr )$ and analogously for the $(0,\mathrm {cof})$ -homogeneous versions by Theorem 3.5 and the fact that k-chain decomposable partial orders have width $\leq \! k$ . It follows that $\mathsf {RCA}_0 \vdash \mathsf {RSpo}_{<\infty } \leftrightarrow \mathsf {RSpo}^{\mathsf {CD}}_{<\infty }$ and that $\mathsf {RCA}_0 \vdash (0,\mathrm {cof})\text {-}\mathsf {RSpo}_{<\infty } \leftrightarrow (0,\mathrm {cof})\text {-}\mathsf {RSpo}^{\mathsf {CD}}_{<\infty }$ . Additionally, $\mathsf {WKL}_0 \vdash \forall k \, (\mathsf {RSpo}_k \leftrightarrow \mathsf {RSpo}^{\mathsf {CD}}_k)$ and analogously for the $(0,\mathrm {cof})$ -homogeneous versions because $\mathsf {WKL}_0$ proves Dilworth’s theorem.

We conclude this section with a few other useful applications of Theorem 3.5. If $(P, <_P)$ is an infinite partial order of width $\leq \! k$ , then $\mathsf {CAC}$ implies that P contains an infinite chain because P does not contain an infinite antichain. However, we may argue more effectively by instead applying Theorem 3.5 to P to obtain a $5^k$ -chain decomposition of P and then by applying the pigeonhole principle to conclude that one of these chains must be infinite. Dually, $\mathsf {CAC}$ implies that an infinite partial order of height $\leq \! k$ contains an infinite antichain, and this fact can be effectivized as well. We show that these special cases of $\mathsf {CAC}$ are provable in $\mathsf {RCA}_0$ for each fixed k and are equivalent to $\mathsf {B}\Sigma ^0_{2}$ over $\mathsf {RCA}_0$ for arbitrary k.

We now show that $\mathsf {ADS}$ is equivalent to the statement “Every infinite partial order of finite width contains either an infinite ascending sequence or an infinite descending sequence.”

4 First proofs of $\mathsf {RSpo}_{<\infty }$ and $(0,\mathrm {cof})\text {-}\mathsf {RSpo}_{<\infty }$

We give a proof of $\mathsf {RSpo}_{<\infty }$ in $\mathsf {ACA}_0$ and a proof of $(0,\mathrm {cof})\text {-}\mathsf {RSpo}_{<\infty }$ in $\Pi ^1_1\text {-}\mathsf {CA}_0$ . The proofs are not axiomatically optimal, but they can be presented in ordinary mathematical language—meaning without reference to relative computability, technical uses of restricted induction, etc.—and are straightforward to formalize. The $\mathsf {ACA}_0$ proof in particular strikes a good balance between axiomatic simplicity and conceptual simplicity. It is based on Dilworth’s theorem, the fact that chains of order-type $\zeta $ are automatically $(0,\infty )$ -homogeneous, and the observation that a linear order containing no suborder of type $\zeta $ can be partitioned into a well-founded part and a reverse well-founded part. This last observation requires the full strength of $\mathsf {ACA}_0$ , as shown by Lemma 4.5. This section also serves to introduce key concepts that will be refined in the next section to prove $\mathsf {RSpo}_{<\infty }$ in $\mathsf {RCA}_0 + \mathsf {I}\Sigma ^0_{2} + \mathsf {ADS}$ .

We also extend the notation of Definition 4.1 to sequences. For example, if ${A = \langle a_n : n \in \mathbb {N} \rangle }$ and $B = \langle b_n : n \in \mathbb {N} \rangle $ are sequences in a partial order $(P, <_P)$ , then we write $A \leq _{\forall \exists } B$ if $\forall n \, \exists m \, (a_n \leq _P b_m)$ .

For a partial order $(P, <_P)$ and non-empty subsets $X, Y, Z \subseteq P$ , $\mathsf {RCA}_0$ suffices to show that $X <_P Y <_P Z$ implies $X <_P Z$ and that $X \leq _{\forall \exists } Y \leq _{\forall \exists } Z$ implies ${X \leq _{\forall \exists } Z}$ . Also, notice that $X \leq _{\forall \exists } Y$ simply means that $X \subseteq Y{\downarrow }$ , but beware that forming the set $Y{\downarrow }$ requires $\mathsf {ACA}_0$ in general.

As mentioned above, we show that partitioning a linear order with no suborder of type $\zeta $ into a well-founded part and a reverse well-founded part is equivalent to $\mathsf {ACA}_0$ over $\mathsf {RCA}_0$ . More generally, we show that isolating the well-founded part of a partial order that contains no infinite antichain and no suborder of type $\zeta $ is equivalent to $\mathsf {ACA}_0$ over $\mathsf {RCA}_0$ . Finding the well-founded part of such a partial order is used to extend $\mathsf {RSpo}_{<\infty }$ to infinite partial orders without infinite antichains in Section 7. The reversal exploits the tool of true and false numbers of an injection $f \colon \mathbb {N} \rightarrow \mathbb {N}$ .

The idea of true numbers appears to have originated with Dekker [Reference Dekker10], who called them minimal. True numbers are important because the range of f is recursive in the join of f with any infinite set of true numbers. In fact, if n is a true number, then one can determine $\operatorname {{\mathrm {ran}}}(f)$ up to $f(n)$ by simply evaluating f on inputs $0, \dots , n$ . In reverse mathematics, true numbers facilitate reversals to $\mathsf {ACA}_0$ . To prove that some statement $\varphi $ implies $\mathsf {ACA}_0$ over $\mathsf {RCA}_0$ , one strategy is to let $f \colon \mathbb {N} \to \mathbb {N}$ be an injection, use $\varphi $ to produce an infinite set S of true numbers, use f and S to compute $\operatorname {{\mathrm {ran}}}(f)$ , and then apply Lemma 2.1. For example, this strategy is used in [Reference Frittaion, Hendtlass, Marcone, Shafer and Van der Meeren12, Reference Frittaion and Marcone13, Reference Marcone and Shore25] in the form of the following well-known construction.

Given an injection $f \colon \mathbb {N} \rightarrow \mathbb {N}$ , Construction 4.4 produces a stable linear order either of type $\omega + \omega ^*$ (if f has infinitely many false numbers) or of type $k + \omega ^*$ for some finite k (otherwise). $\mathsf {RCA}_0$ proves that n is true if and only if n is in the $\omega ^*$ -part of L. Therefore, $\mathsf {RCA}_0$ proves that if there is an infinite subset of the $\omega ^*$ -part of L, or, equivalently, if there is an infinite descending sequence in L, then the range of f exists. For further details, see the proofs of [Reference Marcone and Shore25, Lemma 4.2] and [Reference Frittaion and Marcone13, Theorem 4.5].

Proof For (1) $\Rightarrow $ (2), let $(P, <_P)$ be a partial order with no infinite antichain and no suborder of type $\zeta $ . For the purposes of this proof, call a descending sequence $p_0>_P p_1 >_P \cdots >_P p_n$ in P discrete if for all $i < n$ there is no element of P strictly between $p_i$ and $p_{i+1}$ . Define a sequence of trees $\langle T_p : p \in P \rangle $ , where for each $p \in P$ , $T_p$ consists of the finite discrete descending sequences starting at p. That is, for each $p \in P$ , $T_p$ consists of the $\sigma \in P^{<\mathbb {N}}$ such that

$$ \begin{align*} (|\sigma| &> 0 \;\rightarrow\; \sigma(0) = p)\\ &\wedge \quad \forall i < |\sigma|-1 \; \Bigl(\sigma(i+1) <_P \sigma(i) \;\wedge\; \neg \exists x \in P \; \bigl(\sigma(i+1) <_P x <_P \sigma(i)\bigr)\Bigr). \end{align*} $$

Let $W = \{p \in P : T_p \text { is finite}\}$ . We show that $p \in W$ if and only if $p{\downarrow }$ is well-founded.

First, consider a $p \in P$ where $T_p$ is infinite. Given any $\sigma \in T_p$ , the set $\{q \in P : \sigma ^{\smallfrown } q \in T_p\}$ is an antichain on account of the discreteness condition on the elements of $T_p$ and therefore is finite because P has no infinite antichain. Thus T is an infinite finitely branching tree, and therefore T has an infinite path f by König’s lemma. This path provides an infinite descending sequence in P below p, so $p{\downarrow }$ is ill-founded.

Conversely, consider a $p \in P$ where $T_p$ is finite. Suppose for a contradiction that $p{\downarrow }$ is ill-founded, and let $p = q_0>_P q_1 >_P q_2 >_P \cdots $ be an infinite descending sequence below P. Notice that $\sigma = \langle p \rangle $ is in $T_p$ and satisfies $\sigma (0)>_P q_1$ . Let ${\sigma \in T_p}$ be a non-empty sequence of maximum length for which there is an n such that ${\sigma (|\sigma |-1)>_P q_n}$ . Such a $\sigma $ exists because $T_p$ is finite. Now define an infinite ascending sequence $A = \langle a_i : i \in \mathbb {N} \rangle $ with $\sigma (|\sigma |-1)>_P a_i \geq _P q_n$ for all i as follows. Let $a_0 = q_n$ . Given $a_i$ , let $a_{i+1}$ be the $<$ -least element of P with $\sigma (|\sigma |-1)>_P a_{i+1} >_P a_i$ . Such an $a_{i+1}$ exists because otherwise we would have $\sigma ^{\smallfrown } a_i \in T_p$ and $a_i>_P q_{n+1}$ , which contradicts that $\sigma $ has maximum length. We now have that $\{a_i : i \in \mathbb {N}\} \cup \{q_i : i> n\}$ is a chain in P of order-type $\zeta $ , which is a contradiction. Thus $p{\downarrow }$ is well-founded, as desired.

For (2) $\Rightarrow $ (3), let $(L, <_L)$ be a linear order with no suborder of type $\zeta $ . Then L has no infinite antichain, so by item (2) there is a set W containing exactly the $p \in P$ for which $p{\downarrow }$ is well-founded. Clearly W is downward-closed. Let $R = L \setminus W$ . Then $L = W \cup R$ and $W <_L R$ . We show that R is reverse well-founded. First, observe that R has no least element. If r were the least element of R, then $r{\downarrow }$ would be well-founded because every $p <_L r$ would be in W and W is well-founded. This would imply that $r \in W$ , which is a contradiction. Thus either $R = \emptyset $ , in which case R is reverse well-founded, or R is non-empty and has no minimum element, in which case we can define an infinite descending sequence $\langle d_n : n \in \mathbb {N} \rangle $ that is coinitial in R. If R also has an infinite ascending sequence $B = \langle b_n : n \in \mathbb {N} \rangle $ , then $b_0>_L d_{n_0}$ for some $n_0$ , in which case $\{d_n : n> n_0\} \cup B$ is a contradictory suborder of L of type $\zeta $ . Thus R is reverse well-founded.

For (3) $\Rightarrow $ (1), let $f \colon \mathbb {N} \to \mathbb {N}$ be an injection. We show that the true numbers for f form a set. This implies that the range of f exists as a set, which implies $\mathsf {ACA}_0$ by Lemma 2.1.

If f has only finitely many false numbers, then the set of all false numbers exists by bounded $\Sigma ^0_1$ comprehension, in which case the set of true numbers also exists.

Suppose instead that f has infinitely many false numbers. Let $(L, <_L)$ be the linear order defined as in Construction 4.4 for f. Recall that in this case $L = \{\ell _n : n \in \mathbb {N}\}$ is a linear order of type $\omega + \omega ^*$ , where, for each n, $\ell _n$ is in the $\omega $ -part if n is false and $\ell _n$ is in the $\omega ^*$ -part if n is true. We define a new linear order $(S, <_S)$ from L by replacing each element in the $\omega ^*$ -part of L by an infinite descending sequence and by replacing each element in the $\omega $ -part of L by a finite descending sequence. This way, $\mathsf {RCA}_0$ suffices to verify that elements in the $\omega ^*$ -part of L give rise to elements in the ill-founded part of S and that elements in the $\omega $ -part of L give rise to elements in the well-founded part of S. To do this, let $S = \{s_{n,m} : n, m \in \mathbb {N} \text { and } n \text { is true at stage } m\}$ (note that if $m \leq n$ , then n is true at stage m), and define

$$ \begin{align*} s_{n_0, m_0} <_S s_{n_1, m_1} \quad\Leftrightarrow\quad (\ell_{n_0} <_L \ell_{n_1}) \;\vee\; (\ell_{n_0} = \ell_{n_1} \;\wedge\; m_0>_{\mathbb{N}} m_1). \end{align*} $$

Observe that if $n_0$ is false and $n_1$ is true, then $\ell _{n_0} <_L \ell _{n_1}$ , so $s_{n_0, m_0} <_S s_{n_1, m_1}$ for every $m_0$ and $m_1$ . Thus no infinite ascending sequence in S can contain an element $s_{n,m}$ where n is true, and no infinite descending sequence in S can contain an element $s_{n,m}$ where n is false. It follows that S cannot contain a suborder of type $\zeta $ because such a suborder would have to contain some element $s_{n,m}$ , and $s_{n,m}$ is either in no infinite ascending sequence or in no infinite descending sequence. We may therefore apply item (3) to S and obtain a partition $S = W \cup R$ where $W <_L R$ , W is well-founded, and R is reverse well-founded. We claim that $s_{n, 0} \in R$ if and only if n is true. If n is true, then $s_{n,m} \in S$ for every m, and $s_{n,0}>_S s_{n,1} >_S \cdots $ is an infinite descending sequence in S. Thus $s_{n,0}$ cannot be in W as then W would be ill-founded. So $s_{n,0} \in R$ . Conversely, if n is false, then, using the assumption that there are infinitely many false numbers, we can define an infinite ascending sequence $\ell _n = \ell _{k_0} <_L \ell _{k_1} <_L \cdots $ in L as follows. Set $k_0 = n$ . Given $k_i$ , search for the first pair $\langle k, m \rangle $ where $\ell _{k_i} <_L \ell _k$ and k is false at stage m, and set $k_{i+1} = k$ . We then have the corresponding infinite ascending sequence $s_{n,0} = s_{k_0, 0} <_S s_{k_1, 0} <_S \cdots $ in S. Thus $s_{n,0}$ cannot be in R as then R would not be reverse well-founded. Therefore $\{n : s_{n,0} \in R\}$ is the set of true numbers for f, which completes the proof.

By taking complements and/or reversing the partial order, the statement “ $p{\downarrow }$ is well-founded” may be replaced by any of “ $p{\downarrow }$ is ill-founded,” “ $p{\uparrow }$ is reverse well-founded,” and “ $p{\uparrow }$ is reverse ill-founded” in Lemma 4.5 item (2) and the lemma remains true.

The proof that $\mathsf {ACA}_0$ implies Lemma 4.5 item (2) is uniform with respect to the partial order. That is, $\mathsf {ACA}_0$ proves that if $P_0, P_1, P_2, \dots $ is a sequence of partial orders without infinite antichains or suborders of type $\zeta $ , then there is a sequence of sets $W_0, W_1, W_2, \dots $ where, for each i, $W_i$ consists of exactly the $p \in P_i$ such that $p{\downarrow }$ is well-founded. The proof that $\mathsf {ACA}_0$ implies Lemma 4.5 item (3) is similarly uniform. In fact, to conclude Lemma 4.5 item (3) for a finite sequence of linear orders $L_0, L_1, \dots , L_{n-1}$ , as we shall need in Theorem 4.9, one application of Lemma 4.5 item (2) suffices. Given linear orders $L_0, L_1, \dots , L_{n-1}$ without suborders of type $\zeta $ , let P be the partial order consisting of the disjoint union of the linear orders $L_i$ for $i < n$ . Then P has no infinite antichain and no suborder of type $\zeta $ , so by Lemma 4.5 item (2), there is a set W consisting of exactly the $p \in P$ such that $p{\downarrow }$ is well-founded. Then let $W_i = L_i \cap W$ and $R_i = L_i \setminus W$ for each $i < n$ .

If an infinite ascending sequence $A = \langle a_n : n \in \mathbb {N} \rangle $ in a partial order $(P, <_P)$ is not $(0,\infty )$ -homogeneous, then there is a $p \in P$ that is comparable with some elements of P, but only finitely many. As A is an ascending sequence, this means that there is an $n_0$ such that $p>_P a_{n_0}$ , but $\forall n> n_0 \, (p \mid _P a_n)$ . We think of such a p as a counterexample to A being $(0,\infty )$ -homogeneous. Indeed, p is also a counterexample to $\langle a_n : n \geq n_0 \rangle $ being $(0,\infty )$ -homogeneous.

Notice that if B is a counterexample sequence for an infinite ascending sequence A in some partial order $(P, <_P)$ , then $A \leq _{\forall \exists } B$ , but $B \nleq _{\forall \exists } A$ .

Suppose that A is an infinite ascending sequence in a partial order $(P, <_P)$ where no tail of A is $(0,\infty )$ -homogeneous. Then for every n, there is a counterexample p to $A_{\geq n}$ . If P has finite width, then we can make a counterexample sequence out of such counterexamples.

We are now prepared to give a proof of $\mathsf {RSpo}_{<\infty }$ in $\mathsf {ACA}_0$ .

Proof It suffices to show that $\mathsf {ACA}_0 \vdash \mathsf {RSpo}^{\mathsf {CD}}_{<\infty }$ because $\mathsf {RSpo}_{<\infty }$ and $\mathsf {RSpo}^{\mathsf {CD}}_{<\infty }$ are equivalent over $\mathsf {RCA}_0$ as explained in Section 3. In fact, here we may use that $\mathsf {WKL}_0 \vdash \forall k \, (\mathsf {RSpo}_k \leftrightarrow \mathsf {RSpo}^{\mathsf {CD}}_k)$ , which is simpler than appealing to Theorem 3.5.

Let $(P, <_P)$ be an infinite partial order with k-chain decomposition $C_0, \dots , C_{k-1}$ for some k. Assume for a contradiction that P does not contain a $(0,\infty )$ -homogeneous chain. Then P contains no chain of order-type $\zeta $ because such a chain is automatically $(0,\infty )$ -homogeneous. In particular, no $C_i$ for $i < k$ contains a chain of order-type $\zeta $ , so each $C_i$ may be viewed as a linear order with no suborder of type $\zeta $ . As discussed above, the (1) $\Rightarrow $ (3) direction of Lemma 4.5 generalizes to simultaneously handle any sequence of linear orders without suborders of type $\zeta $ . Apply this to the chains $C_0, \dots , C_{k-1}$ to partition $C_i$ for each $i < k$ into $C_i = W_i \cup R_i$ , where $W_i <_P R_i$ , $W_i$ is well-founded, and $R_i$ is reverse well-founded.

By $\mathsf {RT}^1_{<\infty }$ , either $W_i$ is infinite for some $i < k$ or $R_i$ is infinite for some $i < k$ . Without loss of generality, we may assume that some $W_i$ is infinite because otherwise we could work with the reversed partial order $(P,>_P)$ instead. Relabel the chains $C_0, \dots , C_{k-1}$ so that the infinite chains $W_i$ are exactly $W_0, \dots , W_{u-1}$ for some u with $0 < u \leq k$ . For each $i < u$ , let $\widehat {W}_i = \{p \in W_i : \forall n \; \exists q> n \; (q >_P p \;\wedge \; q \in W_i)\}$ be the elements of $W_i$ with infinitely many successors in $W_i$ . The set $W_i \setminus \widehat {W}_i$ is finite for each $i < u$ because if $W_i \setminus \widehat {W}_i$ were infinite, then it would be a chain in $W_i$ of order-type $\omega ^*$ , which contradicts that $W_i$ is well-founded. It follows that $\widehat {W}_i$ is infinite, well-founded, and has no maximum element for each $i < u$ . Therefore, for each $i < u$ we can define an infinite ascending sequence $A_i$ in $\widehat {W}_i$ that is cofinal in $\widehat {W}_i$ .

We assume that P does not contain a $(0,\infty )$ -homogeneous chain, so no tail of $A_i$ is $(0,\infty )$ -homogeneous for any $i < u$ . The argument of Lemma 4.8 generalizes to simultaneously handle any sequence of infinite ascending sequences. Apply this to the sequences $A_0, \dots , A_{u-1}$ to obtain infinite ascending sequences $B_0, \dots , B_{u-1}$ and a function $h \colon u \rightarrow k$ such that for each $i < u$ , $B_i$ is a counterexample sequence to $A_i$ that is contained in chain $C_{h(i)}$ . Notice that $B_i \cap R_{h(i)} = \emptyset $ for each $i < u$ because $B_i$ is an ascending sequence and $R_{h(i)}$ is reverse well-founded. Thus $B_i \subseteq W_{h(i)}$ , which means that $W_{h(i)}$ is infinite and therefore that $h(i) < u$ . Thus h is in fact a function $h \colon u \rightarrow u$ . Furthermore, $B_i \subseteq \widehat {W}_{h(i)}$ because every element of $B_i$ has infinitely many successors in $W_{h(i)}$ .

Now observe that $B_i \leq _{\forall \exists } A_{h(i)}$ for each $i < u$ because $B_i \subseteq \widehat {W}_{h(i)}$ and $A_{h(i)}$ is cofinal in $\widehat {W}_{h(i)}$ . Additionally, $A_{h(i)} \leq _{\forall \exists } B_{h(i)}$ for each $i < u$ because $B_{h(i)}$ is a counterexample sequence for $A_{h(i)}$ . Therefore $B_i \leq _{\forall \exists } A_{h(i)} \leq _{\forall \exists } B_{h(i)}$ , so $B_i \leq _{\forall \exists } B_{h(i)}$ for each $i < u$ by transitivity. Let $h^n$ denote the n ^th iterate of h, where $h^0(i) = i$ and $h^{n+1}(i) = h(h^n(i))$ for each $i < u$ . By induction, we obtain that $B_{h^m(i)} \leq _{\forall \exists } B_{h^n(i)}$ for all $i < u$ whenever $m \leq n$ . By the pigeonhole principle, there are $m < n \leq u$ with $h^m(0) = h^n(0)$ . We then have that

$$ \begin{align*} B_{h^{m+1}(0)} \leq_{\forall\exists} B_{h^n(0)} = B_{h^m(0)} \leq_{\forall\exists} A_{h^{m+1}(0)} \end{align*} $$

and therefore that $B_{h^{m+1}(0)} \leq _{\forall \exists } A_{h^{m+1}(0)}$ by transitivity. This contradicts that $B_{h^{m+1}(0)}$ is a counterexample sequence for $A_{h^{m+1}(0)}$ , which completes the proof.

If we want a $(0,\mathrm {cof})$ -homogeneous chain rather than a $(0,\infty )$ -homogeneous chain in a given partial order $(P, <_P)$ of finite width, then we may no longer assume that P contains no suborder of type $\zeta $ , and we may no longer apply Lemma 4.5 item (3) to partition each chain $C_i$ into well-founded and reverse well-founded parts. Instead, we may directly define the reverse ill-founded part of each $C_i$ and then proceed as before. This pushes the complexity up to $\Pi ^1_1\text {-}\mathsf {CA}_0$ because defining the set of reverse ill-founded elements in a linear order requires $\Pi ^1_1\text {-}\mathsf {CA}_0$ in general, as shown in Theorem 8.3.

5 Proofs of $\mathsf {RSpo}_{<\infty }$ , $\mathsf {RSpo}_k$ , and $(0,\mathrm {cof})\text {-}\mathsf {RSpo}^{\mathsf {CD}}_2$ in $\mathsf {RCA}_0 + \mathsf {I}\Sigma ^0_{2} + \mathsf {ADS}$ and below

The goal of this section is to show the following:

• • $\mathsf {RCA}_0 + \mathsf {I}\Sigma ^0_{2} + \mathsf {ADS} \vdash \mathsf {RSpo}_{<\infty }$ (Theorem 5.5).

• • $\mathsf {RCA}_0 + \mathsf {ADS} \vdash \mathsf {RSpo}_k$ for each fixed k (Theorem 5.6).

• • $\mathsf {RCA}_0 + \mathsf {SADS} \vdash \mathsf {RSpo}^{\mathsf {CD}}_2$ (Theorem 5.9).

• • $\mathsf {RCA}_0 + \mathsf {I}\Sigma ^0_{2} + \mathsf {ADS} \vdash (0,\mathrm {cof})\text {-}\mathsf {RSpo}_2$ (Theorem 5.11).

The main tools used in the proof of $\mathsf {RSpo}_{<\infty }$ in $\mathsf {ACA}_0$ from Theorem 4.9 are the counterexamples and counterexample sequences of Definition 4.7. Let $A = \langle a_n : n \in \mathbb {N} \rangle $ be an infinite ascending sequence in a partial order $(P, <_P)$ such that no tail of A is $(0,\infty )$ -homogeneous. Given a $p \in P$ , p being a counterexample to a given tail of A is a $\Pi ^0_1$ property, thus when working strictly below $\mathsf {ACA}_0$ we may not necessarily be able to produce a counterexample sequence for A as in Lemma 4.8. However, given an $a_m$ , we can effectively search for an $a_n$ and a $p \in P$ with $p \geq _P a_m$ and $p \mid _P a_n$ . This search procedure can be used to produce ladders for A according to the following definition. These ladders play the role of the counterexample sequences.

In Definition 5.1, the sequence S is not required to be ascending, but in practice it usually is. Notice also that if A is an infinite ascending sequence in a partial order $(P, <_P)$ , then A is a ladder for itself.

Let $(P, <_P)$ be a partial order that has been decomposed into k chains as $P = C_0 \cup \cdots \cup C_{k-1}$ , and let $\vec {P}$ denote $\vec {P} = P \oplus {<_P} \oplus C_0 \oplus \cdots \oplus C_{k-1}$ . Suppose that A is an infinite ascending sequence that is contained in some chain $C_j$ . To produce a $(0,\infty )$ -homogeneous chain for P, we look for ladders for A in the chains $C_i$ with $i \neq j$ . To do this, we define a Turing functional $\operatorname {{\mathrm {FindLadder}}}^{\vec {P}} \colon P^{\mathbb {N}} \times k \rightarrow P^{\mathbb {N}}$ relative to $\vec {P}$ , where $\operatorname {{\mathrm {FindLadder}}}^{\vec {P}}(A, i)$ attempts to compute a ladder for A in $C_i$ . We then use $\mathsf {I}\Sigma ^0_{2}$ in the form of bounded $\Pi ^0_2$ comprehension to determine the $i < k$ with $i \neq j$ for which $\operatorname {{\mathrm {FindLadder}}}^{\vec {P}}(A, i)$ is total. If $\operatorname {{\mathrm {FindLadder}}}^{\vec {P}}(A, i)$ is total, we then want to find ladders for it in the chains $C_{\ell }$ with $\ell \neq i$ and continue this process either until finding enough ladders to knit together into a $(0,\infty )$ -homogeneous chain or until realizing that there are so few ladders that a tail of one of them must already be $(0,\infty )$ -homogeneous. In fact, we consider all the iterations of $\operatorname {{\mathrm {FindLadder}}}^{\vec {P}}$ that we may eventually need up front and apply bounded $\Pi ^0_2$ comprehension only once.

Lemma 5.2 says that if $(P, <_P)$ is a partial order decomposed into chains $C_0, \dots , C_{k-1}$ and A is an infinite ascending sequence in P with no $(0,\infty )$ -homogeneous tail, then it is possible to search for a ladder for A in some $C_i$ .

Lemma 5.2. The following is provable in $\mathsf {RCA}_0 + \mathsf {B}\Sigma ^0_{2}$ . Let $(P, <_P)$ be an infinite partial order with k-chain decomposition $C_0, \dots , C_{k-1}$ , and let $A = \langle a_n : n \in \mathbb {N} \rangle $ be an infinite ascending sequence in P. If no tail of A is $(0,\infty )$ -homogeneous, then there is an $i < k$ such that

$$ \begin{align*} \forall m \; \exists n \; \exists p \in C_i \; (p \geq_P a_m \;\wedge\; p \mid_P a_n). \end{align*} $$

Proof Suppose that no tail $A_{\geq m}$ of A is $(0,\infty )$ -homogeneous. Then for every m, there is a counterexample p to the tail $A_{\geq m}$ . This implies that

$$ \begin{align*} \forall m \; \exists n \; \exists p \in P \; (p \geq_P a_m \;\wedge\; p \mid_P a_n). \end{align*} $$

Thus we may define a function $f \colon \mathbb {N} \rightarrow k$ as follows. Given m, search for an n and a p with $p \geq _P a_m$ and $p \mid _P a_n$ , find the $i < k$ with $p \in C_i$ , and output $f(m) = i$ . By $\mathsf {RT}^1_{<\infty }$ , there is an $i < k$ such that $f(m) = i$ for infinitely many m. This i satisfies the conclusion of the lemma.

Again let $(P, <_P)$ be a partial order with k-chain decomposition $C_0, \dots , C_{k-1}$ . Lemma 5.3 shows how to search for a ladder for a given infinite sequence A within a target chain $C_i$ . It may be thought of as a weaker, yet effective, version of Lemma 4.8.

Proof Let $A = \langle a_n : n \in \mathbb {N} \rangle $ be an infinite sequence in P, and let $i < k$ . Compute $\operatorname {{\mathrm {FindLadder}}}^{\vec {P}}(A, i)(0)$ by searching for an n and a $p_0 \in C_i$ with $p_0 \geq _P a_0$ and $p_0 \mid _P a_n$ . If $p_0$ is found, then output $\operatorname {{\mathrm {FindLadder}}}^{\vec {P}}(A, i)(0) = p_0$ . Compute $\operatorname {{\mathrm {FindLadder}}}^{\vec {P}}(A, i)(m+1)$ by first computing $p_m = \operatorname {{\mathrm {FindLadder}}}^{\vec {P}}(A, i)(m)$ . Then search for an n and a $p_{m+1} \in C_i$ with $p_{m+1}>_P p_m$ , $p_{m+1} \geq _P a_{m+1}$ , and $p_{m+1} \mid _P a_n$ . If $p_{m+1}$ is found, then output $\operatorname {{\mathrm {FindLadder}}}^{\vec {P}}(A, i)(m+1) = p_{m+1}$ .

Item (2) follows immediately from the definition of $\operatorname {{\mathrm {FindLadder}}}^{\vec {P}}$ . If $A = \langle a_n : n \in \mathbb {N} \rangle $ is an infinite sequence in P, if $i < k$ , and if $\operatorname {{\mathrm {FindLadder}}}^{\vec {P}}(A, i)$ is total, then it must be that $\operatorname {{\mathrm {FindLadder}}}^{\vec {P}}(A, i)(m) \in C_i$ , that $a_m \leq _P \operatorname {{\mathrm {FindLadder}}}^{\vec {P}}(A, i)(m)$ , and that $\operatorname {{\mathrm {FindLadder}}}^{\vec {P}}(A, i)(m) <_P \operatorname {{\mathrm {FindLadder}}}^{\vec {P}}(A, i)(m+1)$ for every m.

For item (1), let $A = \langle a_n : n \in \mathbb {N} \rangle $ be an infinite sequence in P, let $i < k$ , and suppose that for every m there are an n and a $p \in C_i$ with $p \geq _P a_m$ and $p \mid _P a_n$ . We use $\mathsf {I}\Sigma ^0_{1}$ to show that $\operatorname {{\mathrm {FindLadder}}}^{\vec {P}}(A, i)$ is total. By assumption, there are an n and a $p_0 \in C_i$ with $p_0 \geq _P a_0$ and $p_0 \mid _P a_n$ . Thus $\operatorname {{\mathrm {FindLadder}}}^{\vec {P}}(A, i)(0)$ is defined. Inductively assume that $p_m = \operatorname {{\mathrm {FindLadder}}}^{\vec {P}}(A, i)(m)$ is defined. Then there is an $\ell $ such that $p_m \mid _P a_{\ell }$ . By assumption, there are an s and a $p \in C_i$ with

$$ \begin{align*} p \geq_P a_{m+1} \quad\text{and}\quad p \mid_P a_s \end{align*} $$

and also a t and a $q \in C_i$ with

$$ \begin{align*} q \geq_P a_{\ell} \quad\text{and}\quad q \mid_P a_t. \end{align*} $$

The elements p and q are both in the chain $C_i$ , so they are comparable. By taking $p_{m+1} = \max _{<_P}\{p, q\}$ and n as either s or t as appropriate, we obtain an n and a $p_{m+1} \in C_i$ with

$$ \begin{align*} p_{m+1} \geq_P a_{m+1} \quad\text{and}\quad p_{m+1} \geq_P a_{\ell} \quad\text{and}\quad p_{m+1} \mid_P a_n. \end{align*} $$

Again, $p_{m+1}$ and $p_m$ are both in the chain $C_i$ , so they are comparable. However, we cannot have that $p_{m+1} \leq _P p_m$ because this would imply that $a_{\ell } \leq _P p_{m+1} \leq _P p_m$ , which contradicts that $p_m \mid _P a_{\ell }$ . Therefore $p_m <_P p_{m+1}$ . Thus there are an n and a $p_{m+1} \in C_i$ with $p_{m+1}>_P p_m$ , $p_{m+1} \geq _P a_{m+1}$ , and $p_{m+1} \mid _P a_n$ . So $\operatorname {{\mathrm {FindLadder}}}^{\vec {P}}(A, i)(m+1)$ is defined.

The following lemma concerning finite labeled trees helps organize the proof of $\mathsf {RSpo}_{<\infty }$ in $\mathsf {RCA}_0 + \mathsf {I}\Sigma ^0_{2} + \mathsf {ADS}$ . Recall that for a finite rooted tree T, the height of a vertex is the length of the path from the vertex to the root, the height of the tree is the maximum height of a vertex in T, and level k of T consists of all the vertices of T that have height k. (We warn the reader that the height of a tree as defined here is one less than the height of the tree according to Definition 3.1 when considering the tree as a partial order. For example, the one-element tree consisting of only the root has height $0$ as a tree but height $1$ as a partial order.) For a rooted tree T, let $\preceq $ denote the associated tree-order on T, where $\sigma \preceq \tau $ if $\sigma $ is on the (unique) path from the root to $\tau $ . Let $\prec $ denote the strict version of $\preceq $ .

Proof It suffices to show that $\mathsf {RCA}_0 + \mathsf {I}\Sigma ^0_{2} + \mathsf {ADS} \vdash \mathsf {RSpo}^{\mathsf {CD}}_{<\infty }$ because $\mathsf {RSpo}_{<\infty }$ and $\mathsf {RSpo}^{\mathsf {CD}}_{<\infty }$ are equivalent over $\mathsf {RCA}_0$ as explained in Section 3. Thus let $(P, <_P)$ be an infinite partial order with k-chain decomposition $C_0, \dots , C_{k-1}$ for some k. We may assume that $k \geq 2$ because if P is a chain, then P itself is $(0,\infty )$ -homogeneous.

Some $C_i$ is infinite by $\mathsf {RT}^1_{<\infty }$ and therefore contains either an infinite ascending sequence or an infinite descending sequence by $\mathsf {ADS}$ . By relabeling the chains and by reversing the partial order if necessary, we may assume that there is an infinite ascending sequence $A = \langle a_n : n \in \mathbb {N} \rangle $ contained in chain $C_0$ . Let $\vec {P} = P \oplus {<_P} \oplus C_0 \oplus \cdots \oplus C_{k-1}$ , and let $\operatorname {{\mathrm {FindLadder}}}^{\vec {P}} \colon P^{\mathbb {N}} \times k \rightarrow P^{\mathbb {N}}$ be the Turing functional relative to $\vec {P}$ from Lemma 5.3.

Let $R = (k-1)^{\leq k}$ be the complete $(k-1)$ -ary tree of height k. Assign a label $\ell (\sigma ) \in \{0, \dots , k-1\}$ to each $\sigma \in R$ as follows. First, label the root $\emptyset \in R$ with $\ell (\emptyset ) = 0$ . Now suppose that $\sigma \in R$ is not a leaf and has been labeled $\ell (\sigma )$ . Index the $k-1$ children of $\sigma $ as $\langle \tau _i : i \in k \setminus \{\ell (\sigma )\} \rangle $ , and label $\ell (\tau _i) = i$ for each $i \in k \setminus \{\ell (\sigma )\}$ .

For a $\sigma \in \mathbb {N}^{<\mathbb {N}}$ with $|\sigma | \geq 1$ , let $\sigma ^- = \sigma {\restriction } (|\sigma |-1)$ denote $\sigma $ with the last term cut off. For $\sigma \in R$ , let $\operatorname {{\mathrm {FindLadder}}}^{\vec {P},\sigma }$ denote the iteration of $\operatorname {{\mathrm {FindLadder}}}^{\vec {P}}$ given by

$$ \begin{align*} \operatorname{{\mathrm{FindLadder}}}^{\vec{P}, \emptyset}(A) &= A,\\ \operatorname{{\mathrm{FindLadder}}}^{\vec{P}, \sigma}(A) &= \operatorname{{\mathrm{FindLadder}}}^{\vec{P}}(\operatorname{{\mathrm{FindLadder}}}^{\vec{P}, \sigma^-}(A), \ell(\sigma)), & \text{if } |\sigma| \geq 1. \end{align*} $$

So if $\sigma \in R$ has $|\sigma | \geq 1$ , then $\operatorname {{\mathrm {FindLadder}}}^{\vec {P}, \sigma }(A)$ is

$$ \begin{align*} \operatorname{{\mathrm{FindLadder}}}^{\vec{P}}\bigl(\cdots \operatorname{{\mathrm{FindLadder}}}^{\vec{P}}\bigl(\operatorname{{\mathrm{FindLadder}}}^{\vec{P}}(A, \ell(\sigma {\restriction} 1)), \ell(\sigma {\restriction} 2)\bigr) \cdots, \ell(\sigma)\bigr). \end{align*} $$

Now use $\mathsf {I}\Sigma ^0_{2}$ in the form of bounded $\Pi ^0_2$ comprehension to form the subtree $T \subseteq R$ given by

$$ \begin{align*} T = \bigl\{\sigma \in R : \operatorname{{\mathrm{FindLadder}}}^{\vec{P}, \sigma}(A) \text{ is total}\bigr\}. \end{align*} $$

Notice that if $\sigma $ is in T, then $\operatorname {{\mathrm {FindLadder}}}^{\vec {P}, \sigma }(A)$ computes an infinite ascending sequence in $C_{\ell (\sigma )}$ by Lemma 5.3 item (2) and the fact that A is an infinite ascending sequence in $C_0 = C_{\ell (\emptyset )}$ .

There are now two cases. The first case is that T has a leaf $\sigma $ at some level $<\! k$ . Let $\langle \tau _i : i \in k \setminus \{\ell (\sigma )\} \rangle $ again denote the indexing of $\sigma $ ’s children in R. As $\sigma $ is in T, $\operatorname {{\mathrm {FindLadder}}}^{\vec {P}, \sigma }(A)$ computes the infinite ascending sequence $B = \langle b_n : n \in \mathbb {N} \rangle $ in $C_{\ell (\sigma )}$ given by $b_n = \operatorname {{\mathrm {FindLadder}}}^{\vec {P}, \sigma }(A)(n)$ for all n. If no tail of B is $(0,\infty )$ -homogeneous, then by Lemma 5.2 there is an $i < k$ such that

$$ \begin{align*} \forall m \; \exists n \; \exists p \in C_i \; \bigl(p \geq_P b_m \;\wedge\; p \mid_P b_n \bigr). \end{align*} $$

It cannot be that $i = \ell (\sigma )$ , so there must be such an $i \in k \setminus \{\ell (\sigma )\}$ . Thus, by Lemma 5.3 item (1),

$$ \begin{align*} \operatorname{{\mathrm{FindLadder}}}^{\vec{P}, \tau_i}\kern-1pt(A) = \operatorname{{\mathrm{FindLadder}}}^{\vec{P}}\kern-1pt(\operatorname{{\mathrm{FindLadder}}}^{\vec{P}, \sigma}\kern-1pt(A), \ell\kern-1pt(\tau_i)) = \operatorname{{\mathrm{FindLadder}}}^{\vec{P}}\kern-1pt(B, i) \end{align*} $$

is total. This means that $\tau _i \in T$ , which contradicts that $\sigma $ is a leaf of T. Therefore some tail of B is indeed $(0,\infty )$ -homogeneous. We may thin this tail so that its range exists as a set, thereby producing a $(0,\infty )$ -homogeneous chain in P.

The second case is that every leaf of T is at level k. Then T and $\ell $ satisfy the hypotheses of Lemma 5.4. Let $\sigma $ be as in the conclusion of Lemma 5.4 for T and $\ell $ . For each child $\tau $ of $\sigma $ in T, let $\eta _{\tau } \in T$ be such that $\eta _{\tau } \succ \tau $ and $\ell (\eta _{\tau }) = \ell (\sigma )$ . As $\sigma \in T$ , $\operatorname {{\mathrm {FindLadder}}}^{\vec {P}, \sigma }(A)$ computes the infinite ascending sequence $X = \langle x_n : n \in \mathbb {N} \rangle $ in $C_{\ell (\sigma )}$ given by $x_n = \operatorname {{\mathrm {FindLadder}}}^{\vec {P}, \sigma }(A)(n)$ for all n. Likewise, $\operatorname {{\mathrm {FindLadder}}}^{\vec {P}, \eta _{\tau }}(A)$ also computes an infinite ascending sequence in $C_{\ell (\eta _{\tau })} = C_{\ell (\sigma )}$ for each child $\tau $ of $\sigma $ in T. Define the infinite sequence $Y = \langle y_n : n \in \mathbb {N} \rangle $ by setting

$$ \begin{align*} y_n = \textstyle{\max_{<_P}}\left\{\operatorname{{\mathrm{FindLadder}}}^{\vec{P}, \eta_{\tau}}(A)(n) : \tau \text{ is a child of } \sigma \text{ in } T\right\} \end{align*} $$

for each n. Then Y is an infinite ascending sequence in $C_{\ell (\sigma )}$ that is cofinal in the union of the sequences computed by the $\operatorname {{\mathrm {FindLadder}}}^{\vec {P}, \eta _{\tau }}(A)$ for the children $\tau $ of $\sigma $ in T.

Claim 1. Let $\tau $ be a child of $\sigma $ in T. Then every $p \in C_{\ell (\tau )}$ is either above every element of X or below some element of Y (and hence below almost every element of Y).

Proof of Claim

We have that $\operatorname {{\mathrm {FindLadder}}}^{\vec {P}, \sigma }(A)$ computes the infinite ascending sequence X and that

$$ \begin{align*} \operatorname{{\mathrm{FindLadder}}}^{\vec{P}, \tau}(A) &= \operatorname{{\mathrm{FindLadder}}}^{\vec{P}}(\operatorname{{\mathrm{FindLadder}}}^{\vec{P}, \sigma}(A), \ell(\tau)) \\&= \operatorname{{\mathrm{FindLadder}}}^{\vec{P}}(X, \ell(\tau)) \end{align*} $$

is total, so $\operatorname {{\mathrm {FindLadder}}}^{\vec {P}, \tau }(A)$ computes a ladder Z for X in $C_{\ell (\tau )}$ . Consider any $p \in C_{\ell (\tau )}$ and its location with respect to the elements of Z. If p is above every element of Z, then p is above every element of X because Z is a ladder for X. Suppose instead that p is below some element $\operatorname {{\mathrm {FindLadder}}}^{\vec {P}, \tau }(A)(n)$ of Z. Consider now the path $\tau = \alpha _0 \prec \alpha _1 \prec \cdots \prec \alpha _{m-1} = \eta _{\tau }$ from $\tau $ to $\eta _{\tau }$ in T. For each $i < m$ , $\operatorname {{\mathrm {FindLadder}}}^{\vec {P}, \alpha _i}(A)$ is total because $\alpha _i \in T$ . Thus $\operatorname {{\mathrm {FindLadder}}}^{\vec {P}, \alpha _{i+1}}(A)$ computes a ladder for $\operatorname {{\mathrm {FindLadder}}}^{\vec {P}, \alpha _i}(A)$ for each $i < m-1$ . Therefore,

$$ \begin{align*} p &\leq_P \operatorname{{\mathrm{FindLadder}}}^{\vec{P}, \tau}(A)(n) \leq_P \operatorname{{\mathrm{FindLadder}}}^{\vec{P}, \alpha_1}(A)(n) \leq_P \cdots \\ &\leq_P \operatorname{{\mathrm{FindLadder}}}^{\vec{P}, \alpha_{m-2}}(A)(n)\leq_P \operatorname{{\mathrm{FindLadder}}}^{\vec{P}, \eta_{\tau}}(A)(n) \leq_P y_n. \end{align*} $$

So p is below an element of Y.

Claim 2. There is an m such that whenever $i \in k \setminus \bigl (\{\ell (\sigma )\} \cup \{\ell (\tau ) : \tau \text { is a child of } \sigma \text { in } T\}\bigr )$ and $p \in C_i$ , then either p is comparable with almost every element of $X_{\geq m}$ , or p is incomparable with every element of $X_{\geq m}$ .

Proof of Claim

Let I denote the finite set

$$ \begin{align*} I = k \setminus \bigl(\{\ell(\sigma)\} \cup \{\ell(\tau) : \tau \text{ is a child of } \sigma \text{ in } T\}\bigr), \end{align*} $$

let $i \in I$ , let $\tau $ be the child of $\sigma $ in R with $\ell (\tau ) = i$ , and notice that $\tau \notin T$ . We have that $\operatorname {{\mathrm {FindLadder}}}^{\vec {P}, \sigma }(A)$ computes the infinite ascending sequence X, so

$$ \begin{align*} \operatorname{{\mathrm{FindLadder}}}^{\vec{P}, \tau}(A) &= \operatorname{{\mathrm{FindLadder}}}^{\vec{P}}(\operatorname{{\mathrm{FindLadder}}}^{\vec{P}, \sigma}(A), \ell(\tau)) \\&= \operatorname{{\mathrm{FindLadder}}}^{\vec{P}}(X, \ell(\tau)) \end{align*} $$

must not be total because otherwise $\tau $ would be in T. Therefore by Lemma 5.3 item (1),

$$ \begin{align*} \exists m \; \forall n \; \forall p \in C_i \; \bigl(p \ngeq_P x_m \;\vee\; p \lessgtr_P x_n \bigr). \end{align*} $$

By applying $\mathsf {B}\Sigma ^0_{2}$ , we obtain a fixed m such that $\forall i \in I \; \forall n \; \forall p \in C_i \; (p \ngeq _P x_m \vee p \lessgtr _P x_n )$ . We show that this m satisfies the claim.

Let $p \in C_i$ for an $i \in I$ . If p is below an element of $X_{\geq m}$ , then p is below almost every element of $X_{\geq m}$ because $X_{\geq m}$ is an ascending sequence. If p is above an element of $X_{\geq m}$ , then $p \geq _P x_m$ , in which case p is comparable with every element of $X_{\geq m}$ . So if p is comparable with some element of $X_{\geq m}$ , then p is comparable with almost every element of $X_{\geq m}$ . That is, either p is comparable with almost every element of $X_{\geq m}$ , or p is incomparable with every element of $X_{\geq m}$ .

We can now assemble a $(0,\infty )$ -homogeneous chain B from X and Y. Let m be as in Claim 2. Thin the infinite ascending sequences $X_{\geq m}$ and Y to infinite ascending sequences $\widehat {X}_{\geq m}$ and $\widehat {Y}$ whose ranges exist as sets. Notice that $\widehat {X}_{\geq m} \cup \widehat {Y}$ is a chain because $\widehat {X}_{\geq m}$ and $\widehat {Y}$ are both contained in the chain $C_{\ell (\sigma )}$ . If $\widehat {Y} \leq _{\forall \exists } \widehat {X}_{\geq m}$ , then take $B = \widehat {X}_{\geq m}$ . Otherwise there is an n such that $y_n$ is above every element of $\widehat {X}_{\geq m}$ . In this case, take $B = \widehat {X}_{\geq m} \cup \widehat {Y}_{\geq n}$ . We show that B is $(0,\infty )$ -homogeneous.

Consider any $p \in P$ . If $p \in C_{\ell (\sigma )}$ , then p is comparable with every element of B because $B \subseteq C_{\ell (\sigma )}$ . Suppose that $p \in C_i$ for an $i \in \{\ell (\tau ) : \tau \text { is a child of } \sigma \text { in } T\}$ . By Claim 1, either p is above every element of X or below almost every element of Y. In either case, p is comparable with infinitely many elements of B. Finally, suppose that $p \in C_i$ for an $i \in k \setminus \bigl (\{\ell (\sigma )\} \cup \{\ell (\tau ) : \tau \text { is a child of } \sigma \text { in } T\}\bigr )$ . By Claim 2, either p is comparable with almost every element of $X_{\geq m}$ , or p is incomparable with every element of $X_{\geq m}$ . If p is comparable with almost every element of $X_{\geq m}$ , then p is comparable with infinitely many elements of B. Suppose instead that p is incomparable with every element of $X_{\geq m}$ . If we took $B = \widehat {X}_{\geq m}$ , then p is incomparable with every element of B. Suppose that we took $B = \widehat {X}_{\geq m} \cup \widehat {Y}_{\geq n}$ . If p is incomparable with every element of $\widehat {Y}_{\geq n}$ , then p is incomparable with every element of B. If p is below an element of $\widehat {Y}_{\geq n}$ , then p is below almost every element of $\widehat {Y}_{\geq n}$ and therefore is comparable with infinity many elements of B. If p is above an element of $\widehat {Y}_{\geq n}$ , then p is above every element of $\widehat {X}_{\geq m}$ and therefore is comparable with infinitely many elements of B. This completes the proof that B is $(0,\infty )$ -homogeneous for P.