Giusto–Simpson conjecture on the reverse-mathematical strength of strong Tietze extension

Let $X$ be a compact complete separable metric space, let $C$ be a closed subset of $X$, and let $f\colon C\to\mathbb{R}$ be a continuous function with a modulus of uniform continuity. A corresponding extension is a continuous function $F\colon X\to\mathbb{R}$ with a modulus of uniform continuity that extends $f$; in the separably closed variant, “closed” means “closed and separably closed.”

Giusto–Simpson conjecture. The following are equivalent over $\mathsf{RCA}_0$:

$$\mathsf{WKL}_0;$$

the strong Tietze extension theorem for closed sets; the strong Tietze extension theorem for closed and separably closed sets; the special case of the former with $X=[0,1]$; and the special case of the latter with $X=[0,1]$.

The conjecture identifies the precise reverse-mathematical strength of the unresolved forms of the strong Tietze extension theorem. The paper records that the strong theorem for separably closed sets is equivalent to $\mathsf{WKL}_0$, while the strong theorem for closed sets is provable in $\mathsf{WKL}_0$ and the version for closed and separably closed sets is not provable in $\mathsf{RCA}_0$; the equivalences asserted above are the remaining conjectural classification.