Banach Space Theory

Regarding the reverse mathematics status of well known theorems of functional analysis, much is known, but many questions remain.

For example, the open mapping theorem for separable Banach spaces is known to be provable in a system called $\mathsf{RCA}_0^{+}$ which is of the same strength as $\mathsf{RCA}_0$ and indeed conservative over $\mathsf{RCA}_0$ for $\Pi^1_1$sentences. But whether it is provable in $\mathsf{RCA}_0$ or even $\mathsf{WKL}_0$remains unknown. See Brown/Simpson [5], Mytilinaios/Slaman [24], Simpson [31].

As another example, consider the Krein/Smulian theorem for separable Banach spaces. This is a somewhat lesser known but still basic theorem of functional analysis. It says that a convex set in the dual of a separable Banach space is weak- ${*}$-closed if and only if it is bounded-weak- ${*}$-closed. It is known from Humphreys/Simpson [16] that this statement is provable in $\mathsf{ACA}_0$, but the exact strength is unknown.