# (Extra)ordinary equivalences with the ascending/descending sequence
principle

Marta Fiori-Carones  Institute of Mathematics, University of Warsaw, Banacha
2, 02-097 Warszawa, Poland<EMAIL_ADDRESS>https://martafioricarones.github.io ,  Alberto Marcone  Dipartimento di
scienze matematiche, informatiche e fisiche, Università di Udine, Via delle
Scienze 208, 33100 Udine, Italy<EMAIL_ADDRESS>http://users.dimi.uniud.it/ alberto.marcone/ ,  Paul Shafer  School of
Mathematics
University of Leeds
Leeds
LS2 9JT
United Kingdom<EMAIL_ADDRESS>http://www1.maths.leeds.ac.uk/ matpsh/
and  Giovanni Soldà  School of Mathematics
University of Leeds
Leeds
LS2 9JT
United Kingdom<EMAIL_ADDRESS>https://giovannisolda.github.io/

###### Abstract.

We analyze the axiomatic strength of the following theorem due to Rival and
Sands [RivalSands] in the style of reverse mathematics. _Every infinite
partial order $P$ of finite width contains an infinite chain $C$ such that
every element of $P$ is either comparable with no element of $C$ or with
infinitely many elements of $C$_. Our main results are the following. The
Rival–Sands theorem for infinite partial orders of arbitrary finite width is
equivalent to $\mathsf{I}\Sigma^{0}_{2}+\mathsf{ADS}$ over $\mathsf{RCA}_{0}$.
For each fixed $k\geq 3$, the Rival–Sands theorem for infinite partial orders
of width $\leq\\!k$ is equivalent to $\mathsf{ADS}$ over $\mathsf{RCA}_{0}$.
The Rival–Sands theorem for infinite partial orders that are decomposable into
the union of two chains is equivalent to $\mathsf{SADS}$ over
$\mathsf{RCA}_{0}$. Here $\mathsf{RCA}_{0}$ denotes the recursive
comprehension axiomatic system, $\mathsf{I}\Sigma^{0}_{2}$ denotes the
$\Sigma^{0}_{2}$ induction scheme, $\mathsf{ADS}$ denotes the
ascending/descending sequence principle, and $\mathsf{SADS}$ denotes the
stable ascending/descending sequence principle. To our knowledge, these
versions of the Rival–Sands theorem for partial orders are the first examples
of theorems from the general mathematics literature whose strength is exactly
characterized by $\mathsf{I}\Sigma^{0}_{2}+\mathsf{ADS}$, by $\mathsf{ADS}$,
and by $\mathsf{SADS}$. Furthermore, we give a new purely combinatorial result
by extending the Rival–Sands theorem to infinite partial orders that do not
have infinite antichains, and we show that this extension is equivalent to
arithmetical comprehension over $\mathsf{RCA}_{0}$.

###### 2020 Mathematics Subject Classification:

Primary 03B30, 03F35, 05D10, 06A06

##  1\. Introduction

One of the major initiatives in reverse mathematics is the logical analysis of
theorems of countable combinatorics, with special attention to Ramsey’s
theorem for pairs and its consequences [CholakJockuschSlaman, ChongSlamanYang,
ChongSlamanYangConvervation, ChongSlamanYangInductiveStrength,
HirschfeldtShore, LiuRT22vsWKL, LiuRT22vsWWKL, PateyYokoyama, SeetapunSlaman,
SlamanYokoyama, LermanSolomonTowsner]. We continue this tradition by analyzing
the second of two theorems from _On the adjacency of vertices to the vertices
of an infinite subgraph_ by Rival and Sands [RivalSands]. To our knowledge,
this analysis yields the first examples of theorems from the general
mathematics literature whose strength is exactly characterized by the
ascending/descending sequence principle.

Both of the Rival–Sands theorems are inspired by Ramsey’s theorem for pairs
and two colors. The first theorem is a hybrid _inside/outside_ version of
Ramsey’s theorem for pairs. Thinking in terms of graphs, Ramsey’s theorem for
pairs produces an infinite set $H$ that is either a clique or an independent
set in a given countable graph. However, Ramsey’s theorem provides no
information concerning the relationship between the vertices _inside_ $H$ and
the vertices _outside_ $H$. The _Rival–Sands theorem for graphs_ balances this
situation by producing an infinite set $H$ that is not necessarily a clique or
an independent set, but for which there is information concerning the
relationship between the vertices inside $H$ and the vertices outside $H$.

######  Rival–Sands theorem for graphs ([RivalSands]).

Every infinite graph $G$ contains an infinite subset $H$ such that every
vertex of $G$ is adjacent to precisely none, one, or infinitely many vertices
of $H$.

Rival and Sands note that the three options “none,” “one,” and “infinitely
many” in their theorem are all necessary. They ask for a class of graphs for
which the “one” option may be removed, and they show that this is possible for
the class of comparability graphs of infinite partial orders of finite width
(i.e., infinite partial orders for which there is a fixed finite upper bound
on the size of the antichains). We call the resulting theorem the _Rival–Sands
theorem for partial orders_.

######  Rival–Sands theorem for partial orders ([RivalSands]).

Every infinite partial order $P$ of finite width contains an infinite chain
$C$ such that every element of $P$ is either comparable with no element of $C$
or with infinitely many elements of $C$.

Furthermore, Rival and Sands show that in the case of countable partial
orders, the “infinitely many” option may be strengthened to “cofinitely many.”

The Rival–Sands theorems do not appear to be immediate consequences of any
version of Ramsey’s theorem, and neither Rival–Sands theorem appears to be an
immediate consequence of the other. Rival and Sands give direct proofs of both
theorems that do not invoke any other Ramsey-theoretic statement.
Interestingly, their proof of the Rival–Sands theorem for partial orders makes
essential use of $\Pi^{1}_{1}\mbox{-}\mathsf{CA}_{0}$ by iterating a maximal
chain principle that is equivalent to $\Pi^{1}_{1}\mbox{-}\mathsf{CA}_{0}$
over $\mathsf{RCA}_{0}$. We discuss this in detail in Section 8.

In [Fiori-CaronesShaferSolda], Fiori-Carones, Shafer, and Soldà analyze the
axiomatic and computational strength of the Rival–Sands theorem for graphs in
the style of reverse mathematics and Weihrauch analysis. In reverse
mathematics, the Rival–Sands theorem for graphs is equivalent to
$\mathsf{ACA}_{0}$ over $\mathsf{RCA}_{0}$. Thus the Rival–Sands theorem for
graphs is indirectly equivalent to Ramsey’s theorem for triples (which is also
equivalent to $\mathsf{ACA}_{0}$, see [SimpsonSOSOA]), but it does not follow
from Ramsey’s theorem for pairs (which is strictly weaker than
$\mathsf{ACA}_{0}$ [SeetapunSlaman]). However, the authors of [Fiori-
CaronesShaferSolda] together with Hirst and Lempp show that a weakened inside-
only version of the Rival–Sands theorem for graphs is indeed equivalent to
Ramsey’s theorem for pairs and two colors. In terms of the Weihrauch degrees,
the main result of [Fiori-CaronesShaferSolda] is that the Rival–Sands theorem
for graphs is strongly Weihrauch-equivalent to the double-jump of weak König’s
lemma. To the authors’ knowledge, the Rival–Sands theorem for graphs is the
first theorem from the general mathematics literature exhibiting exactly this
strength. Furthermore, combining the aforementioned equivalence with a result
of Brattka and Rakotoniaina [BrattkaRakotoniaina] yields that the Rival–Sands
theorem for graphs is Weihrauch-equivalent to the parallelization of Ramsey’s
theorem for pairs and two colors. Thus the uniform computational strength of
the Rival–Sands theorem for graphs is exactly characterized by the ability to
simultaneously solve countably many instances of Ramsey’s theorem for pairs in
parallel.

In this work, we characterize the axiomatic strength of the Rival–Sands
theorem for partial orders in terms of the _ascending/descending sequence
principle_ , which states that an infinite linear order contains either an
infinite ascending sequence or an infinite descending sequence. Our primary
focus is the Rival–Sands theorem for partial orders as stated above, but we
also consider the version with “cofinitely many” in place of “infinitely
many.” The main results are the following, which are summarized in Theorem 6.6
below.

  * •

The Rival–Sands theorem for infinite partial orders of arbitrary finite width
is equivalent to the ascending/descending sequence principle plus the
$\Sigma^{0}_{2}$ induction scheme over $\mathsf{RCA}_{0}$.

  * •

For each fixed standard $k\geq 3$, the Rival–Sands theorem for infinite
partial orders of width $\leq\\!k$ is equivalent to the ascending/descending
sequence principle over $\mathsf{RCA}_{0}$.

  * •

The Rival–Sands theorem for infinite partial orders that are decomposable into
the union of two chains is equivalent to the stable ascending/descending
sequence principle over $\mathsf{RCA}_{0}$.

  * •

The Rival–Sands theorem with “cofinitely many” in place of “infinitely many”
for infinite partial orders of width $\leq\\!2$ is equivalent to the
ascending/descending sequence principle over $\mathsf{RCA}_{0}$ plus the
$\Sigma^{0}_{2}$-induction scheme.

Furthermore, in Theorems 7.2 and 7.3, we give a new purely combinatorial
result by extending the Rival–Sands theorem to all countably infinite partial
orders that do not have infinite antichains. This is non-trivial, as a partial
order may have arbitrarily large finite antichains, and therefore _not_ have
finite width, yet still have no infinite antichain. In Theorem 7.8, we also
show that the extension of the Rival–Sands theorem to countably infinite
partial orders without infinite antichains is equivalent to $\mathsf{ACA}_{0}$
over $\mathsf{RCA}_{0}$.

Computational aspects of linear and partial orders have been long-studied. In
reverse mathematics, the ascending/descending sequence principle is a weak
consequence of Ramsey’s theorem for pairs that was first isolated and studied
by Hirschfeldt and Shore [HirschfeldtShore]. There are a few classical
statements that are readily equivalent to this principle over
$\mathsf{RCA}_{0}$, such as the statement “Every countable sequence of real
numbers contains a monotone subsequence” (see [KreuzerThesis]*Remark 6.8), but
thus far the principle’s primary use has been as an important technical
benchmark. To our knowledge, Theorem 6.6 provides the first examples from the
modern mathematical literature of theorems that are equivalent to the
ascending/descending sequence principle, the ascending/descending sequence
principle plus $\Sigma^{0}_{2}$ induction, and to the stable
ascending/descending sequence principle. This explains our title. It is
extraordinary to find theorems from the ordinary literature that are
equivalent to the ascending/descending sequence principle.

It follows from our analysis that the Rival–Sands theorem for partial orders
without infinite antichains is equivalent to the Rival–Sands theorem for
graphs, but that the Rival–Sands theorem for partial orders of finite width is
strictly weaker. The relationship between the Rival–Sands theorem for partial
orders and Ramsey’s theorem for pairs is more curious. Ramsey’s theorem for
pairs and two colors suffices to prove the Rival–Sands theorem for partial
orders of width $k$ for any fixed $k$, but not for partial orders of arbitrary
finite width. However, Ramsey’s theorem for pairs and arbitrarily many colors
does suffice to prove the Rival–Sands theorem for partial orders of arbitrary
finite width. This is a matter of induction. Ramsey’s theorem for pairs and
two colors does not prove the $\Sigma^{0}_{2}$ induction scheme
[ChongSlamanYangInductiveStrength], but Ramsey’s theorem for pairs and
arbitrarily many colors does [HirstThesis]. All together, the Rival–Sands
theorem for partial orders of arbitrary finite width is strictly weaker than
Ramsey’s theorem for pairs and arbitrarily many colors; the Rival–Sands
theorem for partial orders of arbitrary finite width is not provable from
Ramsey’s theorem for pairs and two colors; and the Rival–Sands theorem for
partial orders of a fixed finite width $k$ is strictly weaker than Ramsey’s
theorem for pairs and two colors.

This article is organized as follows. Section 2 gives an overview of the
relevant reverse mathematics background. Section 3 formalizes several versions
of the Rival–Sands theorem for partial orders and discusses principles
concerning chains in partial orders, most notably Kierstead’s effective analog
of Dilworth’s theorem [KiersteadDilworth]. Section 4 presents our first proofs
of the Rival–Sands theorem for partial orders. These proofs are not
axiomatically optimal, but they are easy to understand, and they introduce
ideas that we later effectivize in order to give proofs in weaker systems.
Section 5 provides the forward directions of the equivalences of Theorem 6.6
mentioned above. Section 6 provides the reverse directions of the equivalences
of Theorem 6.6. Section 7 provides our extension of the Rival–Sands theorem to
infinite partial orders without infinite antichains and a proof that this
extension is equivalent to $\mathsf{ACA}_{0}$. All the proofs of the
Rival–Sands theorem for partial orders and its variants given in Sections 4–7
are new. In Section 8, we discuss the original proof by Rival and Sands, and
we analyze several principles asserting that partial orders contain various
sorts of maximal chains.

##  2\. Reverse mathematics background

We give a brief review of $\mathsf{RCA}_{0}$, $\mathsf{WKL}_{0}$,
$\mathsf{ACA}_{0}$, $\Pi^{1}_{1}\mbox{-}\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
[SimpsonSOSOA] and to Hirschfeldt’s monograph [HirschfeldtBook].

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

$\displaystyle\bigl{(}\varphi(0)\;\wedge\;\forall
n\,(\varphi(n)\;\rightarrow\;\varphi(n+1))\bigr{)}\;\rightarrow\;\forall
n\,\varphi(n),$

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

$\displaystyle\forall
n\,\bigl{(}\varphi(n)\;\leftrightarrow\;\psi(n)\bigr{)}\;\rightarrow\;\exists
X\,\forall n\,\bigl{(}n\in X\;\leftrightarrow\;\varphi(n)\bigr{)},$

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 [SimpsonSOSOA]*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. Furthermore, $\mathsf{RCA}_{0}$ suffices to
develop the basic theory of oracle Turing machines (see for example
[SimpsonSOSOA]*Section VII.1). As usual, $\Phi_{0},\Phi_{1},\Phi_{2},\dots$
denotes the standard enumeration of all Turing machines,
$\Phi_{e}^{X}(n){\downarrow}$ denotes that $\Phi_{e}$ halts on input $n$ when
equipped with oracle $X$, and $\Phi_{e}^{X}(n){\uparrow}$ denotes that
$\Phi_{e}$ does not halt on input $n$ when equipped with oracle $X$. We
sometimes write $\Phi_{e}^{X}(n){\downarrow}=y$ to emphasize that
$\Phi_{e}^{X}(n)$ halts and additionally that the output is $y$.

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$. 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

