Which set existence axioms are needed to prove the separable Hahn-Banach theorem? (Q1820779)

The authors work in the context of weak subsystems of second order arithmetic. \(RCA_ 0\) is the system with \(\Delta^ 0_ 1\) comprehension and \(\Sigma^ 0_ 1\) induction. \(WKL_ 0\) is \(RCA_ 0\) plus weak König's lemma for trees of finite sequences of 0's and 1's. It is shown that the Hahn-Banach theorem for separable Banach spaces is equivalent to \(WKL_ 0\) over \(RCA_ 0\). To prove the separable Hahn- Banach theorem within \(WKL_ 0\), one has to refine the usual proof which uses the \(\omega\)-times iterated arithmetical comprehension axiom. For the other direction, the authors make use of ideas of Bishop, Metakides, Nerode and Shore. The paper is well-written and gives just the right amount of detail. However, in a number of places the reader is referred to the PhD Thesis of the first author and a forthcoming book of the second author.