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 '11 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 '11 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 '11 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.

-

I am a bit surprised. Perhaps I have misunderstood the question, but the standard proof of the OP's question does not rely upon the HB Theorem, but rather simply on Riesz' Lemma - in whose proof in turn I do not see any application of the AoC.

-
The Riesz lemma itself holds true without the axiom of choice. But you will apply it countably many times to choose an "almost orthonormal" sequence of vectors. On the face of it this seems to require an application of the axiom of countable dependent choice: en.wikipedia.org/wiki/Axiom_of_dependent_choice –  Martin Jun 14 '13 at 21:05
It seems to me that a key point here might be the difference between compactness and sequential compactness, at least in Hilbert spaces such as in godelian's example. Let $H$ be a Hilbert space and $\{e_\alpha \colon \alpha \in A\}$ an orthonormal basis. The set $\{e_\alpha\}$ is clearly closed, so its complement in the closed unit sphere $S$ - call this complement $U_0$ - is open. Each of the sets $U_\alpha:=\{x \in S \colon \|x-e_\alpha\|<1\}$ is also open, and the collection of all the $U_\alpha$'s together with $U_0$ is an open cover without a finite subcover. –  Ian Morris Jun 14 '13 at 21:09
Martin's comment is indeed correct. Dependent choice fails in the model described in my answer. I also agree with Ian's comment, see also my comment to the post above. –  godelian Jun 14 '13 at 22:03
@Ian: How do you construct an orthonormal basis without AC? The usual construction uses Zorn's lemma to produce a maximal orthonormal set. –  Nate Eldredge Jun 15 '13 at 14:05
Delio: You're right, I was overlooking that you don't need HB to prove Riesz. But as Martin says, Riesz needs to be applied an infinite number of times, requiring dependent choice. –  Mark Meckes Jun 20 '13 at 15:51