$\displaystyle\exists X\,\forall n\,\bigl{(}n\in
X\;\leftrightarrow\;\varphi(n)\bigr{)},$

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.

######  Lemma 2.1 (see [SimpsonSOSOA]*Lemma III.1.3).

The following are equivalent over $\mathsf{RCA}_{0}$.

  1. (1)

$\mathsf{ACA}_{0}$.

  2. (2)

If $f\colon\mathbb{N}\rightarrow\mathbb{N}$ is an injection, then there is a
set $X$ such that $\forall n\,(n\in X\;\leftrightarrow\;\exists s\,(f(s)=n))$.

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 [SimpsonSOSOA]*Theorem III.7.2).

The axioms of $\Pi^{1}_{1}\mbox{-}\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

$\displaystyle\exists X\,\forall n\,\bigl{(}n\in
X\;\leftrightarrow\;\varphi(n)\bigr{)},$

where $\varphi$ is a $\Pi^{1}_{1}$ formula in which $X$ is not free. To show
that some statement $\varphi$ implies $\Pi^{1}_{1}\mbox{-}\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$.

######  Theorem 2.2 ([MarconeNW]*Theorem 6.5).

The following are equivalent over $\mathsf{RCA}_{0}$.

  1. (1)

$\Pi^{1}_{1}\mbox{-}\mathsf{CA}_{0}$.

  2. (2)

$\mathsf{LPP}$.

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.

$\mathsf{ACA}_{0}$$\mathsf{RT}^{2}_{2}$$\mathsf{SRT}^{2}_{2}$$\mathsf{CAC}$$\mathsf{ADS}$$\mathsf{SADS}$$\mathsf{RT}^{1}_{<\infty}$$\mathsf{WKL}_{0}$$\mathsf{RCA}_{0}$
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 [ChongLemppYang, ChongSlamanYang, HirschfeldtShore,
HirstThesis, LermanSolomonTowsner, LiuRT22vsWKL, PateyImmunity,
SeetapunSlaman, SimpsonSOSOA].

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

$\displaystyle\bigl{(}\varphi(0)\;\wedge\;\forall
n\,(\varphi(n)\;\rightarrow\;\varphi(n+1))\bigr{)}\;\rightarrow\;\forall
n\,\varphi(n).$

  * •

The _least element principle for $\varphi$_ is the universal closure of the
formula

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

  * •

The _bounded comprehension axiom for $\varphi$_ is the universal closure of
the formula

$\displaystyle\forall b\,\exists X\,\forall n\,\bigl{(}n\in
X\;\leftrightarrow\;(n<b\;\wedge\;\varphi(n))\bigr{)},$

where $X$ is not free in $\varphi$.

  * •

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

$\displaystyle\forall a\,\bigl{(}\forall n<a\;\exists
m\;\varphi(n,m)\;\rightarrow\;\exists b\;\forall n<a\;\exists
m<b\;\varphi(n,m)\bigr{)},$

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 [HajekPudlak]*Section I.2 and
[SimpsonSOSOA]*Section II.3).

  * •

Neither $\mathsf{RCA}_{0}$ nor $\mathsf{WKL}_{0}$ proves
$\mathsf{B}\Sigma^{0}_{2}$ (see [SimpsonSOSOA]*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 [HajekPudlak]*Section I.2,
[HirstThesis], and [SimpsonSOSOA]*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}$ [ChongSlamanYangInductiveStrength].

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.

######  Definition 3.1 ($\mathsf{RCA}_{0}$).

Let $(P,<_{P})$ be a partial order.

  * •

Elements $p,q\in P$ are _comparable_ (written $p\between_{P}q$) if either
$p\leq_{P}q$ or $q\leq_{P}p$. If $p$ and $q$ are not comparable, then they are
_incomparable_ (written $p\mid_{P}q$).

  * •

A _chain_ in $P$ is a set $C\subseteq P$ of pairwise comparable elements.

  * •

An _antichain_ in $P$ is a set $X\subseteq P$ of pairwise incomparable
elements.

  * •

$P$ has _width_ $\leq\\!k$ if every antichain in $P$ has at most $k$ elements.
$P$ has _width_ $k$ if it has width $\leq\\!k$ but not width $\leq\\!k-1$. $P$
has _finite width_ if $P$ has width $\leq\\!k$ for some $k$.

  * •

$P$ has _height_ $\leq\\!k$ if every chain in $P$ has at most $k$ elements.
$P$ has _height_ $k$ if it has height $\leq\\!k$ but not height $\leq\\!k-1$.
$P$ has _finite height_ if $P$ has height $\leq\\!k$ for some $k$.

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.

######  Definition 3.2 ($\mathsf{RCA}_{0}$).

Let $(P,<_{P})$ be a partial order. An infinite chain $C\subseteq P$ is:

  * •

_$(0,\infty)$ -homogeneous_ for $P$ if every $p\in P$ is either comparable
with no element of $C$ or is comparable with infinitely many elements of $C$;

  * •

_$(0,\mathrm{cof})$ -homogeneous_ for $P$ if every $p\in P$ is either
comparable with no element of $C$ or is comparable with cofinitely many
elements of $C$.

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.

######  Definition 3.3 ($\mathsf{RCA}_{0}$).

  * •

$\mathsf{RSpo}_{k}$ is the statement “Every infinite partial order of width
$\leq\\!k$ has a $(0,\infty)$-homogeneous chain.”

  * •

$\mathsf{RSpo}_{<\infty}$ abbreviates $\forall k\,\mathsf{RSpo}_{k}$.

  * •

$(0,\mathrm{cof})\mbox{-}\mathsf{RSpo}_{k}$ is the statement “Every infinite
partial order of width $\leq\\!k$ has a $(0,\mathrm{cof})$-homogeneous chain.”

  * •

$(0,\mathrm{cof})\mbox{-}\mathsf{RSpo}_{<\infty}$ abbreviates $\forall
k\,(0,\mathrm{cof})\mbox{-}\mathsf{RSpo}_{k}$.

Immediately,
$\mathsf{RCA}_{0}\vdash(0,\mathrm{cof})\mbox{-}\mathsf{RSpo}_{k}\rightarrow\mathsf{RSpo}_{k}$
holds for every fixed $k$, and we have that
$\mathsf{RCA}_{0}\vdash(0,\mathrm{cof})\mbox{-}\mathsf{RSpo}_{<\infty}\rightarrow\mathsf{RSpo}_{<\infty}$
holds as well. Also, Proposition 6.5 below shows that for every $k\geq 2$,
$(0,\mathrm{cof})\mbox{-}\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.

######  Definition 3.4 ($\mathsf{RCA}_{0}$).

A _$k$ -chain decomposition_ of a partial order $(P,<_{P})$ consists of $k$
chains $C_{0},C_{1},\dots,C_{k-1}\subseteq P$ with $P=\bigcup_{i<k}C_{i}$. If
$P$ has a $k$-chain decomposition, then it is called _$k$ -chain
decomposable_.

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
proved that Dilworth’s theorem for countable partial orders is equivalent to
$\mathsf{WKL}_{0}$ over $\mathsf{RCA}_{0}$ [HirstThesis]. Thus Dilworth’s
theorem is not available when working in
$\mathsf{RCA}_{0}+\mathsf{I}\Sigma^{0}_{2}+\mathsf{ADS}$, for example.
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
[KiersteadDilworth]. 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 [BosekKiersteadKrawczykMateckiSmith].

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
[KiersteadDilworth]*Theorem 1.10. With this view, it is possible to verify
that Kierstead’s theorem is provable in $\mathsf{RCA}_{0}$.

######  Theorem 3.5 ($\mathsf{RCA}_{0}$; Kierstead [KiersteadDilworth]).

For every $k$, every partial order of width $\leq\\!k$ is $(5^{k}-1)/4$-chain
decomposable.

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}$ [HirstThesis]. There is also an
effective analog of Mirsky’s theorem in the spirit of Theorem 3.5
[KiersteadOrderedSets].

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

######  Definition 3.6 ($\mathsf{RCA}_{0}$).

  * •

$\mathsf{RSpo}^{\mathsf{CD}}_{k}$ is the statement “Every infinite $k$-chain
decomposable partial order has a $(0,\infty)$-homogeneous chain.”

  * •

$\mathsf{RSpo}^{\mathsf{CD}}_{<\infty}$ abbreviates $\forall
k\,\mathsf{RSpo}^{\mathsf{CD}}_{k}$.

  * •

$(0,\mathrm{cof})\mbox{-}\mathsf{RSpo}^{\mathsf{CD}}_{k}$ is the statement
“Every infinite $k$-chain decomposable partial order has a
$(0,\mathrm{cof})$-homogeneous chain.”

  * •

$(0,\mathrm{cof})\mbox{-}\mathsf{RSpo}^{\mathsf{CD}}_{<\infty}$ abbreviates
$\forall k\,(0,\mathrm{cof})\mbox{-}\mathsf{RSpo}^{\mathsf{CD}}_{k}$.

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})\mbox{-}\mathsf{RSpo}_{<\infty}\leftrightarrow(0,\mathrm{cof})\mbox{-}\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 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$.

######  Definition 3.7 ($\mathsf{RCA}_{0}$).

  * •

$\mathsf{CC}_{k}$ is the statement “Every infinite partial order of width
$\leq\\!k$ has an infinite chain.”

  * •

$\mathsf{CC}_{<\infty}$ abbreviates $\forall k\,\mathsf{CC}_{k}$.

  * •

$\mathsf{CA}_{k}$ is the statement “Every infinite partial order of height
$\leq\\!k$ has an infinite antichain.”

  * •

$\mathsf{CA}_{<\infty}$ abbreviates $\forall k\,\mathsf{CA}_{k}$.

######  Proposition 3.8.

  1. (1)

For each fixed standard $k$, $\mathsf{RCA}_{0}\vdash\mathsf{CC}_{k}$ and
$\mathsf{RCA}_{0}\vdash\mathsf{CA}_{k}$.

  2. (2)

$\mathsf{CC}_{<\infty}$, $\mathsf{CA}_{<\infty}$, and
$\mathsf{B}\Sigma^{0}_{2}$ are pairwise equivalent over $\mathsf{RCA}_{0}$.

###### Proof.

For $\mathsf{RCA}_{0}\vdash\mathsf{CC}_{k}$, let $(P,<_{P})$ be an infinite
partial order of width $\leq\\!k$. By Theorem 3.5, $P$ has a $5^{k}$-chain
decomposition, and at least one of these chains is infinite by
$\mathsf{RT}^{1}_{5^{k}}$. Thus $P$ has an infinite chain. The proof that
$\mathsf{RCA}_{0}+\mathsf{B}\Sigma^{0}_{2}\vdash\mathsf{CC}_{<\infty}$ is the
same, except we must use $\mathsf{RT}^{1}_{<\infty}$ instead of
$\mathsf{RT}^{1}_{5^{k}}$ because now $k$ is not fixed in advance.

For $\mathsf{RCA}_{0}\vdash\mathsf{CA}_{k}$, we give a direct proof instead of
appealing to an effective analog of Mirsky’s theorem. Let $(P,<_{P})$ be an
infinite partial order of height $\leq\\!k$. Define a coloring $c\colon
P\rightarrow k^{2}$ by $c(p)=\langle x,y\rangle$, where $x$ is the greatest
size of a $<_{P}$-chain in $\\{q<_{\mathbb{N}}p:q<_{P}p\\}$ and $y$ is the
greatest size of a $<_{P}$-chain in $\\{q<_{\mathbb{N}}p:p<_{P}q\\}$. Both $x$
and $y$ are less than $k$ because $P$ has height $\leq\\!k$. By
$\mathsf{RT}^{1}_{k^{2}}$, let $H\subseteq P$ be an infinite set that is
homogeneous for $c$. We claim that $H$ is an antichain. Suppose for a
contradiction that $a,b\in H$ and $a<_{P}b$. If $a<_{\mathbb{N}}b$ and
$q_{0}<_{P}q_{1}<_{P}\cdots<_{P}q_{n-1}$ is a chain in
$\\{q<_{\mathbb{N}}a:q<_{P}a\\}$, then
$q_{0}<_{P}q_{1}<_{P}\cdots<_{P}q_{n-1}<_{P}a$ is a chain in
$\\{q<_{\mathbb{N}}b:q<_{P}b\\}$. This means that if $x$ is the maximum size
of a chain in $\\{q<_{\mathbb{N}}a:q<_{P}a\\}$, then the maximum size of a
chain in $\\{q<_{\mathbb{N}}b:q<_{P}b\\}$ is at least $x+1$. So $c(a)\neq
c(b)$, contradicting that $H$ is homogeneous. Similar reasoning shows that if
$b<_{\mathbb{N}}a$, then $c(a)\neq c(b)$ as well. Therefore $H$ is an infinite
antichain in $P$. The proof that
$\mathsf{RCA}_{0}+\mathsf{B}\Sigma^{0}_{2}\vdash\mathsf{CA}_{<\infty}$ is the
same, except we must use $\mathsf{RT}^{1}_{<\infty}$ instead of
$\mathsf{RT}^{1}_{k^{2}}$ because now $k$ is not fixed in advance.

For $\mathsf{RCA}_{0}+\mathsf{CC}_{<\infty}\vdash\mathsf{B}\Sigma^{0}_{2}$,
let $c\colon\mathbb{N}\rightarrow k$ be a $k$-coloring, and define a partial
order $(P,<_{P})$ with $P=\mathbb{N}$ by setting $p<_{P}q$ if and only if
$p<_{\mathbb{N}}q$ and $c(p)=c(q)$. The partial order $P$ has width
$\leq\\!k$, so by $\mathsf{CC}_{<\infty}$ it has an infinite chain $H$. By the
definition of $<_{P}$, $H$ must be homogeneous for $c$. Therefore
$\mathsf{RT}^{1}_{<\infty}$ holds.

