## Is there an infinite-dimensional Banach space with a compact unit ball?

A popular pair of exercises in first courses on functional analysis prove the following theorem:

The unit ball of a Banach space $X$ is compact if and only if $X$ is finite-dimensional.

My question is, is the "only if" part of this (i.e., that the unit ball of an infinite-dimensional Banach space is noncompact) necessarily true without some form of the axiom of choice? The usual proof uses the Hahn--Banach theorem, which may reasonably be regarded as a weak form of the axiom of choice (see this answer, and other answers to the same question, for some interesting points related to this).

-
It would be sufficient to know that $X$ contains a sequence $(E_n)$ of finite dimensional subspaces whose dimensions tend to infinity. Must such a sequence exist in the absence of AC? – Bill Johnson Oct 10 2011 at 21:55
Note that it is important to take a specific notion of compactness, since in the absence of choice the usual notions may not longer be equivalent. For instance, in N. Brunner's article "Sequential compactness and the axiom of choice" (available online), it is mentioned that the statement "A Hilbert space is finite dimensional iff its closed unit ball is compact" is provable in ZF without choice (even without foundation), but that such a result may no longer be valid in case of sequential compactness. – godelian Oct 10 2011 at 22:30
For all members $p$ of $[1,\scriptsize{+}\normalsize{\infty}]$, $\; \ell^p($amorphous set$) \;$ is an infinite dimensional Banach space without a sequence of finite dimensional subspaces whose dimensions are unbounded. $\hspace{1.25 in}$ – Ricky Demer Oct 10 2011 at 22:33

Let me try a possible answer. Take a model of $ZF$ where the axiom of choice for a denumerable family of finite sets holds but where there is an infinite Dedekind finite set $B$ (this model can be checked to exist, for instance, here; $\mathcal{M}32$ is one such model). Then $\ell_2(B)$ is an infinite dimensional Hilbert space with a Dedekind finite orthonormal base, whose unit ball is, by theorem 2 of the previously cited article, sequentially compact.