Inductive definition with choice for sequence

Question

In topology there is a very common way to define a sequence. This usually go something like:

"Define $\{z_{n}\}$ to be a sequence such that $z_{0}$ is <blah blah blah>, and $z_{n}$ is such that $R(z_{0},z_{1},\ldots,z_{n})$ is true. The sequence is well-defined since there always exist $z_{n}$ that satisfy that relationship because <blah blah blah>."

(here $R$ is some sort of relationship, such as for example $z_{n}\subset\bigcap\limits_{i=1}^{n-1}B_{\delta}(z_{i})$, though the particular is irrelevant for this question)

Sure it seems intuitively clear, and I use it all the time. My professor, despite being a constructivist, accept this reasoning. But I have been wondering out of curiousity: is there anyway to prove that such a sequence exist? Hope someone can shed a light on this. I have only seen a book (about Complex Analysis) that mention that and call this principle of inductive definition though fortunately for it, it never need to use choice anywhere. The name appeared to be made up for the book, since I cannot find anything with that exact name on the Internet.

Note that the issue mainly at play here are:

-We can prove any finite subsequence exist by induction. The question is about the existence of the infinite sequence.

-There is always choice needed to be made at each step ie. there are many $z_{n}$ that fit the bill. Since this is usually about general topological space, there is no good way to actually pick out an element specifically. Axiom of Countable Choice is allowed of course, but even given that, how do you prove that an infinite sequence exist. If Axiom of Countable Choice is not enough, then why, and how do you prove it using the full Axiom of Choice?

I was able to prove that a sequence exist when no choice is needed. I can also prove it assuming that the space is countable (basically reduce to non-choice version through well-ordering). However most topological space is not countable and choice are needed, so I'm stuck.

Thank you for your help.

Answer 1

The principle used to define infinite sequences by induction is stronger than the axiom of countable choice and it is known as Dependent Choice, or $\sf DC$. The principle has many equivalent formulations, one of them is as follows:

Suppose that $S$ is a non-empty set and $R$ is a binary relation on $S$, whose domain is all $S$. Then there exists function $f\colon\Bbb N\to S$ such that $f(n)\mathrel{R}f(n+1)$ for every $n\in\Bbb N$.

The axiom of countable choice is sufficient when we can uniformly define the families from which we are choosing. If we want an arbitrary point whose distance from $x$ is at most $\frac1n$ then this is doable with the axiom of countable choice as we can choose $x_n$ from $B_{\frac1n}(x)$. But often we define $x_n$ to be an element definable from the previously chosen elements, in which case we are in fact using $\sf DC$.

Finally, to use the full axiom of choice one can usually do one of the two following things:

1. Well-order the space, then proceed to pick the least $x$ in the well-ordering which satisfies the needed requirements. Or, more directly,

2. Fix a choice function on all the non-empty subsets of the space (or just the relevant subsets, if we care about open sets or whatever), then define use induction to choose using our choice function. Using the choice function as a parameter the choice of element is no longer arbitrary and we can define the infinite sequence without difficulty.