For $\mathsf{RCA}_{0}+\mathsf{CA}_{<\infty}\vdash\mathsf{B}\Sigma^{0}_{2}$,
let $c\colon\mathbb{N}\rightarrow k$ be a $k$-coloring, and define a partial
order $(P,<_{P})$ with $P=\mathbb{N}$ by setting $p<_{P}q$ if and only if
$c(p)<c(q)$. The partial order $P$ has height $\leq\\!k$, so by
$\mathsf{CA}_{<\infty}$ it has an infinite antichain $H$. By the definition of
$<_{P}$, $H$ must be homogeneous for $c$. Therefore
$\mathsf{RT}^{1}_{<\infty}$ holds. ∎

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.”

######  Proposition 3.9.

The following are equivalent over $\mathsf{RCA}_{0}$.

  1. (1)

$\mathsf{ADS}$.

  2. (2)

The statement “Every infinite partial order of finite width contains either an
infinite ascending sequence or an infinite descending sequence.”

  3. (3)

For each fixed standard $k\geq 1$, the statement “Every infinite partial order
of width $\leq\\!k$ contains either an infinite ascending sequence or an
infinite descending sequence.”

###### Proof.

For 1 $\Rightarrow$ 2, let $(P,<_{P})$ be an infinite partial order of width
$\leq\\!k$ for some $k$. Using the fact that
$\mathsf{RCA}_{0}+\mathsf{ADS}\vdash\mathsf{B}\Sigma^{0}_{2}$, we may appeal
to Proposition 3.8 item 2 and apply $\mathsf{CC}_{<\infty}$ to $P$ to obtain
an infinite chain $C$ in $P$. Now apply $\mathsf{ADS}$ to $C$ to obtain either
an infinite ascending sequence in $C$ or an infinite descending sequence in
$C$.

The implications 2 $\Rightarrow$ 3 and 3 $\Rightarrow$ 1 are immediate because
every partial order of width $\leq\\!k$ has finite width, and every infinite
linear order is an infinite partial order of width $1$. ∎

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

We give a proof of $\mathsf{RSpo}_{<\infty}$ in $\mathsf{ACA}_{0}$ and a proof
of $(0,\mathrm{cof})\mbox{-}\mathsf{RSpo}_{<\infty}$ in
$\Pi^{1}_{1}\mbox{-}\mathsf{CA}_{0}$. The proofs are not 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}$.

######  Definition 4.1 ($\mathsf{RCA}_{0}$).

Let $(P,<_{P})$ be a partial order, and let $X,Y\subseteq P$.

  * •

Write $X<_{P}Y$ if every element of $X$ is strictly below every element of
$Y$: $\forall x\in X\;\forall y\in Y\;(x<_{P}y)$. In the case of singletons,
write $x<_{P}Y$ and $X<_{P}y$ in place of $\\{x\\}<_{P}Y$ and $X<_{P}\\{y\\}$.

  * •

Write $X\leq_{\forall\exists}Y$ if every element of $X$ is below some element
of $Y$: $\forall x\in X\;\exists y\in Y\;(x\leq_{P}y)$.

  * •

Write $X\mid_{P}Y$ if every element of $X$ is incomparable with every element
of $Y$: $\forall x\in X\;\forall y\in Y\;(x\mid_{P}y)$. In the case of
singletons, write $x\mid_{P}Y$ in place of $\\{x\\}\mid_{P}Y$.

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})$.

######  Definition 4.2.

Let $(P,<_{P})$ be a partial order, and let $X\subseteq P$.

  * •

($\mathsf{ACA}_{0}$) Let $X{\downarrow}=\\{p\in P:\exists x\in
X\;(p\leq_{P}x)\\}$ and $X{\uparrow}=\\{p\in P:\exists x\in
X\;(p\geq_{P}x)\\}$ denote the downward and upward closures of $X$ in $P$,
respectively.

  * •

($\mathsf{RCA}_{0}$) In the case of singletons $X=\\{x\\}$, write
$x{\downarrow}$ and $x{\uparrow}$ in place of $\\{x\\}{\downarrow}$ and
$\\{x\\}{\uparrow}$. These sets may be formed in $\mathsf{RCA}_{0}$.

  * •

($\mathsf{RCA}_{0}$) Call $X$ _well-founded_ if it contains no infinite
descending sequence. Otherwise call $X$ _ill-founded_. Likewise, call $X$
_reverse well-founded_ if it contains no infinite ascending sequence.
Otherwise call $X$ _reverse ill-founded_.

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}$.

######  Definition 4.3 ($\mathsf{RCA}_{0}$).

Let $f\colon\mathbb{N}\rightarrow\mathbb{N}$ be an injection. An
$n\in\mathbb{N}$ is a _true number_ if $\forall k>n\;(f(n)<f(k))$, and
otherwise $n$ is a _false number_. Additionally, an $n\in\mathbb{N}$ is _true
at stage $m$_ if $\forall k\,(n<k\leq m\;\rightarrow\;f(n)<f(k))$, and
otherwise $n$ is _false at stage $m$_.

The idea of true numbers appears to have originated with Dekker [Dekker], 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 [MarconeShore,
FrittaionHendtlassMarconeShaferVanderMeeren, FrittaionMarcone] in the form of
the following well-known construction.

######  Construction 4.4 ($\mathsf{RCA}_{0}$).

Let $f\colon\mathbb{N}\to\mathbb{N}$ be an injection. Define a linear order
$(L,<_{L})$ where $L=\\{\ell_{n}:n\in\mathbb{N}\\}$ and for each $n<m$ the
following hold:

  1. (1)

$\ell_{n}<_{L}\ell_{m}$ if $f(k)<f(n)$ for some $k$ with $n<k\leq m$ (i.e.,
$n$ is false at stage $m$), and

  2. (2)

$\ell_{m}<_{L}\ell_{n}$ if $f(n)<f(k)$ for all $k$ with $n<k\leq m$ (i.e., $n$
is true at stage $m$).

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 [MarconeShore]*Lemma 4.2 and
[FrittaionMarcone]*Theorem 4.5.

######  Lemma 4.5.

The following are equivalent over $\mathsf{RCA}_{0}$.

  1. (1)

$\mathsf{ACA}_{0}$.

  2. (2)

For every partial order $(P,<_{P})$, if $P$ has no infinite antichain and no
suborder of type $\zeta$, then there is a set $W\subseteq P$ such that
$\forall p\in P\;(p\in W\;\leftrightarrow\;\textup{$p{\downarrow}$ is well-
founded})$.

  3. (3)

Every linear order $(L,<_{L})$ with no suborder of type $\zeta$ can be
partitioned as $L=W\cup R$, where

     * •

$W<_{L}R$,

     * •

$W$ is well-founded, and

     * •

$R$ is reverse well-founded.

###### 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

$\displaystyle(|\sigma|$ $\displaystyle>0\;\rightarrow\;\sigma(0)=p)$
$\displaystyle\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{)}.$

Let $W=\\{p\in P:\text{$T_{p}$ 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 partial 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}:\text{$n,m\in\mathbb{N}$ and $n$ is true at stage $m$}\\}$ (note
that if $m\leq n$, then $n$ is true at stage $m$), and define

$\displaystyle
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}).$

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.

######  Definition 4.6 ($\mathsf{RCA}_{0}$).

Let $(P,<_{P})$ be a partial order, and let $A=\langle
a_{n}:n\in\mathbb{N}\rangle$ be an ascending sequence in $P$. Then $A_{\geq
n_{0}}$ denotes the ascending sequence $\langle a_{n}:n\geq n_{0}\rangle$.
Sequences of the form $A_{\geq n_{0}}$ are called _tails_ of $A$.

######  Definition 4.7 ($\mathsf{RCA}_{0}$).

Let $(P,<_{P})$ be a partial order, and let $A=\langle
a_{n}:n\in\mathbb{N}\rangle$ be an infinite ascending sequence in $P$. A $p\in
P$ is called a _counterexample to $A$_ if there is an $n$ such that
$p>_{P}a_{n}$ and $p\mid_{P}A_{\geq n+1}$. An infinite ascending sequence
$B=\langle b_{\ell}:\ell\in\mathbb{N}\rangle$ is called a _counterexample
sequence for $A$_ if $B$ contains counterexamples to infinitely many tails of
$A$: $\forall m\;\exists
n>m\;\exists\ell\;(b_{\ell}>_{P}a_{n}\;\wedge\;b_{\ell}\mid_{P}A_{\geq n+1})$.

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.

######  Lemma 4.8 ($\mathsf{ACA}_{0}$).

Let $(P,<_{P})$ be an infinite partial order with $k$-chain decomposition
$C_{0},\dots,C_{k-1}$. Let $A=\langle a_{n}:n\in\mathbb{N}\rangle$ be an
infinite ascending sequence in $C_{i}$ for some $i<k$, and assume that no tail
of $A$ is $(0,\infty)$-homogeneous. Then there is an infinite ascending
sequence $B=\langle b_{n}:n\in\mathbb{N}\rangle$ in $C_{j}$ for some $j<k$
that is a counterexample sequence for $A$.

###### Proof.

We assume that no tail of $A$ is $(0,\infty)$-homogeneous, so every tail of
$A$ has a counterexample $p$. For each $n$, let $p_{n}$ be the $<$-least
counterexample to the tail $A_{\geq n}$. By $\mathsf{RT}^{1}_{<\infty}$, there
are a $j<k$ and an infinite $X\subseteq\mathbb{N}$ such that $p_{n}\in C_{j}$
for all $n\in X$. Now, for every $n\in X$, we have that $p_{n}<_{P}p_{m}$ for
all sufficiently large $m\in X$. To see this, let $n\in X$. As $p_{n}$ is a
counterexample to $A_{\geq n}$, there is an $s\geq n$ such that
$p_{n}>_{P}a_{s}$ and $p_{n}\mid_{P}A_{\geq s+1}$. Let $m\in X$ be such that
$m>s+1$, and consider $p_{m}$. The chain $C_{j}$ contains both $p_{n}$ and
$p_{m}$, so $p_{n}\between_{P}p_{m}$. As $p_{m}$ is a counterexample to
$A_{\geq m}$, there is a $t\geq m$ such that $p_{m}>_{P}a_{t}$. Thus we cannot
have have $p_{m}\leq_{P}p_{n}$ because this would yield
$a_{s+1}<_{P}a_{t}<_{P}p_{m}\leq_{P}p_{n}$, contradicting that
$p_{n}\mid_{P}a_{s+1}$. Note here that $s+1<m\leq t$, so $a_{s+1}<_{P}a_{t}$
because $A$ is an ascending sequence. Thus it must be that $p_{n}<_{P}p_{m}$.
We may then define the desired counterexample sequence $B$ as follows. Let
$n_{0}$ be the $<$-least element of $X$. Given $n_{\ell}$, let $n_{\ell+1}$ be
the $<$-least element of $X$ with $n_{\ell}<n_{\ell+1}$ and
$p_{n_{\ell}}<_{P}p_{n_{\ell+1}}$. Finally, take $b_{\ell}=p_{n_{\ell}}$ for
each $\ell$. ∎

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

######  Theorem 4.9.

$\mathsf{ACA}_{0}\vdash\mathsf{RSpo}_{<\infty}$.

###### 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

$\displaystyle
B_{h^{m+1}(0)}\leq_{\forall\exists}B_{h^{n}(0)}=B_{h^{m}(0)}\leq_{\forall\exists}A_{h^{m+1}(0)}$

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}\mbox{-}\mathsf{CA}_{0}$ because defining the set of reverse ill-
founded elements in a linear order requires
$\Pi^{1}_{1}\mbox{-}\mathsf{CA}_{0}$ in general, as shown in Theorem 8.3
below.

######  Theorem 4.10.

$\Pi^{1}_{1}\mbox{-}\mathsf{CA}_{0}\vdash(0,\mathrm{cof})\mbox{-}\mathsf{RSpo}_{<\infty}$.

###### Proof.

It suffices to show that
$\Pi^{1}_{1}\mbox{-}\mathsf{CA}_{0}\vdash(0,\mathrm{cof})\mbox{-}\mathsf{RSpo}^{\mathsf{CD}}_{<\infty}$
because $(0,\mathrm{cof})\mbox{-}\mathsf{RSpo}_{<\infty}$ and
$(0,\mathrm{cof})\mbox{-}\mathsf{RSpo}^{\mathsf{CD}}_{<\infty}$ are equivalent
as explained in Section 3.

Let $(P,<_{P})$ be an infinite partial order with $k$-chain decomposition
$C_{0},\dots,C_{k-1}$ for some $k$. Apply $\mathsf{RT}^{1}_{<\infty}$ to
conclude that $C_{i}$ is infinite for some $i<k$, and apply $\mathsf{ADS}$ to
$C_{i}$ to conclude that $C_{i}$ contains either an infinite ascending
sequence or an infinite descending sequence. By reversing the partial order if
necessary, we may assume that $C_{i}$ contains an infinite ascending sequence.
Assume for a contradiction that $P$ does not contain a
$(0,\infty)$-homogeneous chain of order-type $\omega$.

