# Proving dependent choice with initial value from dependent choice without

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?

-
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

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.