Separable Banach space theory needs strong set existence axioms

We investigate the strength of set existence axioms needed for separable Banach space theory. We show that a very strong axiom, $\Pi ^1_1$ comprehension, is needed to prove such basic facts as the existence of the weak-$*$ closure of any norm-closed subspace of $\ell _1=c_0^*$. This is in contrast to earlier work in which theorems of separable Banach space theory were proved in very weak subsystems of second order arithmetic, subsystems which are conservative over Primitive Recursive Arithmetic for $\Pi ^0_2$ sentences. En route to our main results, we prove the Krein-\v{S}mulian theorem in $\mathsf {ACA}_0$, and we give a new, elementary proof of a result of McGehee on weak-$*$ sequential closure ordinals.