The axiom of dependent choice: a relation in which every element is related to something admits an $\mathbb{N}$-indexed chain

Let $X$ be a set and let $R\subseteq X\times X$ be a binary relation on $X$. Call $R$ entire on $X$ when

$\text{for every }x\in X\text{ there is }y\in X\text{ with }xRy\mathrm{.}$

The Axiom of Dependent Choice, written $\mathrm{D}\mathrm{C}$, is the following statement.

For every nonempty set $X$, every relation $R$ entire on $X$, and every $a\in X$, there is a function $x:\mathbb{N}\to X$ (A function is a relation $f$ with $(a,b)\in f$ and $(a,c)\in f$ implying $b=c$; $f:A\to B$, the value $f(a)$, domain and codomain, The natural numbers $\mathbb{N}$ (von Neumann)) with $x_0=a\text{and}{x}_{n}R{x}_{n+1}\text{ for every }n\in \mathbb{N}\mathrm{.}$

Here a sequence in $X$ means a function from $\mathbb{N}$ to $X$, not necessarily a real-valued sequence. As everywhere in this library $\mathbb{N}$ contains $0$, and the sequence is indexed from $0$; the term $x_0$ is the prescribed starting point $a$ and every later term is related to its predecessor.

What DC adds to what came before. Choice function and The Axiom of Choice select one element from each member of a family that is fixed in advance, and The Axiom of Countable Choice (${\mathrm{A}\mathrm{C}}_{\omega }$) does the same for a family indexed by $\mathbb{N}$. In both, the family is given before any selection is made. DC is the principle needed when the $n$-th set to select from is not known until the first $n$ selections have been made: here the admissible values of $x_{n+1}$ are exactly the $R$-successors of $x_n$, so the family being chosen from is built along the choosing. That is precisely the situation ${\mathrm{A}\mathrm{C}}_{\omega }$ does not cover, and it is why a construction "pick $x_{n+1}$ depending on $x_n$, for every $n$ at once" is not licensed by countable choice.

The starting point may be dropped. The formally weaker statement obtained by deleting the clause $x_0=a$ — for every nonempty $X$ and every entire $R$ there is a sequence with $x_{n}R{x}_{n+1}$ for all $n$ — is an immediate consequence of the form above, since $X$ is nonempty and any of its elements may be taken as $a$. The reverse derivation is standard and is not needed anywhere in this library, so it is not carried out; every use below prescribes $x_0$.

$R$ need not be an order and the terms need not be distinct. What DC delivers is a sequence, that is a function $\mathbb{N}\to X$, not a chain in the order-theoretic sense (Chain in a poset). The relation may be symmetric, and the sequence may repeat a value or be constant; all that is asserted is $x_{n}R{x}_{n+1}$ at every index.

Where DC sits among the choice principles. It is a standard fact, proved in the references and not in this library, that

$\mathrm{A}\mathrm{C}⟹\mathrm{D}\mathrm{C}⟹{\mathrm{A}\mathrm{C}}_{\omega },$

and that neither implication reverses. The non-reversals are relative-consistency results: what they establish is that ZF, if consistent, does not prove the missing implications, never that those implications are false. This library contains neither forcing nor permutation models and proves no independence result, so all of that is quoted from the references and used nowhere.

Nothing in this library proves DC, and nothing assumes it silently. Like The Axiom of Choice and The Axiom of Countable Choice (${\mathrm{A}\mathrm{C}}_{\omega }$), DC is a statement that may be assumed or not. Every theorem whose proof uses it says so in its own statement, and the accounting for the compactness page is collected in What each implication between the compactness properties of a metric space costs: which are theorems of ZF, which use countable choice, and which use dependent choice ↗.

An upper bound, never a lower one. When a later item records that its proof uses DC, the claim made is that the argument given here is carried out in $\mathrm{Z}\mathrm{F}+\mathrm{D}\mathrm{C}$. No item claims that DC is necessary for the statement proved, because establishing necessity means separating the statement from ZF, and that is an independence result of exactly the kind this library does not prove.