Computability of the Hahn-Banach Theorem Revisited
This work addresses foundational issues in computable analysis and reverse mathematics for mathematicians and logicians, providing incremental refinements to existing complexity results.
The paper tackles the computational complexity of the Hahn-Banach theorem, showing that it attains its full complexity for the Banach space ℓ¹ and proving equivalences to other theorems like the intermediate value theorem and the lesser limited principle of omniscience, with a new simple proof for reduction to weak König's lemma.
Computational properties of the Hahn-Banach theorem have been studied in computable, constructive and reverse mathematics and in all these approaches the theorem is equivalent to weak KÅnig's lemma. Gherardi and Marcone proved that this is also true in the uniform sense of Weihrauch complexity. However, their result requires the underlying space to be variable. We prove that the Hahn-Banach theorem attains its full complexity already for the Banach space $\ell^1$. We also prove that the one-step Hahn-Banach theorem for this space is Weihrauch equivalent to the intermediate value theorem. This also yields a new and very simple proof of the reduction of the Hahn-Banach theorem to weak KÅnig's lemma using infinite products. Finally, we show that the Hahn-Banach theorem for $\ell^1$ in the two-dimensional case is Weihrauch equivalent to the lesser limited principle of omniscience.