Spectra of elements of a Banach algebra and the role played by the Hahn-Banach Theorem. This problem was posed on Math StackExchange some time ago, but it did not garner any solutions there. I think that it is interesting enough to be posed here on Math Overflow, so here it goes.
Let $ \mathcal{A} $ be a unital Banach algebra over $ \mathbb{C} $, with $ \mathbf{1}_{\mathcal{A}} $ denoting the identity of $ \mathcal{A} $. For each $ a \in \mathcal{A} $, define the spectrum of $ a $ to be the following subset of $ \mathbb{C} $:
$$
{\sigma_{\mathcal{A}}}(a) \stackrel{\text{def}}{=} \lbrace \lambda \in \mathbb{C} ~|~ \text{$ a - \lambda \cdot \mathbf{1}_{\mathcal{A}} $ is not invertible} \rbrace.
$$
With the aid of the Hahn-Banach Theorem and Liouville's Theorem from complex analysis, one can prove the well-known result that $ {\sigma_{\mathcal{A}}}(a) \neq \varnothing $ for every $ a \in \mathcal{A} $. All proofs that I have seen of this result use the Hahn-Banach Theorem in one way or another (a typical proof may be found in Walter Rudin's Real and Complex Analysis). Hence, a natural question to ask would be: Can we remove the dependence of this result on the Hahn-Banach Theorem? Is it a consequence of ZF only? Otherwise, if it is equivalent to some weak variant of the Axiom of Choice (possibly weaker than the Hahn-Banach Theorem itself), has anyone managed to construct a model of ZF containing a Banach algebra that has an element with empty spectrum?
 A: I do not believe that the Hahn-Banach theorem is necessary. At some point I had planned on writing up a blog post verifying this but I lost the motivation... 
The idea is that you can prove Liouville's theorem in the Banach space setting directly without using Hahn-Banach to reduce to the case of $\mathbb{C}$ (I asked whether this was possible in this math.SE question). Most of the steps in the proof are exactly the same; the only one that isn't, as far as I can tell, is the fundamental theorem of calculus, which is usually proven using the mean value theorem but which can instead be proven following the answers to this math.SE question. 
A: I think Hahn-Banach can be eliminated from the usual proof, but
being a non-expert in set theory, I cannot guarantee that the proof
is completely independent of the axiom of choice.
Here is a sketch of a basic calculus proof. A function $U\to B$ 
from a region $U\subset C$ to a Banach space $B$ is called analytic if
every point has a neighborhood where it is represented by a
convergent Taylor series.
You can prove a weak form of Cauchy theorem which says that if a function
is analytic in 
$| z |  < R \leq \infty$
 then its Taylor series
has radius of convergence at least $R$. It seems that this does not
use the axiom of choice.
Then you prove that Cauchy inequalities hold (there is a simple algebraic
proof of this, see my answer to Liouville's theorem with your bare hands), and derive the Liouville theorem for Banach-space-valued
functions.
Then again it is an elementary fact that if $a-\lambda_0 1$ has
has a bounded inverse then the resolvent is an analytic function (in the sense I defined above) in
a neighborhood of $\lambda_0$. Then you show that if the resolvent exists everywhere
then it tends to $0$ as $\lambda\to\infty$. Then it seems to me that you obtain a proof
without Hahn-Banach by applying the Liouville theorem to the resolvent.
Sorry if I missed something...
EDIT. The weak form of Cauchy's theorem that I mentioned uses only elementary manipulation with absolutely convergent series, no integral is involved, see
Liouville's theorem with your bare hands.
A: There is a proof without using even complex analysis, and at first glance without using AC. We replace Cauchy integral formula by clever finite sums. Namely, we define the spectral radius as $r(a):=\lim \|a^n\|^{1/n}$ (the limit exists by Fekete lemma), by scaling it suffices to consider two cases: $r(a)=0$ and $r(a)=1$. In the first case $a$ is not invertible, since if $ab=1$, then $a^nb^n=1$ and $\|a^n\|\cdot \|b\|^n\geqslant 1$, thus $r(a)\geqslant 1/\|b\|$. If $r=1$, we prove that there exist $\lambda$ on the unit circle such that $a-\lambda$ is not invertible. Assume the contrary, then by continuity of the inverse and compactness of the circle we get $\|(a-\lambda)^{-1}\|\leqslant M$ for all $\lambda$ on the unit circle and certain $M>0$. Now we use the rational functions identity $$n^2 a^{n-1}=(1-a^n)^2\sum_{w:w^n=1}w(a-w)^{-2}$$
and take the spectral radius of both right and left hand sides. By using the easy equalities and inequalities $r(u^n)=(r(u))^n$, $r(uv)\leqslant r(u)\cdot \|v\|$, $r(1+u)\leqslant 1+r(u)$ for commuting $u,v$ we see that $r(n^2a^{n-1})=n^2$ while $r(RHS)=O(n)$. A contradiction.
I read this proof in the paper of E. Gorin, who says that it is a simplification of the proof in [Rickart C. E. General Theory of Banach Algebras. Princeton NJ, D. van Nostrand (1960).]
