Let $V$ be a vector space over a local field$K$ (usually $\mathbb{R}$ or $\mathbb{C}$), equipped with a seminorm$p: V \to [0, \infty)$. Let $W \subseteq V$ be a subspace, and $f: W \to K$ a linear functional such that ${|f(x)|} \leq p(x)$ for all $x \in W$, then there exists an extension of $f$ to a linear functional $g: V \to K$ such that ${|g(x)|} \leq p(x)$ for all $x \in V$.

The Hahn-Banach theorem can be proven in set theory with the axiom of choice, or more weakly in set theory assuming the ultrafilter theorem, itself a weak form of choice. (To be continued…)

However, the Hahn–Banach theorem for separable spaces is much weaker. It may be proved constructively using only dependent choice. There is also a version of the theorem for locales (or so I heard).