axiom of dependent choices
The axiom of dependent choices (DC), or the principle of dependent choices, is the following statement:
given a set $A$ and a binary relation^{} $R\ne \mathrm{\varnothing}$ on $A$ such that $\mathrm{ran}(R)\subseteq \mathrm{dom}(R)$, then there is a sequence ${({a}_{n})}_{n\in \mathbb{N}}$ in $A$ such that ${a}_{n}R{a}_{n+1}$.
Here, $\mathbb{N}$ is the set of all natural numbers^{}.
The relation between DC, AC (axiom of choice^{}), and CC (axiom of countable choice) are the following:
Proposition 1.
ZF+AC implies ZF+DC.
We prove this by using one of the equivalents^{} of AC: Zorn’s lemma. For this proof, we define $\mathrm{seg}(n):=\{m\in \mathbb{N}\mid m\le n\}$, the initial segment of $\mathbb{N}$ with the greatest element $n$. Before starting the proof, we need a fact about initial segments:
Lemma 1.
The union of initial segments of $\mathrm{N}$ is either $\mathrm{N}$ or an initial segment.
Proof.
Let $S$ be a set of initial segments of $\mathbb{N}$. If $s:=\bigcup S\ne \mathbb{N}$, then $B:=\mathbb{N}S\ne \mathrm{\varnothing}$, so $B$ has a least element $r$. As a result, none of $i\in \mathrm{seg}(r1)$ is in $B$, and $\mathrm{seg}(r1)\subseteq s$. If some $m\ge r$ is in $s$, then there is an initial segment $\mathrm{seg}(n)\in S$ with $m\in \mathrm{seg}(n)$, so that $r\in \mathrm{seg}(m)\subseteq \mathrm{seg}(n)\subseteq s$, contradicting $r\in B$. ∎
Remark. The fact that $B$ in the proof above has a least element is a direct result of ZF, so the wellordering principle (and hence AC) is not needed.
We are now ready for the proof of proposition^{} 1.
Proof.
Let $R$ be a nonempty binary relation on a set $A$ (of course nonempty). We want to find a function $f:\mathbb{N}\to \mathrm{dom}(R)$ such that $f(n)Rf(n+1)$.
Let $P$ be the set of all partial functions^{} $f:\mathbb{N}\Rightarrow \mathrm{dom}(R)$ such that $\mathrm{dom}(f)$ is either an initial segment of $\mathbb{N}$, or $\mathbb{N}$ itself, such that $f(n)Rf(n+1)$, whenever $n,n+1\in \mathrm{dom}(f)$. Since $R\ne \mathrm{\varnothing}$, some $(a,b)\in R$. Additionally, $b\in \mathrm{ran}(R)\subseteq \mathrm{dom}(R)$. Define function $g:\{1,2\}\to \mathrm{dom}(R)$ by $g(1)=a$ and $g(2)=b$. Then $g(1)Rg(2)$, so that $g\in P$, or $P$ is nonempty.
Partial order^{} $P$ by inclusion so it is a poset. Let $C$ be a chain in $P$, then $h:=\bigcup C$ is a partial function from $\mathbb{N}$ to $A$. Since $\mathrm{dom}(h)$ is the union of initial segments or $\mathbb{N}$, $\mathrm{dom}(h)$ itself is either an initial segment or $\mathbb{N}$ by Lemma 1.
Now, suppose $m,m+1\in \mathrm{dom}(h)$, then $m+1\in \mathrm{dom}(s)$ for some $s\in C$, so $m\in \mathrm{dom}(s)$ as well. Therefore $s(m)Rs(m+1)$. Since $h(i)=s(i)$ for any $i\in \mathrm{dom}(s)$, we see that $h(m)Rh(m+1)$. This shows that $h\in P$, or that $C$ has an upper bound in $P$.
By Zorn’s lemma, $P$ has a maximal element $f$. We claim that $f$ is a total function. If not, then $\mathrm{dom}(f)=\{1,\mathrm{\dots},n\}$ for some $n$. Since $f(n)\in \mathrm{dom}(R)$, there is some $d\in \mathrm{ran}(R)$ such that $f(n)Rd$. Define a partial function $g:\mathbb{N}\Rightarrow \mathrm{dom}(R)$ such that $\mathrm{dom}(g)=\{1,\mathrm{\dots},n+1\}$, and $g(i)=f(i)$ for all $i=1,\mathrm{\dots},n$, and $g(n+1)=b$. So $g\ne f$ extends $f$, contradicting the maximality of $f$. Hence, $f$ is a total function, and we are done. ∎
Proposition 2.
ZF+DC implies ZF+CC.
Proof.
Let $C$ be a countable set of nonempty sets. We assume that $C$ is countably infinite^{}, for the finite case can be proved using ZF alone, and is left for the reader.
Since there is a bijection $\varphi :C\to \mathbb{N}$, index each element in $C$ by its image in $\mathbb{N}$, so that $C=\{{A}_{i}\mid i\in \mathbb{N}\}$. Let $A:=\bigcup C$. We want to find a function $f:C\to A$ such that $f({A}_{i})\in {A}_{i}$ for every $i\in \mathbb{N}$.
Define a binary relation $R$ on $A$ as follows: $aRb$ iff there is an $i\in \mathbb{N}$ such that $a\in {A}_{i}$ and $b\in {A}_{i+1}$. Since each ${A}_{i}\ne \mathrm{\varnothing}$, $R\ne \mathrm{\varnothing}$. Furthermore, if $b\in \mathrm{ran}(R)$, then $b\in {A}_{i+1}$ for some $i\in \mathbb{N}$. Pick any $c\in {A}_{i+2}$ (since ${A}_{i+2}\ne \mathrm{\varnothing}$), so that $bRc$, and therefore $b\in \mathrm{dom}(R)$. This shows that $\mathrm{ran}(R)\subseteq \mathrm{dom}(R)$.
By DC, there is a function $g:\mathbb{N}\to \mathrm{dom}(R)$ such that $g(i)Rg(i+1)$ for every $i\in \mathbb{N}$. Now, $g(1)\in {A}_{j}$ for some $j\in \mathbb{N}$. Define a function $h:\mathbb{N}\to A$ as follows, for each $i\in \mathrm{seg}(j1)$, pick ${a}_{i}\in {A}_{i}$ and set $h(i):={a}_{i}$ (this can be done by induction^{}), and for $i\ge j$, set $h(i):=g(ji+1)$ (arithmetic of finite cardinals is possible in ZF). Then $h(i)\in {A}_{i}$ for all $i\in \mathbb{N}$.
Finally, define $f:C\to A$ as follows: for each ${A}_{i}\in C$, set $f({A}_{i}):=h(i)$. Then $f$ has the desired property $f({A}_{i})\in {A}_{i}$, and the proof is complete^{}. ∎
However, the converses^{} of both of these implications^{} are false. Jensen proved the independence of DC from ZF+CC, and Mostowski and Jech proved the independence of AC from ZF+DC. In fact, it was shown that the weaker version of AC, which states that every set with cardinality at most ${\mathrm{\aleph}}_{1}$ has a choice function, is independent from ZF+DC.
Remark. DC is related to Baire spaces^{} in pointset topology. It can be shown that DC is equivalent to each of the following statements in ZF:

•
Any complete pseudometric space is Baire under the topology^{} induced by the pseudometric.

•
Any product^{} of compact^{} Hausdorff spaces is Baire under the product topology.
References
 1 T. Jech, Interdependence of weakened forms of the axiom of choice, Comment. Math. Univ. Carolinae 7, pp. 359371, (1966).
 2 R. B. Jensen Independence of the axiom of dependent choices from the countable axiom of choice (abstract), Jour. Symbolic Logic 31, 294, (1966).
 3 A. Levy, Basic Set Theory, Dover Publications Inc., (2002).
 4 A. Mostowski On the principle of dependent choices, Fund. Math. 35, pp 127130 (1948).
Title  axiom of dependent choices 

Canonical name  AxiomOfDependentChoices 
Date of creation  20130322 18:46:39 
Last modified on  20130322 18:46:39 
Owner  CWoo (3771) 
Last modified by  CWoo (3771) 
Numerical id  7 
Author  CWoo (3771) 
Entry type  Definition 
Classification  msc 03E25 