I'd like to summarize the answer that has developed from Eric Shechter's book, via Mark Meckes, plus the remark from Gerald Edgar. Since it's not really my answer, I'm making this a community answer.
The Hahn-Banach theorem is really the Hahn-Banach axiom. Like the axiom of choice, Hahn-Banach cannot be proved from ZF. What Hahn and Banach proved is that AC implies HB. The converse is not true: Logicians have constructed axiom sets that contradict HB, and they have constructed reasonable axioms strictly between AC and HB. So a version of Andrew's question is, is there a natural Banach space that requires the HB axiom? For the question, let's take HB to say that every Banach space $X$ embeds in its second dual
As Shechter explains, Shelah showed the relative consistency of ZF + DC + BP (dependent choice plus Baire property). By As he also explains, these axioms , imply that
$(\ell^\infty)^* = \ell^1$. This is contrary to the Hahn-Banach theorem as explained in the next point. A jarring striking way to phrase the conclusion is that $\ell^1$ and its dual $\ell^\infty$ are become reflexive Banach spaces.
$c_0$is the closed subspace of $\ell^\infty$ consisting of sequences that converge to 0. The quotient
$\ell^\infty/c_0$is an eminently natural Banach space in which the norm of a sequence is $\max(\lim \sup,-\lim \inf)$. (Another example is $c$, the subspace of convergent sequences. In $\ell^\infty/c$, the norm is half of $\lim \sup - \lim \inf$.) The inner product between $\ell^1$ and
$c_0$is non-degenerate, so in Shelah's axiom system,
$(\ell^\infty/c_0)^* = 0$. Without the Hahn-Banach axiom, the Banach space
$\ell^\infty/c_0$need not have any non-zero bounded functionals at all.