I was reading about the Hahn-Banach Theorem, its many versions and their proofs. It's known that in the proofs we need Zorn's Lemma. But in the book that I'm reading, the author said if $X$ is a separable space then it's possible to prove the Hahn-Banach Theorem without the Zorn's Lemma.
How can we show there is a suitable extension of a linear functional without Zorn's lemma?
Note: I completely rewrote my previous attempt - posted in another (now deleted) answer, since the previous version was incorrect. Thanks to Asaf Karagila for pointing out the problem with my previous proof. And also to Eric Wofsey for simplifying some steps in the proof.
Let us hope that this time I have avoided mistakes. The formulation of the version of HBT which I am trying to prove in ZF is adapted from the claims mentioned in this paper. Some remarks explaining what this paper proves about the relation between ZF, AC and HBT for separable spaces can be found below.
As the OP wrote, there are several formulations of Hahn-Banach Theorem. So maybe it is good to start by clearly stating this result.
The formulation that $f$ is dominated by $p$ on $M$ means that $(\forall x\in M) f(x)\le p(x)$.
This is basically the usual formulation of Hahn-Banach Theorem; although you can find many slight variations.
We will try to prove this in ZF:
You may notice that this implies that every bounded functional on a subspace $M$ of a separable normed space $X$ can be extended to a functional on $X$ with the same norm. This is is the version of HBT stated here.
Notice a few changes in the formulation of the theorem. Since we want to speak about separable spaces, we need some kind of topology. So it is not that surprising that we work now with topological vector spaces. Maybe it is a little bit surprising that we require $p$ to be continuous. (On the other hand, if we want to use separability, then it is perhaps natural that we will probably use somewhere in the proof that $p$ behaves reasonable w.r.t. the topological structure.) But let us try to prove this version first. We will return to the question, whether continuity of $p$ is needed, later.
The standard proof of HBT uses as one of the steps the following fact:
Now we can prove this version of HBT in the following steps:
Let us have a closer look at a more detailed proof of existence and uniqueness of the above limit. (Since this is precisely the place where my previous attempt failed.)
It is worth pointing out that we repeatedly use continuity of $p$. To be more precise, we use $p(a_n)\to p(x)$.
We will use rather simple observation that $g(x)=-g(-x)\ge -p(-x)$, so we have $$-p(-x)\le g(x) \le p(x)$$ for any $x\in A$. Now if we have a sequence $a_n\to x$, we can use the inequality $$-p(a_n-a_m) \le g(a_m-a_n) \le p(a_m-a_n)$$ to show that the sequence $(g(a_n))$ is Cauchy sequence in $\mathbb R$, and therefore it has a limit. Similarly if we have $a_n\to a$ and $b_n\to a$, we can use $$-p(b_n-a_n)\le g(a_n-b_n) \le p(a_n-b_n)$$ to show that $\lim g(a_n)=\lim g(b_n)$.
Putting all things mentioned above together we get the proof of the above result.
Would it be possible to prove stronger result - to omit condition that $p$ is continuous and just leave the sublinearity? The answer is no, which shows that these problems might be a bit more subtle than they could appear on the first glance. It is shown in the paper Juliette Dodu and Marianne Morillon: The Hahn-Banach Property and the Axiom of Choice (Mathematical Logic Quarterly, Volume 45, Issue 3, pages 299–314, 1999, DOI: 10.1002/malq.19990450303) that if every separable normed space satisfies the Hahn-Banach property (i.e., if the above theorem holds without the assumption that the sublinear function $p$ is continuous), then there are non-trivial finitely-additive measures on the set of positive integers. Therefore this result cannot be shown in ZF. (See Theorem 6 and Corollary 4 in Section 9 of this paper for details.)
The authors also say the following:
The "classical lemma" mentioned there is the lemma I formulated above. And if the dense subset is countable, then this is the above claim (for which I tried at least to sketch a proof).
If $X$ is not separable, then the argument above cannot be used to get a function $\widehat f$ defined on the whole space $X$. But the usual proof of Hahn-Banach Theorem is along the same lines, we just use Zorn's Lemma or transfinite induction instead of mathematical induction. (Zorn's lemma is known to be equivalent to the Axiom of Choice. The proof based on transfinite induction uses AC too, since we start by choosing some well-ordering of $X$. Well-ordering theorem is equivalent to AC.)
The only step in which the above proof and the usual proof of HBT differ substantially is the extensions from a dense subspace to the whole space. This is the point of the proof where we used continuity of the sublinear function $p$. (And this condition is not needed if AC is available.)