When induction proofs need a choice function

Question

Reading the comment to this the user makes the argument that one can pick a dense subset of a separable vector spaces without relying the axiom of countable choices. Since the comment got a lot of up votes, I guess it's correct, but to me this seems very strange. My rule of thumb was/is the following: We can get by without a choice function if

• There is a canonical choice at each iteration.
• The proof doesn't actually require the iteration process to terminate.

None of these seem to be satisfied in the present case, unless there is a canonical choice for the dense subset, or the set is dense at some finite iteration, so my question is:

When can I tell if an induction arguments relies on the existence of a countable choice function?

Answer 1

You are right that a canonical choice function is needed for recursive constructions.

However, if you have an underlying set which is countable—or generally can be well-ordered—then there is a canonical choice function given by enumerating the set, and at each step choosing the element with the least index in the enumeration which "fits".

In those cases, you only need to prove that the recursive construction can actually proceed from $n$ steps to $n+1$ steps. Just like you would in "the usual case where choice is assumed".

Note that to choose one element from a family which is assumed to be non-empty, no choice is needed. So if you assume that a set is countable, for example, you don't need the axiom of choice to enumerate it. You already assume that an enumeration exists.

---

Also, let me point out this minor issue that "countable choice" only means that you can make a choice once from a countable family of sets. What you want for recursive definitions and/or inductive proofs, is Dependent Choice, which allows you to make a countable sequence of choices, where each choice might depend on the previous ones you made. Just like in a recursive definition.

Answer 2

Your misunderstanding seems to come from the fact that you are not iterating making choices -- you are not picking the elements of the countable dense subset one by one, or anything like that. By definition, "$X$ is separable" means that $$ \{Y \in \mathcal P(X) \mid |Y| \leq \aleph_0 \land \overline{Y} = X\} \neq \emptyset. $$ Since it is non-empty, it contains some element. Pick one element from this set -- we can call it $Y$. There is no further iteration to be done; you now have a separating subset $Y$ of $X$.