Use $\Pi^{1}_{1}\mbox{-}\mathsf{CA}_{0}$ (and the fact that the
$\Sigma^{1}_{1}$ sets are the complements of the $\Pi^{1}_{1}$ sets) to
simultaneously define for each $i<k$ the subset $W_{i}=\\{p\in
C_{i}:\text{$p{\uparrow}\cap C_{i}$ is reverse ill-founded}\\}$ of $C_{i}$
consisting of the elements of $C_{i}$ that have infinite ascending sequences
above them in $C_{i}$. At least one $W_{i}$ is non-empty because at least one
$C_{i}$ contains an infinite ascending sequence. Now proceed as in the proof
of Theorem 4.9, except notice that now the sets $W_{i}$ are not necessarily
well-founded. What matters is that $W_{i}$ has no maximum element and that
$C_{i}\setminus W_{i}$ is reverse well-founded for each $i<k$. Relabel the
chains $C_{0},\dots,C_{k-1}$ so that the non-empty $W_{i}$ are exactly
$W_{0},\dots,W_{u-1}$ for some $u$ with $0<u\leq k$. Each $W_{i}$ for $i<u$ is
non-empty and has no maximum element. Therefore, for each $i<u$ we can define
an infinite ascending sequence $A_{i}$ in $W_{i}$ that is cofinal in $W_{i}$.
No tail of $A_{i}$ is $(0,\infty)$-homogeneous for any $i<u$ by the assumption
that $P$ does not contain a $(0,\infty)$-homogeneous chain of order-type
$\omega$. As in the proof of Theorem 4.9, apply Lemma 4.8 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)}$. The sequence $B_{i}$ is contained in $W_{h(i)}$ for each
$i<u$ by the definition of $W_{h(i)}$. Thus $W_{h(i)}$ is infinite and
therefore $h(i)<u$ for each $i<u$. Therefore $h$ is a function $h\colon
u\rightarrow u$. As in the proof of Theorem 4.9, there are $m<n\leq u$ with
$h^{m}(0)=h^{n}(0)$, which yields that
$B_{h^{m+1}(0)}\leq_{\forall\exists}A_{h^{m+1}(0)}$, which contradicts that
$B_{h^{m+1}(0)}$ is a counterexample sequence for $A_{h^{m+1}(0)}$.
Ultimately, we contradicted the assumption that $P$ does not contain a
$(0,\infty)$-homogeneous chain of order-type $\omega$. Thus $P$ does contain a
$(0,\infty)$-homogeneous chain of order-type $\omega$, and such a chain is
necessarily $(0,\mathrm{cof})$-homogeneous. ∎

##  5\. Proofs of $\mathsf{RSpo}_{<\infty}$, $\mathsf{RSpo}_{k}$, and
$(0,\mathrm{cof})\mbox{-}\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})\mbox{-}\mathsf{RSpo}_{2}$
(Theorem 5.11).

To do this, we weaken the notion of a counterexample sequence from Definition
4.7 to that of a _ladder_.

######  Definition 5.1 ($\mathsf{RCA}_{0}$).

Let $(P,<_{P})$ be a partial order, and let $S=\langle
s_{n}:n\in\mathbb{N}\rangle$ be an infinite sequence in $P$. An infinite
ascending sequence $A=\langle a_{n}:n\in\mathbb{N}\rangle$ is called a _ladder
for $S$_ if $\forall n\,(s_{n}\leq_{P}a_{n})$.

In Definition 5.1, the sequence $S$ is not required to be ascending, but in
practice it usually will be. Notice also that if $A$ is an infinite ascending
sequence in a partial order $(P,<_{P})$, then $A$ is a ladder of itself.
However, the typical situation is that $P$ has been decomposed into $k$ chains
as $P=C_{0}\cup\cdots\cup C_{k-1}$, we have an infinite ascending sequence $A$
contained in some chain $C_{j}$, and we want to find a ladder $B$ for $A$ in
some chain $C_{i}$ with $i\neq j$. Lemma 5.3, which may be thought of as a
weaker but effective version of Lemma 4.8, shows how to convert an algorithm
computing $A$ into an algorithm computing such a ladder $B$, provided 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}$.

######  Lemma 5.2 ($\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

$\displaystyle\forall m\;\exists n\;\exists p\in
C_{i}\;(p\geq_{P}a_{m}\;\wedge\;p\mid_{P}a_{n}).$

###### 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

$\displaystyle\forall m\;\exists n\;\exists p\in
P\;(p\geq_{P}a_{m}\;\wedge\;p\mid_{P}a_{n}).$

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. ∎

For a partial order $(P,<_{P})$ and an oracle $X$, say that $\Phi_{e}^{X}$
_computes an infinite sequence in $P$_ if $\Phi_{e}^{X}(n){\downarrow}$ and
$\Phi_{e}^{X}(n)\in P$ for every $n$. Say that $\Phi_{e}^{X}$ _computes an
infinite ascending sequence in $P$_ if additionally
$\Phi_{e}^{X}(n)<_{P}\Phi_{e}^{X}(n+1)$ for every $n$.

######  Lemma 5.3 ($\mathsf{RCA}_{0}$).

Let $(P,<_{P})$ be a partial order with $k$-chain decomposition
$C_{0},\dots,C_{k-1}$. Let $\vec{P}$ denote $\vec{P}=P\oplus{<_{P}}\oplus
C_{0}\oplus\cdots\oplus C_{k-1}$. Then there is a recursive function
$f\colon\mathbb{N}\times\mathbb{N}\rightarrow\mathbb{N}$ with the following
properties for all $e$, all $i<k$, and all $X$.

  1. (1)

If $\Phi_{e}^{\vec{P}\oplus X}$ computes an infinite sequence in $P$ and

$\displaystyle\forall m\;\exists n\;\exists p\in
C_{i}\;\left(p\geq_{P}\Phi_{e}^{\vec{P}\oplus
X}(m)\;\wedge\;p\mid_{P}\Phi_{e}^{\vec{P}\oplus X}(n)\right),$

then $\Phi_{f(e,i)}^{\vec{P}\oplus X}$ is total.

  2. (2)

If $\Phi_{f(e,i)}^{\vec{P}\oplus X}$ is total, then $\Phi_{e}^{\vec{P}\oplus
X}$ is total, $\Phi_{e}^{\vec{P}\oplus X}$ computes an infinite sequence in
$P$, and $\Phi_{f(e,i)}^{\vec{P}\oplus X}$ computes a ladder for
$\Phi_{e}^{\vec{P}\oplus X}$ in $C_{i}$.

###### Proof.

If $i\geq k$, then set $f(e,i)=0$. If $i<k$, then compute $f(e,i)$ by
generating an index $f(e,i)=\widehat{e}$ for a machine $\Phi_{\widehat{e}}$
that operates as follows. To compute $\Phi_{\widehat{e}}^{\vec{P}\oplus
X}(0)$, search for an $n$ and a $p_{0}\in C_{i}$ with
$p_{0}\geq_{P}\Phi_{e}^{\vec{P}\oplus X}(0)$ and
$p_{0}\mid_{P}\Phi_{e}^{\vec{P}\oplus X}(n)$. If $p_{0}$ is found, then output
$\Phi_{\widehat{e}}^{\vec{P}\oplus X}(0)=p_{0}$. To compute
$\Phi_{\widehat{e}}^{\vec{P}\oplus X}(m+1)$, first compute
$p_{m}=\Phi_{\widehat{e}}^{\vec{P}\oplus X}(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}\Phi_{e}^{\vec{P}\oplus X}(m+1)$, and
$p_{m+1}\mid_{P}\Phi_{e}^{\vec{P}\oplus X}(n)$. If $p_{m+1}$ is found, then
output $\Phi_{\widehat{e}}^{\vec{P}\oplus X}(m+1)=p_{m+1}$.

Item 2 follows immediately from the definition of $\widehat{e}$. If $i<k$ and
$\Phi_{\widehat{e}}^{\vec{P}\oplus X}$ is total, then it must be that
$\Phi_{e}^{\vec{P}\oplus X}(m){\downarrow}\in P$, that
$\Phi_{e}^{\vec{P}\oplus X}(m)\leq_{P}\Phi_{\widehat{e}}^{\vec{P}\oplus
X}(m)$, and that $\Phi_{\widehat{e}}^{\vec{P}\oplus
X}(m)<_{P}\Phi_{\widehat{e}}^{\vec{P}\oplus X}(m+1)$ for every $m$.

For item 1, let $i<k$, suppose that $\Phi_{e}^{\vec{P}\oplus X}$ computes an
infinite sequence in $P$, and suppose that for every $m$ there are an $n$ and
a $p\in C_{i}$ with $p\geq_{P}\Phi_{e}^{\vec{P}\oplus X}(m)$ and
$p\mid_{P}\Phi_{e}^{\vec{P}\oplus X}(n)$. We use $\mathsf{I}\Sigma^{0}_{1}$ to
show that $\Phi_{\widehat{e}}^{\vec{P}\oplus X}$ is total. By assumption,
there are an $n$ and a $p_{0}\in C_{i}$ with
$p_{0}\geq_{P}\Phi_{e}^{\vec{P}\oplus X}(0)$ and
$p_{0}\mid_{P}\Phi_{e}^{\vec{P}\oplus X}(n)$. Thus
$\Phi_{\widehat{e}}^{\vec{P}\oplus X}(0){\downarrow}$. Inductively assume that
$\Phi_{\widehat{e}}^{\vec{P}\oplus X}(m){\downarrow}=p_{m}$. Then there is an
$\ell$ such that $p_{m}\mid_{P}\Phi_{e}^{\vec{P}\oplus X}(\ell)$. By
assumption, there are an $s$ and a $p\in C_{i}$ with

$\displaystyle p\geq_{P}\Phi_{e}^{\vec{P}\oplus X}(m+1)\quad\text{and}\quad
p\mid_{P}\Phi_{e}^{\vec{P}\oplus X}(s)$

and also a $t$ and a $q\in C_{i}$ with

$\displaystyle q\geq_{P}\Phi_{e}^{\vec{P}\oplus X}(\ell)\quad\text{and}\quad
q\mid_{P}\Phi_{e}^{\vec{P}\oplus X}(t).$

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

$\displaystyle p_{m+1}\geq_{P}\Phi_{e}^{\vec{P}\oplus
X}(m+1)\quad\text{and}\quad p_{m+1}\geq_{P}\Phi_{e}^{\vec{P}\oplus
X}(\ell)\quad\text{and}\quad p_{m+1}\mid_{P}\Phi_{e}^{\vec{P}\oplus X}(n).$

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

$\displaystyle\Phi_{e}^{\vec{P}\oplus X}(\ell)\leq_{P}p_{m+1}\leq_{P}p_{m},$

contradicting that $p_{m}\mid_{P}\Phi_{e}^{\vec{P}\oplus X}(\ell)$. Thus
$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}\Phi_{e}^{\vec{P}\oplus X}(m+1)$, and
$p_{m+1}\mid_{P}\Phi_{e}^{\vec{P}\oplus X}(n)$. So
$\Phi_{\widehat{e}}^{\vec{P}\oplus X}(m+1){\downarrow}$. ∎

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.)

######  Lemma 5.4 ($\mathsf{RCA}_{0}$).

Let $k\geq 2$, and let $T$ be a finite rooted tree with the following
properties.

  * •

$T$ has height $k$.

  * •

Every leaf of $T$ is at level $k$.

  * •

The vertices of $T$ are labeled by a function $\ell\colon T\rightarrow k$ in
such a way that if $\sigma\in T$ is not a leaf and $\tau_{0},\dots,\tau_{n-1}$
are the children of $\sigma$, then $\ell(\tau_{0}),\dots,\ell(\tau_{n-1})$ are
distinct elements of $k\setminus\\{\ell(\sigma)\\}$.

Then there is a $\sigma\in T$ that is not a leaf such that for every child
$\tau$ of $\sigma$ there is an $\eta\succ\tau$ with $\ell(\eta)=\ell(\sigma)$.

###### Proof.

Proceed by $\Pi^{0}_{1}$ induction on $k\geq 2$. For the base case $k=2$, the
only possibility for $T$ is a path of length $2$ consisting of a root $r$,
$r$’s child $\tau$, and $\tau$’s child $\eta$, where $\ell(r)\neq\ell(\tau)$
and $\ell(\tau)\neq\ell(\eta)$. As $k=2$, it must be that
$\ell(r)=\ell(\eta)$, so we may take $\sigma=r$.

Now suppose that the lemma holds for $k$. Consider a tree $T$ of height $k+1$,
where every leaf is at level $k+1$, and consider also a labeling $\ell\colon
T\rightarrow k+1$ that labels $T$ according to the hypothesis of the lemma.
Let $r$ be the root, and let $\tau_{0},\dots,\tau_{n-1}$ be $r$’s children. If
for every $\tau_{i}$ there is an $\eta\succ\tau_{i}$ with
$\ell(\eta)=\ell(r)$, then we may take $\sigma=r$. Otherwise, there is a
$\tau_{i}$ such that no $\eta\succ\tau_{i}$ has $\ell(\eta)=\ell(r)$. Let
$S=\\{\eta\in T:\eta\succeq\tau_{i}\\}$ be the complete subtree of $T$ above
$\tau_{i}$ rooted at $\tau_{i}$. Then $S$ has height $k$, and every leaf of
$S$ is at level $k$ of $S$. Moreover, $S$ is labeled by $\ell$, which only
uses labels from the set $(k+1)\setminus\\{\ell(r)\\}$. Fix a bijection
$f\colon(k+1)\setminus\\{\ell(r)\\}\rightarrow k$, and define a labeling
$\widehat{\ell}\colon S\rightarrow k$ by $\widehat{\ell}=f\circ\ell$. By the
induction hypothesis applied to $S$ and $\widehat{\ell}$, there is a
$\sigma\in S$ that is not a leaf such that for every child $\tau$ of $\sigma$
in $S$ there is an $\eta\succ\tau$ in $S$ with
$\widehat{\ell}(\eta)=\widehat{\ell}(\sigma)$. This $\sigma$ also satisfies
the conclusion of the lemma for $T$ because $S$ is the complete subtree of $T$
above $\tau_{i}$: for every child $\tau$ of $\sigma$ in $T$, there is an
$\eta\succ\tau$ in $T$ with $\widehat{\ell}(\eta)=\widehat{\ell}(\sigma)$ and
hence with $\ell(\eta)=\ell(\sigma)$. ∎

######  Theorem 5.5.

$\mathsf{RCA}_{0}+\mathsf{I}\Sigma^{0}_{2}+\mathsf{ADS}\vdash\mathsf{RSpo}_{<\infty}$.

