# Reverse Mathematics of Well-Orderings

In Simpson's book, a well-ordered set $X$ is a linear ordering such that there are no functions $f : \mathbb{N} \rightarrow X$ which is decreasing.

However, a familiar definition of well-ordering is that every nonempty subset has a least element. The set theory proof that these two definitions are equivalent requires dependent choice.

In some model of $\text{RCA}_0$, is there a well-ordered set (Simpson's sense) which does not contain a least element. If such a set does exist then, does anyone know what the principle that every set that is not well-ordered in the second sense has an infinite decreasing function (i.e. not well-ordered in Simpson sense) is equivalent to.

-

A key difference between reverse mathematics and set theory is that "sets" in reverse mathematics are sets of natural numbers. This removes some, but not all, problems dependent choice.

$\mathsf{RCA}_0$ proves that if a linear ordering $(L,\prec)$ has no least element, then it has an infinite decreasing sequence.

The proof is simply to start with some element $a_0$, and given $a_i$ let $a_{i+1}$ be the first element in the usual ordering of $\mathbb{N}$ such that $a_{i+1} \not = a_i$ and $a_{i+1}\prec a_i$. This construction gives a computable decreasing sequence if $(L,\prec)$ is computable, and the construction can be formalized in $\mathsf{RCA}_0$.

The same proof shows

$\mathsf{RCA}_0$ proves that if $(L, \prec)$ has a subset with no least element then there is an infinite decreasing sequence in $L$.

On the other hand,

$\mathsf{RCA}_0$ proves that if a linear ordering $(L, \prec)$ has an infinite decreasing sequence, then it has a subset with no least element.

This proof uses a different method from recursion theory. Assume $(s_i)$ is an infinite $\prec$-decreasing sequence in $L$. The range $R$ of this sequence is a set of the desired form, but in general the range of a function may not be a set in $\mathsf{RCA}_0$, because the range corresponds to an r.e. set and $\mathsf{RCA}_0$ can only form computable sets. We can be inspired by the proof that any infinite r.e. set has an infinite computable subset.

All we need to do is to find some infinite subset of $R$ which is cofinal in $R$. To do this, we form a set $S$ which is the set of $n \in L$ such that $n$ is enumerated in ($s_i$) before any larger number (in the sense of $<_\mathbb{N}$) is enumerated. This set can be formed in $\mathsf{RCA}_0$, so that $\mathsf{RCA}_0$ proves that $S$ exists.

To show that $S$ is cofinal in $(s_i)$ requires a little induction argument that can also be formalized in $\mathsf{RCA}_0$. After a number $m$ is enumerated into $S$, at most $m$ numbers can be discarded before the next number is enumerated into $S$. Thus $S$ is infinite. But this means that if $s_k \in S$ there must be some $j > k$ with $s_j \in S$, as desired.

-