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.
Best Answer
Suppose that $C(x)$ is the following formula (expressible in the language of first order theory of sets)
$$x\,\mbox{ is a enumeration of a countable dense subset of a fixed normed space }X$$
I think (maybe other users can correct me) that there is the following theorem of the first order logic:
$$\exists_xC(x)\rightarrow \left(\left(C(s)\rightarrow T\right)\rightarrow T\right)$$
where $T$ is any sentence of the first order set theory. So if we pick as $T$ a statement of Hahn-Banach theorem for $X$ (expressed in the language of first order set theory) and provided that we have proved before that $C(s)\rightarrow T$, then by modus ponens we have proved $T$. All steps without invoking axiom of choice.
This boils down to say that we have valid deduction
$$C(s)\rightarrow T, \exists_xC(x), \exists_xC(x)\rightarrow \left(\left(C(s)\rightarrow T\right)\rightarrow T\right)\vdash T$$
and all three premises are proved without AC. Is that correct (Asaf Kagila can you please help me)? I am not an expert in logic.
Edit.
Moreover, $C(s)\rightarrow T$ is just the same as proving Hanh-Banach theorem for $X$ with the assumption that $s$ is a fixed enumeration of a countable dense subset of $X$. So $s$ is of the form $\{x_n\}_{n\in \mathbb{N}}$ and this sequence is dense in $X$. You want to prove from this HB for $X$.