Hahn-Banach without Choice The standard proof of the Hahn-Banach theorem makes use of Zorn's lemma. I hear that, however, Hahn-Banach is strictly weaker than Choice. A quick search leads to many sources stating that Hahn-Banach can be proven using the ultrafilter theorem, but I cannot seem to find an actual proof. So...


*

*What is the ultrafilter theorem; and

*How does the said theorem imply the Hahn-Banach theorem?


Any easily-accessible reference would be quite enough; thanks in advance!
 A: Since I can't (yet) leave a comment to Andres Calceido's answer.
A link to another paper by Luxemburg with a proof of the Hahn-Banach Theorem using ultrapowers https://www.ams.org/bull/1962-68-04/S0002-9904-1962-10824-6/S0002-9904-1962-10824-6.pdf
A: The ultrafilter theorem is the statement that any filter on a set can be extended to an ultrafilter. It is perhaps more common to see it sated as the (Boolean) Prime ideal theorem: Every Boolean algebra admits a prime ideal. 
The Hahn-Banach theorem is actually equivalent to the statement that every Boolean algebra admits a real-valued measure, but this is not entirely straightforward (see Luxemburg, "Reduced powers of the real number system and equivalents of the Hahn-Banach extension theorem", Intern. Symp. on the applications of model theory, (1969) 123-127).
For a discussion of Hahn-Banach vs. Choice and some additional remarks and references, see Jech "The axiom of choice", North-Holland, 1973.
You may also be interested in the references I include in this answer. 
A: An amusing related fact is that the non linear Hahn-Banach theorem (that every Lipschitz one function into the reals from a subset of a metric space can be extended to a Lipschitz one function on the entire space) is provable in ZF.  I believe it is proved this way in the book of Araujo and Gine. 
A: This might be irrelevant, but I would like to point out that if one
restates Hahn-Banach theorem in the language of locales (replacing topological spaces),
one can get rid of the axiom of choice and the ultrafilter theorem altogether.
See the paper “A Direct Proof of the Localic Hahn-Banach Theorem” by Thierry Coquand
and references therein.
A: https://en.wikipedia.org/wiki/Hahn%E2%80%93Banach_theorem#Relation_to_axiom_of_choice (current revision)

As mentioned earlier, the axiom of
  choice implies the Hahn–Banach
  theorem. The converse is not true. One
  way to see that is by noting that the
  ultrafilter lemma, which is strictly
  weaker than the axiom of choice, can
  be used to show the Hahn–Banach
  theorem, although the converse is not
  the case. The Hahn–Banach theorem can
  in fact be proved using even weaker
  hypotheses than the ultrafilter
  lemma.[4] For separable Banach spaces,
  Brown and Simpson proved that the
  Hahn–Banach theorem follows from WKL0,
  a weak subsystem of second-order
  arithmetic.[5]

