[proofplan] We prove both directions of the equivalence between well-ordering and the absence of infinite strictly decreasing sequences. The forward direction ($\Rightarrow$) is a short contrapositive: an infinite strictly decreasing sequence is itself a non-empty subset with no least element, violating the well-ordering hypothesis. The reverse direction ($\Leftarrow$) is a construction by recursion: given a non-empty subset $S$ with no least element, we produce an infinite strictly decreasing sequence in $S$ by repeatedly selecting strictly smaller elements, invoking the [Axiom of Dependent Choice](/theorems/???) to make the countably many selections simultaneously. [/proofplan] [step:Fix notation and state the contrapositive form of each direction] Let $(X, <)$ be a total order. Recall that $(X, <)$ is a **well-ordering** if every non-empty subset $S \subseteq X$ has a least element — an element $m \in S$ such that $m \le x$ for every $x \in S$ (equivalently, $m < x$ or $m = x$). We prove the biconditional by splitting into two implications: - **($\Rightarrow$)** *If $(X, <)$ is a well-ordering, then it has no infinite strictly decreasing sequence.* We prove the contrapositive: *if $(X, <)$ admits an infinite strictly decreasing sequence, then it is not a well-ordering.* - **($\Leftarrow$)** *If $(X, <)$ has no infinite strictly decreasing sequence, then it is a well-ordering.* We prove the contrapositive: *if $(X, <)$ is not a well-ordering, then it admits an infinite strictly decreasing sequence.* [guided] Before attacking the argument, let us unpack the terms and strategy. A **well-ordering** is a total order in which every non-empty subset has a least element. The negation of well-ordering is therefore: *there exists a non-empty subset with no least element*. An **infinite strictly decreasing sequence** is a function $\mathbb{N} \to X$, written $n \mapsto x_n$, such that $x_{n+1} < x_n$ for every $n \in \mathbb{N}$. We prove both implications by contrapositive, because the positive form of each is cumbersome: - For $(\Rightarrow)$, rather than arguing from "well-ordered" to "no infinite decreasing sequence", we argue from "there is an infinite decreasing sequence" to "not well-ordered". The hypothesis supplies a concrete object (the sequence); from it we must extract a concrete witness (a subset with no least element). This is a one-line construction. - For $(\Leftarrow)$, rather than arguing from "no infinite decreasing sequence" to "well-ordered", we argue from "not well-ordered" to "there is an infinite decreasing sequence". Here the hypothesis is weaker (a mere non-existence) but the conclusion is stronger (an explicit sequence). The argument is a recursion that produces the sequence step by step, and will require a choice principle. [/guided] [/step] [step:Prove that an infinite strictly decreasing sequence yields a subset with no least element] Suppose there exists an infinite strictly decreasing sequence $(x_n)_{n \in \mathbb{N}}$ in $X$, meaning \begin{align*} x_1 > x_2 > x_3 > \cdots, \qquad \text{i.e.\ } x_{n+1} < x_n \text{ for every } n \in \mathbb{N}. \end{align*} Define $S := \{x_n : n \in \mathbb{N}\} \subseteq X$. Then $S$ is non-empty (it contains $x_1$) and has no least element: if $m \in S$, then $m = x_k$ for some $k \in \mathbb{N}$, and since $x_{k+1} < x_k = m$ with $x_{k+1} \in S$, the element $m$ is not a lower bound for $S$. This contradicts the defining property of a well-ordering, so $(X, <)$ is not well-ordered. This proves $(\Rightarrow)$ by contrapositive. [guided] Assume an infinite strictly decreasing sequence $(x_n)_{n \in \mathbb{N}}$ exists in $X$: $x_{n+1} < x_n$ for every $n \in \mathbb{N}$. We must exhibit a non-empty subset with no least element. The natural candidate is the **image** of the sequence: \begin{align*} S &:= \{x_n : n \in \mathbb{N}\}. \end{align*} Why this set? Because the strict decrease makes "being in $S$" incompatible with "being a lower bound for $S$": any element of $S$ has the form $x_k$, and the very next term $x_{k+1}$ is strictly smaller and also in $S$. Let us verify the two required properties. **$S$ is non-empty.** Since $\mathbb{N}$ is non-empty, the element $x_1 \in S$. **$S$ has no least element.** Let $m \in S$; we show $m$ is not a least element of $S$. By definition of $S$, there is some $k \in \mathbb{N}$ with $m = x_k$. By the strict decrease, $x_{k+1} < x_k = m$. But $x_{k+1} \in S$, so $S$ contains an element strictly smaller than $m$; hence $m$ is not a least element. Since $m \in S$ was arbitrary, $S$ has no least element. The existence of such an $S$ contradicts well-ordering. [/guided] [/step] [step:Prove that a subset with no least element yields an infinite strictly decreasing sequence] For the reverse direction, suppose $(X, <)$ is not well-ordered: there exists a non-empty subset $S \subseteq X$ with no least element. We construct an infinite strictly decreasing sequence $(x_n)_{n \in \mathbb{N}}$ with $x_n \in S$ for every $n$. **Key observation.** Since $S$ has no least element, for every $x \in S$ there exists some $x' \in S$ with $x' < x$. That is, the set \begin{align*} T(x) &:= \{x' \in S : x' < x\} \end{align*} is non-empty for every $x \in S$. **Recursive construction.** Fix an arbitrary $x_1 \in S$ (possible since $S \ne \varnothing$). Given $x_n \in S$, the set $T(x_n) \ne \varnothing$, so we may choose some $x_{n+1} \in T(x_n)$; by construction $x_{n+1} \in S$ and $x_{n+1} < x_n$. The sequence $(x_n)_{n \in \mathbb{N}}$ with $x_1 > x_2 > x_3 > \cdots$ produced by this recursion is infinite and strictly decreasing, as required. Formally, the simultaneous selection of $x_{n+1}$ from $T(x_n)$ for all $n$ is furnished by the [Axiom of Dependent Choice](/theorems/???): given a non-empty set $A$ (here $A = S$) and a relation $R \subseteq A \times A$ such that for every $a \in A$ there exists $b \in A$ with $(a, b) \in R$ (here $R = \{(x, x') : x' < x\}$, and the hypothesis "$S$ has no least element" guarantees totality), there exists a sequence $(a_n)_{n \in \mathbb{N}}$ in $A$ with $(a_n, a_{n+1}) \in R$ for every $n$. The $(a_n)$ so produced is the desired strictly decreasing sequence. This proves $(\Leftarrow)$ by contrapositive. [guided] We are given that $(X, <)$ is not well-ordered. Unpacking: there exists a non-empty $S \subseteq X$ such that $S$ has no least element. We must produce an infinite strictly decreasing sequence in $X$. **Strategy.** Start anywhere in $S$; at each stage, jump to a strictly smaller element of $S$. The absence of a least element guarantees such a jump is always possible. Iterating forever yields the sequence. **Setting up the recursion.** The phrase "$S$ has no least element" means: there is no $m \in S$ with $m \le x'$ for all $x' \in S$. Equivalently (since $<$ is total): for every $m \in S$, there exists $x' \in S$ with $x' < m$. Let us package this as a set: \begin{align*} T(x) &:= \{x' \in S : x' < x\}, \qquad x \in S. \end{align*} The observation "$S$ has no least element" says precisely that $T(x) \ne \varnothing$ for every $x \in S$. This is the engine that makes the recursion run. **Performing the recursion.** Pick $x_1 \in S$ (possible since $S \ne \varnothing$). Suppose $x_1, \dots, x_n$ have been chosen with each $x_k \in S$ and $x_{k+1} < x_k$. Since $x_n \in S$, we have $T(x_n) \ne \varnothing$, so we can select some $x_{n+1} \in T(x_n)$. By construction $x_{n+1} \in S$ and $x_{n+1} < x_n$. The induction continues forever, producing $(x_n)_{n \in \mathbb{N}}$ with $x_1 > x_2 > x_3 > \cdots$. **A subtlety: we need to make countably many choices.** At each stage we select an arbitrary element from $T(x_n)$, but there is no canonical choice function. To rigorously obtain a single sequence $(x_n)$ from these infinitely many independent selections, we invoke the [Axiom of Dependent Choice](/theorems/???): if $A \ne \varnothing$ and $R \subseteq A \times A$ satisfies $\forall a \in A\ \exists b \in A\ (a R b)$, then there exists $(a_n)_{n \in \mathbb{N}}$ with $a_{n+1} R a_n$ inverted — actually, $a_n R a_{n+1}$ — for every $n$. Apply DC with: - $A := S$ (non-empty by hypothesis); - $R := \{(x, x') \in S \times S : x' < x\}$. The hypothesis "$\forall x \in S,\ T(x) \ne \varnothing$" is exactly "$\forall x \in S,\ \exists x' \in S,\ (x, x') \in R$". DC then produces a sequence $(x_n) \in S^\mathbb{N}$ with $(x_n, x_{n+1}) \in R$ for every $n$, i.e.\ $x_{n+1} < x_n$. This is the desired infinite strictly decreasing sequence. **Why DC rather than ordinary induction?** Ordinary induction defines $x_{n+1}$ as a deterministic function of $x_n$ (a recursion with a specified recurrence). Here the choice of $x_{n+1}$ is not canonical — $T(x_n)$ may have many elements and we have no preferred one. DC is exactly the weak choice principle that lets us perform countably many arbitrary selections coherently. [/guided] [/step] [step:Combine the two implications] Step 2 proves the contrapositive of $(\Rightarrow)$: if $(X, <)$ admits an infinite strictly decreasing sequence, it is not a well-ordering. Step 3 proves the contrapositive of $(\Leftarrow)$: if $(X, <)$ is not a well-ordering, it admits an infinite strictly decreasing sequence. Taken together, a total order $(X, <)$ is a well-ordering if and only if it contains no infinite strictly decreasing sequence. This completes the proof. [/step]