Open Mapping Theorem for Separable Banach Spaces

Definitions and mathematical statement

Shared notation.

$\mathbb N=\{1,2,\ldots\}$, and $\mathbb Z,\mathbb Q,\mathbb R,\mathbb C$ denote the integers, rationals, reals and complex numbers. Any other conventions are specified locally.

Work over $\mathsf{RCA}_0$, the subsystem of second-order arithmetic with $\Delta^0_1$ comprehension and $\Sigma^0_1$ induction; all structures and orders are countable and coded by sets of integers. $\mathsf{ACA}_0$ adds comprehension for every arithmetical formula (set parameters allowed), and $\mathsf{ATR}_0$ adds arithmetical transfinite recursion along every coded well-order. Reverse-mathematical equivalence means provability of both implications over this base. $\mathsf{WKL}_0$ adds the assertion that every infinite binary tree has an infinite path. A separable Banach space is a complete normed real vector space with a countable dense set. For a bounded linear surjection $T:X\to Y$ between such spaces, the open mapping theorem asserts that $T$ sends every norm-open set to a norm-open set; equivalently there is $\delta>0$ with $B_Y(0,\delta)\subseteq T(B_X(0,1))$.

Statement recorded in the supplied source.

Is this separable open mapping theorem provable in $\mathsf{RCA}_0$? Is it provable in $\mathsf{WKL}_0$? [S2]

Short English statement

Determine whether either recursive comprehension alone or weak König's lemma suffices for the open mapping theorem on separable Banach spaces.

Sources

• S1 ULAM.AI and the UnsolvedMath Contributors, UnsolvedMath: A Curated Collection of Open Mathematics Problems, record 7500204 (AMR-074-0204). CC BY 4.0. https://huggingface.co/datasets/ulamai/UnsolvedMath.
• S2 Stephen G. Simpson, Open Problems in Reverse Mathematics (15 December 1999), Banach Space Theory, first example. https://sgslogic.net/t20/talks/cta/problems/node3.html.