How to construct a sequence inductively in set theory? I would like to construct a sequence $\{a_n\}$ inductively in set theory.

(1) I can choose $a_1$ from $\mathbb{R}$.
(2) If I have chosen $a_i$ ($i \ge 1$), then there exists a set $S_i (\subset \mathbb{R})$ which depends on $a_i$ and I can choose $a_{i+1}$ from $S_i$.

The tricky part that every $S_i$ is dependent on $a_i$. If $S_i$ doesn't depend on $a_i$, we have a choice function. However, in this case, how can we know there is a choice function which guarantees the existence of the sequence $\{a_n\}$? (The source of this question is in the following.)

 A: NOTE: the first two parts of the answer address the original version of the problem, where $\mathbb{R}$ was replaced with $\mathbb{N}$. There's still interesting material there, so I'm leaving those parts, but for the question as edited see the final section.

Generalizing a bit, what you have is a next option function $$F: \mathbb{N}^{<\mathbb{N}}\rightarrow\mathcal{P}(\mathbb{N})$$ sending a given sequence $(a_1,...,a_n)$ to the set of "allowed next numbers" (and let's say for simplicity that when $(a_1,...,a_n)$ itself is illegal we have $F((a_1,...,a_n))=\mathbb{N}$ - nothing is less legal that things already are).
Robert Shore's comment makes a key observation: since we're always picking from a well-ordered set (namely, $\mathbb{N}$) we can make our choices ahead of time: letting $$G:\mathbb{N}^{<\mathbb{N}}\rightarrow\mathbb{N}: (a_1,...,a_n)\mapsto \min(F((a_1,...,a_n))),$$ we have that $G((a_1,...,a_n))$ is always a "legal next choice" whenever $(a_1,...,a_n)$ is a "legal sequence so far."

That gets rid of the choicey flavor, and reveals the actual content: recursion. We want to define the sequence 


*

*$a_1=G(\langle\rangle)$,

*$a_{n+1}=G(\langle a_1,..., a_n\rangle)$,
but that isn't an "all at once" definition and might feel weird at first.
This is where the recursion theorem kicks in: this is a result in set theory which says that we can in fact make sense of "definitions" like this. A special case of it (which is enough for your purposes here) is given at wikipedia; its more general form is the following:

(Almost-fully-general recursion theorem) Suppose $\alpha$ is an ordinal, $X$ is a set, and $$I: X^{<\alpha}\rightarrow X$$ is a function. Then there is a unique $$f: \alpha\rightarrow X$$ (more intuitively, $f=(a_i)_{i\in\alpha}$ with each $a_i$ in $X$) such that for all $\beta<\alpha$ we have $$f(\beta)=I(f\upharpoonright\beta).$$

As the title indicates, we can generalize a bit further ... but meh. Also, be careful not to confuse this with the recursion theorem in computability theory or the master/recursion theorem in theoretical computer science and combinatorics.
Here $I$ is our "iterator" telling us what to add to our "sequence-so-far," and $f$ is the "completed sequence" we want.
The axiom(s) which makes the recursion theorem work is the axiom (scheme) of replacement. This is in many ways more powerful than choice, e.g. in terms of consistency strength: ZFC is consistent if ZF is, but ZF proves the consistency of Z (= ZF without replacement) and so in principle ZF could be inconsistent even if Z is consistent.
Indeed, set theory without replacement is an incredibly finicky thing, as a quick glance at this will indicate.

Going back to the choice issue, what happens if we replace $\mathbb{N}$ with some more complicated set $X$, so that the "least element" trick need not apply?
In this case we're in the realm of dependent choice principles; these are strictly weaker than choice, but still not provable from ZF alone. The usual axiom of dependent choice, DC, handles the case when we want to make $\omega$-many choices, but we also have stronger dependent choice axioms for "longer" processes, and there are some subtleties around these.
That said, we often can get away without choice by being a bit clever. This is along the lines of Robert Shore's original comment: although a choice function for arbitrary subsets of $\mathbb{R}$ need not exist without choice, the particular situation we're looking at may admit one. This is often the case in topology, at least as concerns "simple" properties of "nice" spaces - for example, it's often enough to pick rational numbers instead of real numbers, and $\mathbb{Q}$ is (provably in ZF) well-orderable.
