2 Clearer phrasing

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.

1. 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 $X^{**}$.

2. 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.

3. $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.

1. 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 $X^{**}$.
2. As Shechter explains, Shelah showed the relative consistency of ZF + DC + BP (dependent choice plus Baire property). By these axioms, $(\ell^\infty)^* = \ell^1$. This is contrary to the Hahn-Banach theorem as explained in the next point. A jarring way to phrase the conclusion is that $\ell^1$ and its dual $\ell^\infty$ are reflexive Banach spaces.
3. $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.