Everybody knows arguments like:
"We can construct such a sequence inductively. Let $a_0$ be chosen as [..]. Then we can choose $a_{k+1}$ out of the set $A_{k+1}$ (which was shown to be non-empty)."
Or
"We can construct this sequence inductively. Let $a_0$ be chosen as [..]. Then we define $a_{k+1}=f(a_k)$"
What does it formally mean to "construct" a sequence? It is intuitively clear, but I wonder how this procedure of constructing something is translated to set theory and formal logic. Especially in the first case, it seems to me like the axiom of choice is needed, and since no one ever mentioned that in my beginner classes, I wonder if there is even more behind this that you simply don't think about when you just want to do maths.
The first case requires Countable Choice in general as it can be easily reformulated to give a choice function for a countable collection of nonempty sets.
For the second case (i.e. with a functional predicate $f$ given), choice is not required. Let $X$ be the set of natural numbers $n$ such that there exists a set $Y_n$ and a function $\alpha_n\colon\{0,\ldots,n\}\to Y_n$ such that $\alpha_n(0)=a_0$ and $\alpha_n(k+1)=f(a_k)$ for all $k<n$. Then by induction we can readily show that $X=\mathbb N$. Next, letting $a_k=\alpha_n(k)$ for arbitrary $n\ge k$ turns out to be well-defined and give a sequence as required.