###### 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
$f\colon\mathbb{N}\times\mathbb{N}\rightarrow\mathbb{N}$ be the recursive
function of Lemma 5.3. Let $R=(k-1)^{\leq k}$ be the complete $(k-1)$-ary tree
of height $k$. Assign to each $\sigma\in R$ a machine $e(\sigma)$ and label
$\ell(\sigma)\in\\{0,\dots,k-1\\}$. For the root $r\in R$, let $e(r)$ be such
that $\Phi_{e(r)}^{\vec{P}\oplus A}(n)=a_{n}$ for each $n$, so that
$\Phi_{e(r)}^{\vec{P}\oplus A}$ computes the infinite ascending sequence $A$
in $C_{0}$, and label the root with $\ell(r)=0$. Suppose that $\sigma\in R$ is
not a leaf and that $e(\sigma)$ and $\ell(\sigma)$ have been defined. Index
the $k-1$ children of $\sigma$ as $\langle\tau_{i}:i\in
k\setminus\\{\ell(\sigma)\\}\rangle$. Then define $e(\tau_{i})=f(e(\sigma),i)$
and $\ell(\tau_{i})=i$ for each $i\in k\setminus\\{\ell(\sigma)\\}$. Using
$\mathsf{I}\Sigma^{0}_{2}$ in the form of bounded $\Pi^{0}_{2}$ comprehension,
let $T\subseteq R$ be the subtree $\bigl{\\{}\sigma\in
R:\forall\tau\preceq\sigma\;\bigl{(}\text{$\Phi_{e(\tau)}^{\vec{P}\oplus A}$
is total}\bigr{)}\bigr{\\}}$. Notice that if $\sigma$ is in $T$, then
$\Phi_{e(\sigma)}^{\vec{P}\oplus A}$ computes an infinite ascending sequence
in $C_{\ell(\sigma)}$.

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$. We have that $\Phi_{e(\sigma)}^{\vec{P}\oplus A}$ computes an
infinite ascending sequence in $C_{\ell(\sigma)}$. If no tail of this sequence
is $(0,\infty)$-homogeneous, then by Lemma 5.2 there is an $i<k$ such that

$\displaystyle\forall m\;\exists n\;\exists p\in
C_{i}\;\left(p\geq_{P}\Phi_{e(\sigma)}^{\vec{P}\oplus
A}(m)\;\wedge\;p\mid_{P}\Phi_{e(\sigma)}^{\vec{P}\oplus A}(n)\right).$

It cannot be that $i=\ell(\sigma)$, thus there must be such an $i\in
k\setminus\\{\ell(\sigma)\\}$. Thus $\Phi_{e(\tau_{i})}^{\vec{P}\oplus A}$ is
total by Lemma 5.3 because $e(\tau_{i})=f(e(\sigma),i)$. So $\tau_{i}\in T$,
contradicting that $\sigma$ is a leaf of $T$. Therefore some tail of the
sequence computed by $\Phi_{e(\sigma)}^{\vec{P}\oplus A}$ 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)$. Let $X=\langle x_{n}:n\in\mathbb{N}\rangle$
be the infinite ascending sequence in $C_{\ell(\sigma)}$ that is computed by
$\Phi_{e(\sigma)}^{\vec{P}\oplus A}$: $x_{n}=\Phi_{e(\sigma)}^{\vec{P}\oplus
A}(n)$ for all $n$. Each $\Phi_{e(\eta_{\tau})}^{\vec{P}\oplus A}$ also
computes an infinite ascending sequence in $C_{\ell(\sigma)}$. Define the
infinite sequence $Y=\langle y_{n}:n\in\mathbb{N}\rangle$ by setting

