Over ZF, does "every Hilbert space have a basis" imply AC?
According to the book Albrecht Pietsch: History of Banach Spaces and Linear Operators (Birkhäuser, 2007, DOI: 10.1007/978-0-8176-4596-0) this is an open problem. (Or at least it was at the time of publishing the book.)
I quote from p.586:
We list two more consequences of the axiom of choice, which have already been discussed in 1.2.2 and 1.5.10, respectively:
$(\mathsf{B}_{\mathsf{alg}})$ Every real or complex linear space has a Hamel basis.
$(\mathsf{B}_{\mathsf{orth}})$ Every real or complex Hilbert space has an orthonormal basis.It is unknown whether $(\mathsf{B}_{\mathsf{alg}}) \overset{?}\Rightarrow (\mathsf{AC})$ or $(\mathsf{B}_{\mathsf{orth}}) \overset{?}\Rightarrow (\mathsf{AC})$. Some partial results were obtained by Bleicher [1964] and Halpern [1966]. Blass [1984, p. 31] showed that the axiom of choice follows if we assume that every linear space over an arbitrary field has a basis.
- J.D. Halpern [1966] Bases in vector spaces and the axiom of choice, Proc. Amer. Math. Soc. 17, 670–673. DOI: 10.1090/S0002-9939-1966-0194340-1
- M.N. Bleicher [1964] Some theorems on vector spaces and the axiom of choice, Fund. Math. 54, 95–107. eudml, matwbn
- A. Blass [1984] Existence of basis implies the axiom of choice, Contemp. Math. 31, 31–33. author's website