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 relationMathworldPlanetmath R on A such that ran(R)dom(R), then there is a sequence (an)n in A such that anRan+1.

Here, is the set of all natural numbersMathworldPlanetmath.

The relation between DC, AC (axiom of choiceMathworldPlanetmath), and CC (axiom of countable choice) are the following:

Proposition 1.

ZF+AC implies ZF+DC.

We prove this by using one of the equivalentsMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath of AC: Zorn’s lemma. For this proof, we define seg(n):={mmn}, the initial segment of with the greatest element n. Before starting the proof, we need a fact about initial segments:

Lemma 1.

The union of initial segments of N is either N or an initial segment.


Let S be a set of initial segments of . If s:=S, then B:=-S, so B has a least element r. As a result, none of iseg(r-1) is in B, and seg(r-1)s. If some mr is in s, then there is an initial segment seg(n)S with mseg(n), so that rseg(m)seg(n)s, contradicting rB. ∎

Remark. The fact that B in the proof above has a least element is a direct result of ZF, so the well-ordering principle (and hence AC) is not needed.

We are now ready for the proof of propositionPlanetmathPlanetmath 1.


Let R be a non-empty binary relation on a set A (of course non-empty). We want to find a function f:dom(R) such that f(n)Rf(n+1).

Let P be the set of all partial functionsMathworldPlanetmath f:dom(R) such that dom(f) is either an initial segment of , or itself, such that f(n)Rf(n+1), whenever n,n+1dom(f). Since R, some (a,b)R. Additionally, bran(R)dom(R). Define function g:{1,2}dom(R) by g(1)=a and g(2)=b. Then g(1)Rg(2), so that gP, or P is non-empty.

Partial orderMathworldPlanetmath P by inclusion so it is a poset. Let C be a chain in P, then h:=C is a partial function from to A. Since dom(h) is the union of initial segments or , dom(h) itself is either an initial segment or by Lemma 1.

Now, suppose m,m+1dom(h), then m+1dom(s) for some sC, so mdom(s) as well. Therefore s(m)Rs(m+1). Since h(i)=s(i) for any idom(s), we see that h(m)Rh(m+1). This shows that hP, 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 dom(f)={1,,n} for some n. Since f(n)dom(R), there is some dran(R) such that f(n)Rd. Define a partial function g:dom(R) such that dom(g)={1,,n+1}, and g(i)=f(i) for all i=1,,n, and g(n+1)=b. So gf extends f, contradicting the maximality of f. Hence, f is a total function, and we are done. ∎

Proposition 2.

ZF+DC implies ZF+CC.


Let C be a countable set of non-empty sets. We assume that C is countably infiniteMathworldPlanetmath, for the finite case can be proved using ZF alone, and is left for the reader.

Since there is a bijection ϕ:C, index each element in C by its image in , so that C={Aii}. Let A:=C. We want to find a function f:CA such that f(Ai)Ai for every i.

Define a binary relation R on A as follows: aRb iff there is an i such that aAi and bAi+1. Since each Ai, R. Furthermore, if bran(R), then bAi+1 for some i. Pick any cAi+2 (since Ai+2), so that bRc, and therefore bdom(R). This shows that ran(R)dom(R).

By DC, there is a function g:dom(R) such that g(i)Rg(i+1) for every i. Now, g(1)Aj for some j. Define a function h:A as follows, for each iseg(j-1), pick aiAi and set h(i):=ai (this can be done by inductionMathworldPlanetmath), and for ij, set h(i):=g(j-i+1) (arithmetic of finite cardinals is possible in ZF). Then h(i)Ai for all i.

Finally, define f:CA as follows: for each AiC, set f(Ai):=h(i). Then f has the desired property f(Ai)Ai, and the proof is completePlanetmathPlanetmathPlanetmathPlanetmathPlanetmath. ∎

However, the conversesMathworldPlanetmath of both of these implicationsMathworldPlanetmath 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 1 has a choice function, is independent from ZF+DC.

Remark. DC is related to Baire spacesPlanetmathPlanetmath in point-set topology. It can be shown that DC is equivalent to each of the following statements in ZF:


  • 1 T. Jech, Interdependence of weakened forms of the axiom of choice, Comment. Math. Univ. Carolinae 7, pp. 359-371, (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 127-130 (1948).
Title axiom of dependent choices
Canonical name AxiomOfDependentChoices
Date of creation 2013-03-22 18:46:39
Last modified on 2013-03-22 18:46:39
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 7
Author CWoo (3771)
Entry type Definition
Classification msc 03E25