Inductive definition with choice for sequence

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.

• It looks like the choice strength you need for this is exactly Dependent Choice. – Henning Makholm Oct 25 '13 at 20:24
• Alternatively, in topology you'd often be able to get away with assuming your space is separable, and choosing your things from a countably dense subset. – Henning Makholm Oct 25 '13 at 20:27
• If the topology is done over functional space (which is what my class is about right now) then that assumption don't apply though. And beside that only apply if all the choice are from set that have interior anyway. – Gina Oct 25 '13 at 22:40

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.

• Oh I see. Thanks for the clue on DC, my professor never mentioned it. I just look it up and apparently it is quite difficult to prove that DC is strictly stronger than Countable Choice, though I guess that confirm that Countable Choice is indeed not enough for the proof. – Gina Oct 25 '13 at 22:46
• @Gina: None of the "irreversible implication" proofs about choice principles are easy, and they all require a lot of knowledge about set theory. But that been said most people are familiar with full choice and countable choice, and while it's not uncommon to meet people familiar with $\sf DC$, many are not. – Asaf Karagila Oct 25 '13 at 22:49