It is stated that the Hahn-Banach theorem can be proved without the need of the axiom of choice when the vector space is separable. A supposed proof is here, from where I quote
- If $X$ is separable and $\{x_n; n\in\mathbb N\}$ is a countable dense subset of $X$, then we can prove using induction and the above lemma that there exists a linear functional $f_n$ defined on $A_n=[M\cup\{x_1,\dots,x_n\}]$ which agrees with $f$ on $M$ and is dominated by $p$ on $A_n$. Moreover, each $f_n$ extends $f_{n-1}$.
I cannot understand how this proof doesn't use the axiom of choice when it have an enumeration of an infinite countable subset. I had read this other question making the same question as Im doing here, but the comments on it doesn't make clear that we are not using the axiom of choice in an enumeration like in the set $\{x_n:n\in \Bbb N \}$. As far as I understand to enumerate an infinite countable set, or build recursively a sequence from this set, we need to make infinite countable choices from infinite countable subsets. In other words: I dont see a way to do it without making infinite choices on infinite sets.
Can someone explain in detail how we can make such an enumeration without the axiom of choice? Thank you in advance.