Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

A precise statement of the Axiom of Dependent Choice (DC1) is as follows:

$$\forall A,F\big[\big(A\ne\emptyset\wedge [F\!:A\to{\cal P}(A)-\{\emptyset\}]\big)\to\exists g\big([g\!:\omega\to A]\wedge(\forall n\in\omega)[g(n+1)\in F(g(n))]\big)\big]$$

In words, this says that for any set $A$, and any function $F$ from $A$ to nonempty subsets of $A$, there exists a sequence $g(n)$ such that $g(n+1)$ is a member of $F(g(n))$ for every $n$. (Note that this can be proven for a sequence of any given finite length by induction without needing any new axioms.)

I would like to prove, from this statement of the axiom, the following generalization (which I'll call DC2):

$$\begin{align} \forall x,A,F\big[\big(\!\!&x\in A\wedge [F\!:A\to{\cal P}(A)-\{\emptyset\}]\big)\to \\ &\quad\exists g\big([g\!:\omega\to A]\wedge g(0)=x\wedge(\forall n\in\omega)[g(n+1)\in F(g(n))]\big)\big] \end{align}$$

The obvious difference is that now the initial value is specified, where previously it was completely unrestricted (except that $g(0)\in A$). My question is how to reconstruct DC2 from DC1. Obviously going the other way is trivial, but if we were after a certain sequence starting from $x$, say ($x,x_1,x_2,\dots$), then in particular any sequence $x_n,x_{n+1},x_{n+2},\dots$ starting in the middle of the sequence is also a possible "solution to the equation" provided by the $g$ of DC1, since $F$ is "memoryless" and the initial value could be any point in the domain. Now this is alright, because if we actually coincide with a possible solution to the problem with $x$ as initial value (that is, there is some sequence of choices starting at $x$ and containing $x_n$), we can use finite induction to patch the sequence back together. But in general, this is not the case, and there seems to be no way to construct $F$ to restrict the values of $g$ at the beginning, since the initial value is completely unpredictable and the same $F$ is used for all $n$.

I understand that (DC1) is a statement of the axiom in some (many?) textbooks, so this problem must be surmountable. How would one deal with it?

share|cite|improve this question
And this is why I often prefer using words to "formal notation". It is quite simple to give those precise formulations in a vastly more comprehensible way including both words and notation. – Asaf Karagila Jan 22 '13 at 19:36
@AsafKaragila Although words will get you a long way, formal notation is totally unambiguous, and in this case the "edge cases" which are not necessarily clear from the general description are of utmost importance. I subscribe to a balanced approach, where the formal notation is accompanied with a relatively complete description of the meaning of the notation, when the notation is not trivial (and this certainly isn't). – Mario Carneiro Jan 22 '13 at 20:48
"If $S$ is a non-empty set, and $R$ is a binary relation over $S$, such that $\operatorname{dom}(R)=S$, then there is a sequence $x_n\in S$ such that for all $n\in\omega$, $(x_n,x_{n+1})\in R$." – Asaf Karagila Jan 22 '13 at 20:58
@AsafKaragila That definition is indeed equivalent. – Mario Carneiro Jan 22 '13 at 21:09
And I feel that it is much clearer than both the "formal" and the "in words" combined. – Asaf Karagila Jan 22 '13 at 21:10
up vote 3 down vote accepted

Suppose you have $x,A,F$ as in the hypothesis of DC2. Let $S$ be the set of finite sequences of elements of $A$ whose first element is $x$ and whose successive terms are related by $F$, i.e., $s(n+1)\in F(s(n))$. So the elements of $S$ are finite partial approximations to the sort of infinite sequence demanded in DC2. For any $s\in S$, let $G(s)$ be the set of those $s'\in S$ obtainable by appending one additional element to the end of $s$. Now apply DC1 to $S$ and $G$ to get an infinite sequence of finite sequences, each extending the previous one by a single term. The union of all those finite sequences will be as required in DC2.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.