$\displaystyle
y_{n}=\textstyle{\max_{<_{P}}}\left\\{\Phi_{e(\eta_{\tau})}^{\vec{P}\oplus
A}(n):\text{$\tau$ is a child of $\sigma$ in $T$}\right\\}$

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
$\Phi_{e(\eta_{\tau})}^{\vec{P}\oplus 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 $\Phi_{e(\sigma)}^{\vec{P}\oplus A}$ computes the infinite
ascending sequence $X$ and that $\Phi_{e(\tau)}^{\vec{P}\oplus A}$ is total,
so $\Phi_{e(\tau)}^{\vec{P}\oplus 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 $\Phi_{e(\tau)}^{\vec{P}\oplus 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$,
$\Phi_{e(\alpha_{i})}^{\vec{P}\oplus A}$ is total because $\alpha_{i}\in T$.
Thus $\Phi_{e(\alpha_{i+1})}^{\vec{P}\oplus A}$ computes a ladder for the
sequence computed by $\Phi_{e(\alpha_{i})}^{\vec{P}\oplus A}$ for each
$i<m-1$. Therefore

$\displaystyle p\leq_{P}\Phi_{e(\tau)}^{\vec{P}\oplus
A}(n)\leq_{P}\Phi_{e(\alpha_{1})}^{\vec{P}\oplus
A}(n)\leq_{P}\cdots\leq_{P}\Phi_{e(\alpha_{m-2})}^{\vec{P}\oplus
A}(n)\leq_{P}\Phi_{e(\eta_{\tau})}^{\vec{P}\oplus A}(n)\leq_{P}y_{n}.$

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):\text{$\tau$ is a child
of $\sigma$ 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

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

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 $\Phi_{e(\sigma)}^{\vec{P}\oplus
A}$ computes the ascending sequence $X$, so $\Phi_{e(\tau)}^{\vec{P}\oplus
A}=\Phi_{f(e(\sigma),i)}^{\vec{P}\oplus A}$ must not be total because
otherwise $\tau$ would be in $T$. Therefore by Lemma 5.3,

$\displaystyle\exists m\;\forall n\;\forall p\in
C_{i}\;\bigl{(}p\ngeq_{P}x_{m}\;\vee\;p\between_{P}x_{n}\bigr{)}.$

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}\;\left(p\ngeq_{P}x_{m}\;\vee\;p\between_{P}x_{n}\right)$. 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}$. 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):\text{$\tau$ is a child of $\sigma$ 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 $i\in
k\setminus\bigl{(}\\{\ell(\sigma)\\}\cup\\{\ell(\tau):\text{$\tau$ is a child
of $\sigma$ 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$. ∎

######  Theorem 5.6.

For each fixed standard $k$,
$\mathsf{RCA}_{0}+\mathsf{ADS}\vdash\mathsf{RSpo}_{k}$.

###### Proof.

The proof is essentially the same as that of Theorem 5.5. In the proof of
Theorem 5.5, the sole use of $\mathsf{I}\Sigma^{0}_{2}$ is the application of
bounded $\Pi^{0}_{2}$ comprehension to form the subtree $T=\bigl{\\{}\sigma\in
R:\forall\tau\preceq\sigma\;\bigl{(}\text{$\Phi_{e(\sigma)}^{\vec{P}\oplus A}$
is total}\bigr{)}\bigr{\\}}$ of the tree $R=(k-1)^{\leq k}$. In the case where
$k$ is fixed and standard, $R$ and its elements have fixed standard codes, so
we may instead form $T$ by a giant case analysis, using excluded middle for
the predicates $\bigl{(}\text{$\Phi_{e(\sigma)}^{\vec{P}\oplus A}$ is
total}\bigr{)}\;\vee\;\bigl{(}\text{$\Phi_{e(\sigma)}^{\vec{P}\oplus A}$ is
not total}\bigr{)}$ for the $\sigma\in R$. The proof then continues exactly as
in that of Theorem 5.5. The proof of Theorem 5.5 does make use of
$\mathsf{B}\Sigma^{0}_{2}$ in addition to the aforementioned use of
$\mathsf{I}\Sigma^{0}_{2}$, but the relevant instances of
$\mathsf{B}\Sigma^{0}_{2}$ are provable in $\mathsf{RCA}_{0}$ when $k$ is
fixed and standard (plus $\mathsf{B}\Sigma^{0}_{2}$ is available here anyway
because $\mathsf{RCA}_{0}+\mathsf{ADS}\vdash\mathsf{B}\Sigma^{0}_{2}$ as
explained in Section 2). ∎

Before continuing, we remark that the explicit use of machines in this
section’s proofs is not essential. In the proof of Theorem 5.5, for example,
one could instead define a partial function $g\colon
R\times\mathbb{N}\rightarrow P$, where for each $\sigma\in R$, the function
$g(\sigma,\cdot)$ plays the role of machine $\Phi_{e(\sigma)}^{\vec{P}\oplus
A}$. One then takes $T=\\{\sigma\in
R:\forall\tau\preceq\sigma\;(\text{$g(\tau,\cdot)$ is total})\\}$. However,
defining $g$ is fairly delicate, and we feel that the proof using machines is
more modular and easier to present.

When working under the assumption that the partial order $(P,<_{P})$ contains
an infinite ascending sequence, the proof of Theorem 5.5 produces either a
chain of order-type $\omega$ (when taking $B=\widehat{X}_{\geq m})$ or a chain
of order-type $\omega+\omega$ (when taking $B=\widehat{X}_{\geq
m}\cup\widehat{Y}_{\geq n}$). Therefore,
$\mathsf{RCA}_{0}+\mathsf{I}\Sigma^{0}_{2}+\mathsf{ADS}$ in fact proves that
every infinite partial order of finite width contains a
$(0,\infty)$-homogeneous chain of order-type $\omega$, $\omega+\omega$,
$\omega^{*}$, or $\omega^{*}+\omega^{*}$. Likewise, for each fixed standard
$k$, $\mathsf{RCA}_{0}+\mathsf{ADS}$ proves that every infinite partial order
of width $\leq\\!k$ contains a $(0,\infty)$-homogeneous chain of order-type
$\omega$, $\omega+\omega$, $\omega^{*}$, or $\omega^{*}+\omega^{*}$.

In the particular case of $\mathsf{RSpo}^{\mathsf{CD}}_{2}$, we may weaken
$\mathsf{ADS}$ to $\mathsf{SADS}$ and show that
$\mathsf{RCA}_{0}+\mathsf{SADS}\vdash\mathsf{RSpo}^{\mathsf{CD}}_{2}$. To do
this, we make use of a strict version of $\mathsf{SRT}^{2}_{k}$ where we
assume not only that the coloring $c\colon[\mathbb{N}]^{2}\rightarrow k$ is
stable, but that there is a fixed bound $n$ such that for every $x$ there are
at most $n$ many $y>x$ where $c(x,y)\neq c(x,y+1)$.

######  Definition 5.7 ($\mathsf{RCA}_{0}$).

  * •

A $k$-coloring of pairs $c\colon[\mathbb{N}]^{2}\rightarrow k$ is _$n$
-stable_ if, for every $x$, $|\\{y>x:c(x,y)\neq c(x,y+1)\\}|\leq n$.

  * •

${n}\mbox{-}\mathrm{stable~{}}\mathsf{SRT}^{2}_{k}$ is the restriction of
$\mathsf{RT}^{2}_{k}$ to $n$-stable $k$-colorings of pairs $c$.

  * •

${n}\mbox{-}\mathrm{stable~{}}\mathsf{SRT}^{2}_{<\infty}$ denotes $\forall
k\,({n}\mbox{-}\mathrm{stable~{}}\mathsf{SRT}^{2}_{k})$.

######  Proposition 5.8.

  1. (1)

For each fixed standard $n$ and $k$,
$\mathsf{RCA}_{0}\vdash{n}\mbox{-}\mathrm{stable~{}}\mathsf{SRT}^{2}_{k}$.

  2. (2)

For each fixed standard $n$, $\mathsf{B}\Sigma^{0}_{2}$ and
${n}\mbox{-}\mathrm{stable~{}}\mathsf{SRT}^{2}_{<\infty}$ are equivalent over
$\mathsf{RCA}_{0}$.

  3. (3)

$\mathsf{I}\Sigma^{0}_{2}$ and $\forall
n\,({n}\mbox{-}\mathrm{stable~{}}\mathsf{SRT}^{2}_{<\infty})$ are equivalent
over $\mathsf{RCA}_{0}$.

###### Proof.

For item 1, let $c\colon[\mathbb{N}]^{2}\rightarrow k$ be an $n$-stable
$k$-coloring of pairs. Let $\varphi(x,i,c)$ be the $\Sigma^{0}_{1}$ formula
expressing that there is a sequence $x<y_{0}<y_{1}<\dots<y_{i-1}$ where
$\forall j<i\;(c(x,y_{j})\neq c(x,y_{j}+1))$. Note that $\varphi(x,0,c)$ holds
for every $x$. By repeated applications of excluded middle, there is a maximum
$i\leq n$ such that $\varphi(x,i,c)$ holds for infinitely many $x$. By the
maximality of $i$, there is a bound $b$ such that if $x>b$ and $j>i$, then
$\neg\varphi(x,j,c)$. $\mathsf{RCA}_{0}$ suffices to formalize the well-known
fact that every infinite recursively enumerable set contains an infinite
recursive subset. That is, for every $\Sigma^{0}_{1}$ formula $\psi(x)$
(possibly with parameters), $\mathsf{RCA}_{0}$ proves that if $\psi(x)$ holds
for infinitely many $x$, then there is an infinite set $X$ such that $\forall
x\,(x\in X\rightarrow\psi(x))$. Applying this to the $\Sigma^{0}_{1}$ formula
$(x>b)\wedge\varphi(x,i,c)$, we obtain an infinite set $X$ such that $\forall
x\,(x\in X\;\rightarrow\;(x>b)\wedge\varphi(x,i,c))$. Then for every $x\in X$,
there are exactly $i$ many elements $y>x$ with $c(x,y)\neq c(x,y+1)$. So for
every $x\in X$, there is a unique sequence $x<y_{0}^{x}<\cdots<y_{i-1}^{x}$
where $\forall j<i\;(c(x,y_{j}^{x})\neq c(x,y_{j}^{x}+1))$. It follows that
$c(x,y)=c(x,y_{i-1}^{x}+1)$ for all $x\in X$ and $y>y_{i-1}^{x}$. Define a
$k$-coloring of singletons $f\colon X\rightarrow k$ by
$f(x)=c(x,y_{i-1}^{x}+1)$. Apply $\mathsf{RT}^{1}_{k}$ to $f$ to obtain a set
$G\subseteq X$ that is homogeneous for $f$ for some color $\ell<k$. Now define
an infinite set $H=\\{x_{s}:s\in\mathbb{N}\\}\subseteq G$ with
$x_{0}<x_{1}<x_{2}<\cdots$ by letting each $x_{s}$ be the least element of $G$
with
$x_{s}\geq\max\\{y_{i-1}^{x_{0}},y_{i-1}^{x_{1}},\dots,y_{i-1}^{x_{s-1}}\\}+1$.
Then $H$ is homogeneous for $c$. If $s<t$, then $x_{t}\geq y_{i-1}^{x_{s}}+1$,
so $c(x_{s},x_{t})=c(x_{s},y_{i-1}^{x_{s}}+1)=f(x_{s})=\ell$.

For the forward direction of item 2, we may use the same proof as for item 1,
except now $k$ is arbitrary so we must use $\mathsf{RT}^{1}_{<\infty}$ in
place of $\mathsf{RT}^{1}_{k}$. For the reversal, it is easy to see that
$\mathsf{RCA}_{0}+{0}\mbox{-}\mathrm{stable~{}}\mathsf{SRT}^{2}_{<\infty}\vdash\mathsf{RT}^{1}_{<\infty}$.
Let $f\colon\mathbb{N}\rightarrow k$ be a $k$-coloring of singletons for some
$k$, and define $c\colon[\mathbb{N}]^{2}\rightarrow k$ by $c(x,y)=f(x)$. Then
$c$ is a $0$-stable $k$-coloring of pairs, and every $H$ that is homogeneous
for $c$ is also homogeneous for $f$.

For the forward direction of item 3, we may use the same proof as for item 2,
except now $n$ is also arbitrary, so we must use $\mathsf{I}\Sigma^{0}_{2}$ in
the form of the $\Pi^{0}_{2}$ least element principle (see Section 2) to
obtain $i$. To do this, apply the $\Pi^{0}_{2}$ least element principle to
obtain the least $j$ such that $\forall s\;\exists x>s\;\varphi(x,n-j,c)$.
Then $i=n-j$ is the greatest $i\leq n$ such that $\varphi(x,i,c)$ holds for
infinitely many $x$. For the reversal, we show that $\mathsf{RCA}_{0}+\forall
n\,({n}\mbox{-}\mathrm{stable~{}}\mathsf{SRT}^{2}_{<\infty})$ proves the
$\Pi^{0}_{2}$ least element principle. Let $\forall x\,\exists y\,\psi(m,x,y)$
be a $\Pi^{0}_{2}$ formula, possibly with undisplayed parameters, where $\psi$
is $\Sigma^{0}_{0}$. Let $k$ be such that $\forall x\,\exists y\,\psi(k,x,y)$.
We want to find the least $i$ such that $\forall x\,\exists y\,\psi(i,x,y)$.
Define a $(k+2)$-coloring of pairs $c\colon[\mathbb{N}]^{2}\rightarrow k+2$ by

$\displaystyle c(s,t)=\begin{cases}i&\text{if $i\leq k$ is least such that
$\forall x\leq s\;\exists y\leq t\;\psi(i,x,y)$}\\\ k+1&\text{if $\forall
i\leq k\;\exists x\leq s\;\forall y\leq t\;\neg\psi(i,x,y)$.}\end{cases}$

The coloring $c$ is $(k+2)$-stable because, for fixed $s$, if $s<t_{0}<t_{1}$,
then $c(s,t_{0})\geq c(s,t_{1})$. By $\forall
n\,({n}\mbox{-}\mathrm{stable~{}}\mathsf{SRT}^{2}_{<\infty})$, let $H$ be a
set that is homogeneous for $c$ with color $i$. Then $i$ is least such that
$\forall x\,\exists y\,\psi(i,x,y)$. To see this, we first show that if $j\leq
k$ and $\forall x\,\exists y\,\psi(j,x,y)$, then $i\leq j$. Let $s\in H$, and,
by $\mathsf{B}\Sigma^{0}_{0}$ and the assumption $\forall x\,\exists
y\,\psi(j,x,y)$, let $t\in H$ be large enough so that $t>s$ and $\forall x\leq
s\;\exists y\leq t\;\psi(j,x,y)$. Then $i=c(s,t)\leq j$, so $i\leq j$. It
follows that $i\leq k$ by the assumption $\forall x\,\exists y\,\psi(k,x,y)$.
Now we show that $\forall x\,\exists y\,\psi(i,x,y)$. Consider any $x_{0}$,
and let $s,t\in H$ be such that $x_{0}<s<t$. Then $c(s,t)=i$ and $i\leq k$, so
$i$ is least such that $\forall x\leq s\;\exists y\leq t\;\psi(i,x,y)$. In
particular, $\exists y\,\psi(i,x_{0},y)$ because $x_{0}<s$. Therefore $\forall
x\,\exists y\,\psi(i,x,y)$. Thus $i$ is least such that $\forall x\,\exists
y\,\psi(i,x,y)$. ∎

Our proof of $\mathsf{RSpo}^{\mathsf{CD}}_{2}$ in
$\mathsf{RCA}_{0}+\mathsf{SADS}$ only uses the principle
${2}\mbox{-}\mathrm{stable~{}}\mathsf{SRT}^{2}_{3}$ from Proposition 5.8 item
1. We include items 2 and 3 for completeness. For fixed standard $k\geq 2$,
one might also consider the principle $\forall
n\,({n}\mbox{-}\mathrm{stable~{}}\mathsf{SRT}^{2}_{k})$. That
$\mathsf{RCA}_{0}+\mathsf{I}\Sigma^{0}_{2}\vdash\forall
n\,({n}\mbox{-}\mathrm{stable~{}}\mathsf{SRT}^{2}_{k})$ follows from
Proposition 5.8 item 3, but there cannot be a reversal because
$\mathsf{RCA}_{0}+\mathsf{SRT}^{2}_{k}\vdash\forall
n\,({n}\mbox{-}\mathrm{stable~{}}\mathsf{SRT}^{2}_{k})$, but
$\mathsf{RCA}_{0}+\mathsf{SRT}^{2}_{k}\nvdash\mathsf{I}\Sigma^{0}_{2}$ (see
Section 2). We did not determine if
$\mathsf{RCA}_{0}+\mathsf{B}\Sigma^{0}_{2}\vdash\forall
n\,({n}\mbox{-}\mathrm{stable~{}}\mathsf{SRT}^{2}_{k})$.

######  Theorem 5.9.

$\mathsf{RCA}_{0}+\mathsf{SADS}\vdash\mathsf{RSpo}^{\mathsf{CD}}_{2}$.

###### Proof.

By inspecting the proofs of Theorems 5.5 and 5.6, we see that the only use of
$\mathsf{ADS}$ is to produce either an infinite ascending sequence or an
infinite descending sequence in the partial order. That is, $\mathsf{RCA}_{0}$
proves the following for each fixed standard $k$.

  * $(\star)$

Let $(P,<_{P})$ be an infinite $k$-chain decomposable partial order that
contains either an infinite ascending sequence or an infinite descending
sequence. Then $P$ contains a $(0,\infty)$-homogeneous chain.

Let $(P,<_{P})$ be an infinite partial order with $2$-chain decomposition
$C_{0},C_{1}$. The plan of the proof is to either produce a
$(0,\infty)$-homogeneous chain outright or to apply $\mathsf{SADS}$ to obtain
an infinite ascending sequence or an infinite descending sequence in $P$, in
which case we may produce a $(0,\infty)$-homogeneous chain in $P$ by applying
$(\star)$. Notice that we may make free use of $\mathsf{B}\Sigma^{0}_{2}$
because $\mathsf{RCA}_{0}+\mathsf{SADS}\vdash\mathsf{B}\Sigma^{0}_{2}$ as
explained in Section 2.

The partial order $P$ is infinite, so at least one of $C_{0}$ and $C_{1}$ is
infinite. Assume that $C_{0}$ is infinite for the sake of argument.

######  Claim 1.

Suppose that there are an infinite $D_{0}\subseteq C_{0}$ and a finite
$D_{1}\subseteq C_{1}$ such that $D_{0}\mid_{P}(C_{1}\setminus D_{1})$. Then
$P$ contains a $(0,\infty)$-homogeneous chain.

###### Proof of Claim.

Suppose that $D_{1}=\\{q_{0},\dots,q_{n-1}\\}$, and define a $2^{n}$-coloring
$f\colon D_{0}\rightarrow 2^{n}$ by $f(p)=\langle b_{0},\dots,b_{n-1}\rangle$,
where, for each $i<n$, $b_{i}=0$ if $p\mid_{P}q_{i}$ and $b_{i}=1$ if
$p\between_{P}q_{i}$. Apply $\mathsf{RT}^{1}_{<\infty}$ to $f$ to obtain an
infinite set $H\subseteq D_{0}$ that is homogeneous for $f$. Then $H$ is a
$(0,\infty)$-homogeneous chain for $P$. $H$ is a chain because $H\subseteq
D_{0}\subseteq C_{0}$ and $C_{0}$ is a chain. Consider a $q\in P$. If $q\in
C_{0}$, then $q$ is comparable with every element of $H$ because $H\subseteq
C_{0}$ and $C_{0}$ is a chain. If $q\in C_{1}\setminus D_{1}$, then $q$ is
incomparable with every element of $D_{0}$ by assumption and therefore is
incomparable with every element of $H$ because $H\subseteq D_{0}$. If $q\in
D_{1}$, then $q=q_{i}$ for some $i<n$, so by the homogeneity of $H$, either
$q$ is comparable with every element of $H$ or $q$ is incomparable with every
element of $H$. ∎

If $C_{1}$ is finite, then we may apply Claim 1 with $D_{0}=C_{0}$ and
$D_{1}=C_{1}$ to obtain a $(0,\infty)$-homogeneous chain for $P$. Thus we may
assume that $C_{0}$ and $C_{1}$ are both infinite. Let $\langle
p_{n}:n\in\mathbb{N}\rangle$ be a bijective enumeration of $C_{0}$, and let
$\langle q_{n}:n\in\mathbb{N}\rangle$ be a bijective enumeration of $C_{1}$.
The goal is now to work into a situation where we may apply the following
claim.

######  Claim 2.

Suppose that there is an infinite $H\subseteq\mathbb{N}$ and an injection
$f\colon H\rightarrow\mathbb{N}$ where $\forall n\in
H\;\bigl{(}p_{n}\between_{P}q_{f(n)}\bigr{)}$. Then $P$ contains an
$(0,\infty)$-homogeneous chain.

###### Proof of Claim.

We may assume that the range of $f$ exists as a set by shrinking $H$ if
necessary.

For this argument, for a $p\in C_{0}$, let $p{\uparrow}=\\{x\in
C_{0}:x\geq_{P}p\\}$ and $p{\downarrow}=\\{x\in C_{0}:x\leq_{P}p\\}$ denote
the upward and downward closures of $p$ in $C_{0}$. Similarly, for a $q\in
C_{1}$, let $q{\uparrow}$ and $q{\downarrow}$ denote the upward and downward
closures of $q$ in $C_{1}$.

Let $X=\\{n\in H:p_{n}<_{P}q_{f(n)}\\}$, and let $Y=\\{n\in
H:p_{n}>_{P}q_{f(n)}\\}$. Then $H=X\cup Y$, so at least one of $X$ and $Y$ is
infinite. The two cases are symmetric, so suppose that $X$ is infinite for the
sake of argument. Let $L=\\{p_{n}:n\in X\\}$. Then $L\subseteq C_{0}$ and
$C_{0}$ is a chain, so $L$ is an infinite linear order. If $L$ is also stable,
then it has either an infinite ascending sequence or an infinite descending
sequence by $\mathsf{SADS}$. Thus $P$ has either an infinite ascending
sequence or an infinite descending sequence, so $P$ has a
$(0,\infty)$-homogeneous chain by $(\star)$.

If $L$ is not stable, then let $n\in X$ be such that $p_{n}{\uparrow}\cap L$
and $p_{n}{\downarrow}\cap L$ are both infinite. Suppose that there is an
$m\in X$ where $p_{n}\leq_{P}p_{m}$ and $q_{f(m)}{\uparrow}$ is infinite. Then
$p_{n}\leq_{P}p_{m}<_{P}q_{f(m)}$, so $C=p_{n}{\downarrow}\cup
q_{f(m)}{\uparrow}$ is an infinite chain in $P$. Furthermore, $C$ is
$(0,\infty)$-homogeneous because it has infinite intersection with both
$C_{0}$ and $C_{1}$. Finally, suppose instead that $q_{f(m)}{\uparrow}$ is
finite whenever $m\in X$ and $p_{n}\leq_{P}p_{m}$. Then the set
$\\{q_{f(m)}:m\in X\;\wedge\;p_{m}\geq_{P}p_{n}\\}\subseteq C_{1}$ is an
infinite chain because $p_{n}{\uparrow}\cap L$ is infinite, but it has no
least element. We may therefore define an infinite descending sequence in
$\\{q_{f(m)}:m\in X\;\wedge\;p_{m}\geq_{P}p_{n}\\}$. Thus $P$ has an infinite
descending sequence, so it has a $(0,\infty)$-homogeneous chain by $(\star)$.
∎

To finish the proof, define a coloring $c\colon[\mathbb{N}]^{2}\rightarrow 3$
as follows.

$\displaystyle c(n,m)=\begin{cases}0&\text{if $\forall i\leq
m\;(p_{n}\mid_{P}q_{i})$}\\\ 1&\text{if $\exists i\,(n<i\leq
m\;\wedge\;p_{n}\between_{P}q_{i})$}\\\ 2&\text{if $\exists i\,(i\leq
n\;\wedge\;p_{n}\between_{P}q_{i})\;\wedge\;\forall i\,(n<i\leq
m\;\rightarrow\;p_{n}\mid_{P}q_{i})$}.\end{cases}$

For every $n$, the color of $c(n,m)$ changes at most twice. This can be seen
by considering the value of $c(n,n+1)$ and making the following observations.

  * •

If $c(n,m_{0})=0$ for some $m_{0}>n$, then $c(n,m)\neq 2$ for all $m\geq
m_{0}$.

  * •

If $c(n,m_{0})=1$ for some $m_{0}>n$, then $c(n,m)=1$ for all $m\geq m_{0}$.

  * •

If $c(n,m_{0})=2$ for some $m_{0}>n$, then $c(n,m)\neq 0$ for all $m\geq
m_{0}$.

Apply ${2}\mbox{-}\mathrm{stable~{}}\mathsf{SRT}^{2}_{3}$, which is provable
in $\mathsf{RCA}_{0}$ by Proposition 5.8 item 1, to $c$ to obtain a set $H$
that is homogeneous for $c$, and consider the color for which $H$ is
homogeneous.

Suppose that $H$ is $0$-homogeneous. Let $C=\\{p_{n}:n\in H\\}$. Then
$C\subseteq C_{0}$ is an infinite chain, and thus every element of $C_{0}$ is
comparable with every element of $C$. Furthermore, every element of $C_{1}$ is
incomparable with every element of $C$ because $H$ is $0$-homogeneous. So $C$
is a $(0,\infty)$-homogeneous chain for $P$.

Suppose that $H$ is $1$-homogeneous. Define a function $f\colon
H\rightarrow\mathbb{N}$ by $f(n)=i$, where $i$ is $<$-least with $i>n$ and
$p_{n}\between_{P}q_{i}$. Such an $i$ exists by the $1$-homogeneity of $H$.
The function $f$ is injective because if $n$ and $m$ are members of $H$ with
$n<m$, then $f(n)\leq m$ and $f(m)>m$. Thus $H$ and $f$ satisfy the hypothesis
of Claim 2, so $P$ contains a $(0,\infty)$-homogeneous chain.

Finally, suppose that $H$ is $2$-homogeneous. First, suppose that there is a
bound $m_{0}$ such that $\forall n\in H\;\forall i\geq
m_{0}\;(p_{n}\mid_{P}q_{i})$. In this case, $D_{0}=\\{p_{n}:n\in H\\}$ and
$D_{1}=\\{q_{0},\dots,q_{m_{0}-1}\\}$ satisfy the hypothesis of Claim 1, so
$P$ contains a $(0,\infty)$-homogeneous chain. If there is no such bound
$m_{0}$, then $\forall m_{0}\;\exists n\in H\;\exists i\geq
m_{0}\;(p_{n}\between_{P}q_{i})$. However, given $m_{0}$, there cannot be a
witnessing $n\in H$ and $i\geq m_{0}$ with $n<m_{0}$. If there were, then we
could choose an $m\in H$ with $m>i$, in which case we would have $n,m\in H$,
$n<i<m$, and $p_{n}\between_{P}q_{i}$. We would then have that $c(n,m)=1$,
which contradicts that $H$ is $2$-homogeneous. Therefore, the situation is
that $\forall m\,\exists n\geq m\,\exists i\geq m\,(n\in
H\;\wedge\;p_{n}\between_{P}q_{i})$. We can thus define an infinite subset
$H_{0}=\\{n_{0},n_{1},n_{2},\dots\\}$ of $H$ and an injection $f\colon
H_{0}\rightarrow\mathbb{N}$ as follows. Given $n_{0}<n_{1}<\cdots<n_{\ell-1}$
and $f(n_{0}),f(n_{1}),\dots,f(n_{\ell-1})$, search for the first pair
$\langle n,i\rangle$ with $n$ and $i$ both greater than
$\max_{<}\\{n_{0},\dots,n_{\ell-1},f(n_{0}),\dots,f(n_{\ell-1})\\}$, with
$n\in H$, and with $p_{n}\between_{P}q_{i}$; put $n_{\ell}=n$; and put
$f(n_{\ell})=i$. Then $H_{0}$ and $f$ satisfy the hypothesis of Claim 2, so
$P$ contains a $(0,\infty)$-homogeneous chain. ∎

Finally, we show that $(0,\mathrm{cof})\mbox{-}\mathsf{RSpo}_{2}$ is provable
in $\mathsf{RCA}_{0}+\mathsf{I}\Sigma^{0}_{2}+\mathsf{ADS}$. To do this, we
first adapt Lemma 5.3 for use with partial orders of width $\leq\\!2$.

######  Lemma 5.10 ($\mathsf{RCA}_{0}$).

Let $(P,<_{P})$ be a partial order of width $\leq\\!2$, and let $\vec{P}$
denote $\vec{P}=P\oplus{<_{P}}$. Then there is a recursive function
$f\colon\mathbb{N}\rightarrow\mathbb{N}$ with the following properties for all
$e$ and all $X$.

  1. (1)

If $\Phi_{e}^{\vec{P}\oplus X}$ computes an infinite ascending sequence in $P$
and

$\displaystyle\forall m\;\exists n>m\;\exists p\in
P\;\left(p\geq_{P}\Phi_{e}^{\vec{P}\oplus
X}(m)\;\wedge\;p\mid_{P}\Phi_{e}^{\vec{P}\oplus X}(n)\right),$

then $\Phi_{f(e)}^{\vec{P}\oplus X}$ is total.

  2. (2)

If $\Phi_{f(e)}^{\vec{P}\oplus X}$ is total, then $\Phi_{e}^{\vec{P}\oplus X}$
is total, $\Phi_{e}^{\vec{P}\oplus X}$ computes an infinite sequence in $P$,
$\Phi_{f(e)}^{\vec{P}\oplus X}$ computes a ladder for $\Phi_{e}^{\vec{P}\oplus
X}$ in $P$, and

$\displaystyle\forall m\;\exists n>m\;\left(\Phi_{f(e)}^{\vec{P}\oplus
X}(m)\mid_{P}\Phi_{e}^{\vec{P}\oplus X}(n)\right).$

###### Proof.

Compute $f(e)$ by generating an index $f(e)=\widehat{e}$ for a machine
$\Phi_{\widehat{e}}$ that operates as follows. To compute
$\Phi_{\widehat{e}}^{\vec{P}\oplus X}(0)$, search for an $n>0$ and a $p_{0}\in
P$ with $p_{0}\geq_{P}\Phi_{e}^{\vec{P}\oplus X}(0)$ and
$p_{0}\mid_{P}\Phi_{e}^{\vec{P}\oplus X}(n)$. If $p_{0}$ is found, then output
$\Phi_{\widehat{e}}^{\vec{P}\oplus X}(0)=p_{0}$. To compute
$\Phi_{\widehat{e}}^{\vec{P}\oplus X}(m+1)$, first compute
$p_{m}=\Phi_{\widehat{e}}^{\vec{P}\oplus X}(m)$. Then search for an $n>m+1$
and a $p_{m+1}\in P$ with $p_{m+1}>_{P}p_{m}$,
$p_{m+1}\geq_{P}\Phi_{e}^{\vec{P}\oplus X}(m+1)$, and
$p_{m+1}\mid_{P}\Phi_{e}^{\vec{P}\oplus X}(n)$. If $p_{m+1}$ is found, then
output $\Phi_{\widehat{e}}^{\vec{P}\oplus X}(m+1)=p_{m+1}$.

Item 2 follows immediately from the definition of $\widehat{e}$. If
$\Phi_{\widehat{e}}^{\vec{P}\oplus X}$ is total, then for every $m$ it must be
that $\Phi_{e}^{\vec{P}\oplus X}(m){\downarrow}\in P$, that
$\Phi_{e}^{\vec{P}\oplus X}(m)\leq_{P}\Phi_{\widehat{e}}^{\vec{P}\oplus
X}(m)$, that $\Phi_{\widehat{e}}^{\vec{P}\oplus
X}(m)<_{P}\Phi_{\widehat{e}}^{\vec{P}\oplus X}(m+1)$, and that there is an
$n>m$ such that $\Phi_{\widehat{e}}^{\vec{P}\oplus
X}(m)\mid_{P}\Phi_{e}^{\vec{P}\oplus X}(n)$.

For item 1, suppose that $\Phi_{e}^{\vec{P}\oplus X}$ computes an infinite
ascending sequence in $P$, and suppose that for every $m$ there are an $n>m$
and a $p\in P$ with $p\geq_{P}\Phi_{e}^{\vec{P}\oplus X}(m)$ and
$p\mid_{P}\Phi_{e}^{\vec{P}\oplus X}(n)$. We use $\mathsf{I}\Sigma^{0}_{1}$ to
show that $\Phi_{\widehat{e}}^{\vec{P}\oplus X}$ is total. By assumption,
there are an $n>0$ and a $p_{0}\in P$ with
$p_{0}\geq_{P}\Phi_{e}^{\vec{P}\oplus X}(0)$ and
$p_{0}\mid_{P}\Phi_{e}^{\vec{P}\oplus X}(n)$. Thus
$\Phi_{\widehat{e}}^{\vec{P}\oplus X}(0){\downarrow}$. Inductively assume that
$\Phi_{\widehat{e}}^{\vec{P}\oplus X}(m){\downarrow}=p_{m}$. Then
$p_{m}\geq_{P}\Phi_{e}^{\vec{P}\oplus X}(m)$, and there is an $\ell>m$ such
that $p_{m}\mid_{P}\Phi_{e}^{\vec{P}\oplus X}(\ell)$. By assumption, there are
an $s>\ell$ and an $x\in P$ with

$\displaystyle x\geq_{P}\Phi_{e}^{\vec{P}\oplus X}(\ell)\quad\text{and}\quad
x\mid_{P}\Phi_{e}^{\vec{P}\oplus X}(s).$

The element $p_{m}$ is comparable either with $x$ or with
$\Phi_{e}^{\vec{P}\oplus X}(s)$ because $x\mid_{P}\Phi_{e}^{\vec{P}\oplus
X}(s)$ and $P$ has width $\leq\\!2$. Also, $x\nleq_{P}p_{m}$ because otherwise
we would have the contradiction $\Phi_{e}^{\vec{P}\oplus
X}(\ell)\leq_{P}x\leq_{P}p_{m}$. Similarly, $\Phi_{e}^{\vec{P}\oplus
X}(s)\nleq_{P}p_{m}$ because otherwise we would have the contradiction
$\Phi_{e}^{\vec{P}\oplus X}(\ell)\leq_{P}\Phi_{e}^{\vec{P}\oplus
X}(s)\leq_{P}p_{m}$. Therefore either $x>_{P}p_{m}$ or
$\Phi_{e}^{\vec{P}\oplus X}(s)>_{P}p_{m}$.

If $x>_{P}p_{m}$, then $x$ satisfies $x>_{P}p_{m}$,
$x\geq_{P}\Phi_{e}^{\vec{P}\oplus X}(\ell)\geq_{P}\Phi_{e}^{\vec{P}\oplus
X}(m+1)$, and $x\mid_{P}\Phi_{e}^{\vec{P}\oplus X}(s)$. That is, there are an
$n>m+1$ and a $p_{m+1}\in P$ with $p_{m+1}>_{P}p_{m}$,
$p_{m+1}\geq_{P}\Phi_{e}^{\vec{P}\oplus X}(m+1)$, and
$p_{m+1}\mid_{P}\Phi_{e}^{\vec{P}\oplus X}(n)$. So
$\Phi_{\widehat{e}}^{\vec{P}\oplus X}(m+1){\downarrow}$.

Otherwise $\Phi_{e}^{\vec{P}\oplus X}(s)>_{P}p_{m}$. In this case, again by
assumption there are a $t>s$ and a $y\in P$ with

$\displaystyle y\geq_{P}\Phi_{e}^{\vec{P}\oplus X}(s)\quad\text{and}\quad
y\mid_{P}\Phi_{e}^{\vec{P}\oplus X}(t).$

This $y$ satisfies $y\geq_{P}\Phi_{e}^{\vec{P}\oplus X}(s)>_{P}p_{m}$,
$y\geq_{P}\Phi_{e}^{\vec{P}\oplus X}(s)\geq_{P}\Phi_{e}^{\vec{P}\oplus
X}(m+1)$, and $y\mid_{P}\Phi_{e}^{\vec{P}\oplus X}(t)$. That is, there are an
$n>m+1$ and a $p_{m+1}\in P$ with $p_{m+1}>_{P}p_{m}$,
$p_{m+1}\geq_{P}\Phi_{e}^{\vec{P}\oplus X}(m+1)$, and
$p_{m+1}\mid_{P}\Phi_{e}^{\vec{P}\oplus X}(n)$. So
$\Phi_{\widehat{e}}^{\vec{P}\oplus X}(m+1){\downarrow}$. ∎

######  Theorem 5.11.

$\mathsf{RCA}_{0}+\mathsf{I}\Sigma^{0}_{2}+\mathsf{ADS}\vdash(0,\mathrm{cof})\mbox{-}\mathsf{RSpo}_{2}$.

###### Proof.

Let $(P,<_{P})$ be an infinite partial order of width $\leq\\!2$.
$\mathsf{RCA}_{0}\vdash\mathsf{CC}_{2}$ by Proposition 3.8, so we may apply
$\mathsf{CC}_{2}$ to $P$ to obtain an infinite chain $C$. Apply $\mathsf{ADS}$
to $C$ to obtain either an infinite ascending sequence or an infinite
descending sequence in $C$. By reversing $P$ if necessary, we may assume that
$P$ contains an infinite ascending sequence $A=\langle
a_{i}:i\in\mathbb{N}\rangle$.

Let $\vec{P}=P\oplus{<_{P}}$, and let $f\colon\mathbb{N}\rightarrow\mathbb{N}$
be the recursive function of Lemma 5.10. Define a sequence of indices $\langle
e_{i}:i\in\mathbb{N}\rangle$ as follows. First, let $e_{0}$ be an index such
that $\Phi_{e_{0}}^{\vec{P}\oplus A}(n)=a_{n}$ for each $n$, so that
$\Phi_{e_{0}}^{\vec{P}\oplus A}$ computes the infinite ascending sequence $A$.
Then given $e_{i}$, let $e_{i+1}=f(e_{i})$. There are two cases: either
$\Phi_{e_{i}}^{\vec{P}\oplus A}$ is partial for some $i$, or
$\Phi_{e_{i}}^{\vec{P}\oplus A}$ is total for all $i$.

First suppose that $\Phi_{e_{i}}^{\vec{P}\oplus A}$ is partial for some $i$.
Then, by $\mathsf{I}\Sigma^{0}_{2}$ in the form of the $\Sigma^{0}_{2}$ least
element principle, there is a least $i$ such that $\Phi_{e_{i}}^{\vec{P}\oplus
A}$ is partial. As $\Phi_{e_{0}}^{\vec{P}\oplus A}$ is total, it must be that
$i>0$ and that $\Phi_{e_{i-1}}^{\vec{P}\oplus A}$ is total. Then
$\Phi_{e_{i-1}}^{\vec{P}\oplus A}$ computes an infinite ascending sequence in
$P$ because either $e_{i-1}=e_{0}$, in which case
$\Phi_{e_{i-1}}^{\vec{P}\oplus A}$ computes $A$; or $e_{i-1}=f(e_{i-2})$, in
which case $\Phi_{e_{i-1}}^{\vec{P}\oplus A}$ computes an infinite ascending
sequence by Lemma 5.10 item 2. Let $B=\langle b_{n}:n\in\mathbb{N}\rangle$
denote the infinite ascending sequence computed by
$\Phi_{e_{i-1}}^{\vec{P}\oplus A}$, where $b_{n}=\Phi_{e_{i-1}}^{\vec{P}\oplus
A}(n)$ for each $n$. We claim that some tail of $B$ is
$(0,\infty)$-homogeneous. If not, then every tail of $B$ has a counterexample,
which implies that

$\displaystyle\forall m\;\exists n>m\;\exists p\in
P\;\left(p\geq_{P}\Phi_{e_{i-1}}^{\vec{P}\oplus
A}(m)\;\wedge\;p\mid_{P}\Phi_{e_{i-1}}^{\vec{P}\oplus A}(n)\right).$

Therefore $\Phi_{f(e_{i-1})}^{\vec{P}\oplus A}=\Phi_{e_{i}}^{\vec{P}\oplus A}$
is total by Lemma 5.10 item 1, which contradicts that
$\Phi_{e_{i}}^{\vec{P}\oplus A}$ is partial. Therefore some tail $B_{\geq n}$
of $B$ is $(0,\infty)$-homogeneous. Ascending $(0,\infty)$-homogeneous
sequences are necessarily $(0,\mathrm{cof})$-homogeneous, and infinite subsets
of $(0,\mathrm{cof})$-homogeneous chains are necessarily
$(0,\mathrm{cof})$-homogeneous as well. Thus we may thin $B_{\geq n}$ to an
infinite sequence whose range exists as a set and thereby obtain a
$(0,\mathrm{cof})$-homogeneous chain for $P$.

Now suppose that $\Phi_{e_{i}}^{\vec{P}\oplus A}$ is total for all $i$, and
let $A_{i}=\langle a^{i}_{n}:n\in\mathbb{N}\rangle$ denote the infinite
sequence computed by $\Phi_{e_{i}}^{\vec{P}\oplus A}$, where
$a^{i}_{n}=\Phi_{e_{i}}^{\vec{P}\oplus A}(n)$ for all $i$ and $n$. For every
$i$, $A_{i}$ is an infinite ascending sequence in $P$ and $A_{i+1}$ is a
ladder for $A_{i}$ by the fact that $A_{0}=A$ is an infinite ascending
sequence, by the assumption that every $\Phi_{e_{i}}^{\vec{P}\oplus A}$ is
total, and by Lemma 5.10 item 2. We have that for every
$i_{0},i_{1},n_{0},n_{1}$, if $i_{0}\leq i_{1}$ and $n_{0}\leq n_{1}$, then
$a^{i_{0}}_{n_{0}}\leq_{P}a^{i_{1}}_{n_{1}}$. This is because

$\displaystyle
a^{i_{0}}_{n_{0}}\leq_{P}a^{i_{0}}_{n_{1}}\leq_{P}a^{i_{0}+1}_{n_{1}}\leq_{P}a^{i_{0}+2}_{n_{1}}\leq_{P}\cdots\leq_{P}a^{i_{1}}_{n_{1}}.$

The inequality $a^{i_{0}}_{n_{0}}\leq_{P}a^{i_{0}}_{n_{1}}$ is because
$A_{i_{0}}$ is an ascending sequence. The inequalities
$a^{i_{0}}_{n_{1}}\leq_{P}a^{i_{0}+1}_{n_{1}}\leq_{P}\cdots\leq_{P}a^{i_{1}}_{n_{1}}$
are because $A_{i+1}$ is a ladder for $A_{i}$ for each $i$. Additionally, if
$n_{0}<n_{1}$, then the inequality $a^{i_{0}}_{n_{0}}<_{P}a^{i_{0}}_{n_{1}}$
is strict and therefore the inequality
$a^{i_{0}}_{n_{0}}<_{P}a^{i_{1}}_{n_{1}}$ is strict as well.

Define an infinite sequence $B=\langle b_{i}:i\in\mathbb{N}\rangle$ by
$b_{i}=a^{i}_{i}$ for each $n$. The sequence $B$ is ascending in $P$ because
$a_{i}^{i}<_{P}a_{i+1}^{i+1}$ for each $i$. The ascending sequence $B$ is also
$(0,\mathrm{cof})$-homogeneous. To see this, consider a $p\in P$ such that
$p\nleq_{P}b_{i}$ for all $i$. We show that $p\geq_{P}b_{i}$ for all $i$.
Given $i$, there is an $n>i+1$ with $a^{i+1}_{i+1}\mid_{P}a^{i}_{n}$ by Lemma
5.10 item 2. The element $p$ is comparable either with $b_{i+1}=a^{i+1}_{i+1}$
or with $a^{i}_{n}$ because $P$ has width $\leq 2$. We have that
$p\nleq_{P}b_{i+1}$ by assumption and that $p\nleq_{P}a^{i}_{n}$ because
$p\leq_{P}a^{i}_{n}$ yields the contradiction
$p\leq_{P}a^{i}_{n}\leq_{P}a^{n}_{n}=b_{n}$. Thus either
$p\geq_{P}b_{i+1}\geq_{P}b_{i}$ or
$p\geq_{P}a^{i}_{n}\geq_{P}a^{i}_{i}=b_{i}$. Therefore $p\geq_{P}b_{i}$, as
desired. Thus every $p\in P$ is either below some element of $B$, in which
case it is below almost every element of $B$ because $B$ is an ascending
sequence; or is above all elements of $B$. So $B$ is a
$(0,\mathrm{cof})$-homogeneous ascending sequence. As above, we may thin $B$
to an infinite sequence whose range exists as a set and thereby obtain a
$(0,\mathrm{cof})$-homogeneous chain for $P$. ∎

Unfortunately, the method of Theorem 5.11 does not appear to readily
generalize even to $3$-chain decomposable partial orders.

##  6\. Reversals and equivalences

We supply the following reversals.

  * •

$\mathsf{RCA}_{0}+\mathsf{RSpo}^{\mathsf{CD}}_{3}\vdash\mathsf{ADS}$ (Lemma
6.1).

  * •

$\mathsf{RCA}_{0}+\mathsf{RSpo}^{\mathsf{CD}}_{2}\vdash\mathsf{SADS}$ (Lemma
6.2).

  * •

$\mathsf{RCA}_{0}+\mathsf{RSpo}^{\mathsf{CD}}_{<\infty}\vdash\mathsf{I}\Sigma^{0}_{2}$
(Lemma 6.3).

  * •

$\mathsf{RCA}_{0}+(0,\mathrm{cof})\mbox{-}\mathsf{RSpo}^{\mathsf{CD}}_{2}\vdash\mathsf{ADS}$
(Lemma 6.4).

Theorem 6.6 then combines these reversals with the results of the previous
section in order to characterize the axiomatic strength of several versions of
the Rival–Sands theorem for partial orders. We also present a few questions.

######  Lemma 6.1.

$\mathsf{RCA}_{0}+\mathsf{RSpo}^{\mathsf{CD}}_{3}\vdash\mathsf{ADS}$.

###### Proof.

Let $(L,<_{L})$ be an infinite linear order. Let $(Q,<_{Q})$ be the three-
element partial order $Q=\\{a,b,z\\}$ with $a,b<_{Q}z$ and $a\mid_{Q}b$.
Consider the product partial order $(P,<_{P})$, where $P=L\times Q$ and
$\langle\ell_{0},q_{0}\rangle\leq_{P}\langle\ell_{1},q_{1}\rangle$ if and only
if $\ell_{0}\leq_{L}\ell_{1}$ and $q_{0}\leq_{Q}q_{1}$. The partial order $P$
has the $3$-chain decomposition $C_{a}=L\times\\{a\\}$,
$C_{b}=L\times\\{b\\}$, $C_{z}=L\times\\{z\\}$. Thus by
$\mathsf{RSpo}^{\mathsf{CD}}_{3}$, let $C$ be a $(0,\infty)$-homogeneous chain
for $P$.

Notice that $C$ cannot intersect both $C_{a}$ and $C_{b}$ because
$\langle\ell_{0},a\rangle\mid_{P}\langle\ell_{1},b\rangle$ for every
$\ell_{0},\ell_{1}\in L$. Thus either $C\subseteq C_{a}\cup C_{z}$ or
$C\subseteq C_{b}\cup C_{z}$. Assume for the sake of argument that $C\subseteq
C_{a}\cup C_{z}$. The $C\subseteq C_{b}\cup C_{z}$ case is symmetric.

We claim that $C\cap C_{z}$ has no maximum element. Suppose for a
contradiction that $\langle m,z\rangle$ is the maximum element of $C\cap
C_{z}$, and consider the element $\langle m,b\rangle$. Then $\langle
m,b\rangle<_{Q}\langle m,z\rangle$. However, every other element of $C$ is
either of the form $\langle\ell,a\rangle$, in which case $\langle
m,b\rangle\mid_{P}\langle\ell,a\rangle$ because $b\mid_{Q}a$; or of the form
$\langle\ell,z\rangle$ with $\ell<_{L}m$, in which case $\langle
m,b\rangle\mid_{P}\langle\ell,z\rangle$ because $m>_{L}\ell$ and $b<_{Q}z$.
Thus $\langle m,b\rangle$ is comparable with exactly one element of $C$,
contradicting that $C$ is $(0,\infty)$-homogeneous.

If $C\cap C_{z}\neq\emptyset$, then $C\cap C_{z}$ is non-empty and has no
maximum element, so we can define an infinite ascending sequence
$\langle\ell_{0},z\rangle<_{P}\langle\ell_{1},z\rangle<_{P}\langle\ell_{2},z\rangle<_{P}\cdots$
in $C\cap C_{z}$. This yields an infinite ascending sequence
$\ell_{0}<_{L}\ell_{1}<_{L}\ell_{2}<_{L}\cdots$ in $L$.

If $C\cap C_{z}=\emptyset$, then $C\subseteq C_{a}$. In this case, we claim
that $C$ has no minimum element. Suppose for a contradiction that $\langle
m,a\rangle$ is the minimum element of $C$, and consider the element $\langle
m,z\rangle$. Then $\langle m,a\rangle<_{P}\langle m,z\rangle$. However, every
other element of $C$ is of the form $\langle\ell,a\rangle$ with $m<_{L}\ell$,
in which case $\langle m,z\rangle\mid_{P}\langle\ell,a\rangle$ because
$m<_{L}\ell$ and $z>_{Q}a$. Thus $\langle m,z\rangle$ is comparable with
exactly one element of $C$, contradicting that $C$ is
$(0,\infty)$-homogeneous. We may now define an infinite descending sequence
$\langle\ell_{0},a\rangle>_{P}\langle\ell_{1},a\rangle>_{P}\langle\ell_{2},a\rangle>_{P}\cdots$
in $C$ and hence an infinite descending sequence
$\ell_{0}>_{L}\ell_{1}>_{L}\ell_{2}>_{L}\cdots$ in $L$.

Thus $L$ has either an infinite ascending sequence or an infinite descending
sequence. ∎

######  Lemma 6.2.

$\mathsf{RCA}_{0}+\mathsf{RSpo}^{\mathsf{CD}}_{2}\vdash\mathsf{SADS}$.

###### Proof.

Let $(L,<_{L})$ be an infinite stable linear order. Let $(Q,<_{Q})$ be the
two-element linear order $Q=\\{a,z\\}$ with $a<_{Q}z$, and let $(P,<_{P})$ be
the product partial order $L\times Q$. The partial order $P$ has the $2$-chain
decomposition $C_{a}=L\times\\{a\\}$, $C_{z}=L\times\\{z\\}$. Thus by
$\mathsf{RSpo}^{\mathsf{CD}}_{2}$, let $C$ be a $(0,\infty)$-homogeneous chain
for $P$.

The linear order $L$ is stable, so every $\ell\in L$ has either finitely many
$<_{L}$-predecessors or finitely many $<_{L}$-successors. We claim that $C\cap
C_{a}$ cannot contain two elements $\langle\ell,a\rangle$ and $\langle
r,a\rangle$ where $\ell$ has only finitely many $<_{L}$-predecessors and $r$
has only finitely many $<_{L}$-successors. Suppose for a contradiction that
$C\cap C_{a}$ does contain such an $\langle\ell,a\rangle$ and $\langle
r,a\rangle$, and consider the element $\langle\ell,z\rangle$. The element
$\langle\ell,z\rangle$ is comparable with an $\langle x,a\rangle\in C_{a}$ if
and only if $x\leq_{L}\ell$, and there are only finitely many such elements
$x\in L$. Thus $\langle\ell,z\rangle$ is comparable with only finitely many
elements of $C\cap C_{a}$. On the other hand, the element $\langle r,a\rangle$
is comparable with an $\langle x,z\rangle\in C_{z}$ if and only if
$r\leq_{L}x$, and there are only finitely many such elements $x\in L$. Thus
$C\cap C_{z}$ is finite because all of its elements are comparable with
$\langle r,a\rangle$. It follows that $\langle\ell,z\rangle$ is comparable
with $\langle\ell,a\rangle\in C$ and is comparable with only finitely many
elements of $C$ in total. This contradicts that $C$ is
$(0,\infty)$-homogeneous for $P$. Symmetric reasoning shows that $C\cap C_{z}$
also cannot contain two elements $\langle\ell,z\rangle$ and $\langle
r,z\rangle$ where $\ell$ has only finitely many $<_{L}$-predecessors and $r$
has only finitely many $<_{L}$-successors.

The chain $C$ is infinite, so either $C\cap C_{a}$ is infinite or $C\cap