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.


If a set is countable, then by definition there is an injection of that set into the natural numbers.

Therefore, there is provably an injection into an initial segment of the natural numbers.

Therefore, we can enumerate the set by setting $x_n$ as the unique member of the set mapped to $n$, if such exists. If the set is infinite, then indeed that $x$ exists.


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.


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$.

  • $\begingroup$ Apparently the question is not at all about HBT (despite the title and the choice of tags), rather a remark made in the proof... $\endgroup$ – Asaf Karagila Oct 24 at 13:11
  • $\begingroup$ Yes, I think you are write and the question concerns first order logic. $\endgroup$ – Slup Oct 24 at 13:15
  • $\begingroup$ I changed the title, sorry for the confusion. Anyway it is advised to read the body of the question (and not just the title) before to write an answer $\endgroup$ – Masacroso Oct 24 at 13:15
  • $\begingroup$ Ok. It is fine. Now you have two answers and I think that both are correct. $\endgroup$ – Slup Oct 24 at 13:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.