Does the existence of a recursive sequence that involves an arbitrary choice at every step require the axiom of choice?

Question

Say I want to define a sequence $(x_n)$ recursively, and at each step I make an arbitrary selection for $x_{n+1}$ out of some nonempty pool of acceptable candidates dependent on $x_n$. Does the existence of this sequence rest on the axiom of choice (or perhaps a weaker form)? And if so, how? That is, what would be the nonempty sets from which I choose each $x_n$?

Answer 1

In general, this (whenever we define by recursion a sequence, then it exists) is equivalent to the principle of dependent choice. Which we will formulate here in the following way:

If $X$ is a non-empty set, and $R$ is a binary relation on $X$, such that for every $x\in X$ there is some $y\in X$ such that $x\mathrel R y$, then there is a function $f\colon\Bbb N\to X$ such that $f(n)\mathrel R f(n+1)$ for all $n\in\Bbb N$.

To see the equivalence, first note that this implies the principle of dependent choice. If our principle holds, and $X$ is a non-empty set, $R$ is a binary relation satisfying the conditions required, then we define by recursion, $x_0$ to be some arbitrary element of $X$, and if $x_n$ was defined, then $x_{n+1}$ is some $y$ such that $x_n\mathrel R y$ is true. By our principle there is a sequence, which is a function $f(n)=x_n$, satisfying the wanted property.

On the other hand, if the principle of dependent choice holds, then our principle holds as well. To see this we need to take a slight detour first. The reason is that (in general) recursive definitions may appeal to previous choices as well, not just the last one that we made.

Suppose that we define a sequence $x_n$, and let $S$ be the set of all possible $x_n$'s, and let $X$ be the set of finite sequences from $S$ which satisfy the property that the sequence obeys our recursive definition. Now consider the relation on $X$, $t\lhd s$ if and only if $t$ is an initial segment of $s$. This relation satisfies the property that every element of $X$ is in the domain of the relation, since the recursion can always continue.

Therefore by the principle of dependent choice there is a function $f\colon\Bbb N\to X$ such that $f(n)\lhd f(n+1)$. But now consider the sequence $x_n=f(n)(n-1)$ (remember that $f(n)$ is a sequence of length at least $n$, so this is well-defined). It is not hard to see that $\{x_n\mid n\in\Bbb N\}$ satisfy the wanted property.