Metrization of Proper MF 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 in second-order arithmetic over $\mathsf{RCA}_0$, the base theory with $\Delta^0_1$ comprehension and $\Sigma^0_1$ induction. The strength of a principle means which subsystems prove it and which subsystems it implies over that base; equivalence requires both implications. For a countable partially ordered set $(P,\leq)$, a filter is a nonempty upward-closed subset directed downwards: any two of its elements have a common lower bound in the filter. The space $\operatorname{MF}(P)$ has as points the filters maximal under inclusion, with basic open sets $N_p=\{F:p\in F\}$. The presentation is proper when $p\leq q\iff N_p\subseteq N_q$ and, whenever $p,q$ are compatible (have a common lower bound), some $r\in P$ satisfies $N_r=N_p\cap N_q$. Regularity means that a point and a closed set not containing it have disjoint open neighbourhoods. Metrizability means existence of a metric inducing the topology.

Statement recorded in the supplied source.

What is the reverse-mathematical strength of the statement that every proper MF space is metrizable if and only if it is regular? [S2]

Short English statement

Which set-existence axioms are required for regularity to characterize metrizable spaces in the proper maximal-filter presentation?

Sources

• S1 ULAM.AI and the UnsolvedMath Contributors, UnsolvedMath: A Curated Collection of Open Mathematics Problems, record 7500115 (AMR-074-0115). CC BY 4.0. https://huggingface.co/datasets/ulamai/UnsolvedMath.
• S2 Antonio Montalbán, Open Questions in Reverse Mathematics, author preprint dated 17 August 2010, Question 15, printed p. 7. https://math.berkeley.edu/~antonio/papers/questionsRM.pdf.