Urysohn's lemma is not a theorem of ZF, nor of ZF plus countable choice

Urysohn's lemma (UL). If $X$ is a $T_4$ space and $A, B \subseteq X$ are disjoint closed sets, there is a continuous $f : X \to [0,1]$ with $A \subseteq f^{-1}(\{0\})$ and $B \subseteq f^{-1}(\{1\})$.

The following are all relative to the consistency of ZF.

(a) UL is not a theorem of ZF. Läuchli (1962/63) builds a permutation model of ZF with atoms in which the set of atoms is densely linearly ordered, of the order type of the rationals of the ground model, and in which that set with its order topology is a $T_4$ space on which every continuous real-valued function is constant; UL fails there. Since the negation of UL is a boundable statement, the Jech-Sochor first embedding theorem transfers the failure to ZF proper.

(b) UL is not a theorem of ZF + countable choice. Tachtsis (2019) produces a model of ZF in which $\mathrm{AC}_\omega$ holds and UL fails, and hence in which the Tietze extension theorem fails as well.

(c) What does suffice. Dependent choice implies UL by the usual dyadic construction. Blass (1979) proves the stronger statement that dependent multiple choice implies UL. Whether UL implies DMC is open.

(d) The Boolean prime ideal theorem does not suffice. Brunner (1983) shows UL fails in the Mostowski linearly ordered model, where BPI holds; Pincus's transfer theorems carry this to ZF.

• Not proved in this library. None of (a) to (d) is proved here. Even the positive direction, that DC implies UL, is not proved here, because the library has no topology track yet at the point where this page sits.

• What would prove it. For (a), (b) and (d): permutation models of ZF with atoms, plus the Jech-Sochor and Pincus transfer theorems, that is, the same track named in Cohen 1963: ZF does not prove the Axiom of Choice ‡. For (c): the tree combinatorics behind DMC, the same principle that appears in The Baire category theorem is four inequivalent statements over ZF ‡.

• Why it matters here. Urysohn's lemma is the workhorse of every separation and metrisation argument, and it looks like pure point-set topology. It is not: the usual proof indexes a family of open sets by the dyadic rationals and chooses one at each stage in terms of the previous stage, which is dependent choice. Any page in this library that proves Urysohn's lemma, Tietze extension, or a metrisation theorem must therefore record a choice principle in The choice ledger: what costs the Axiom of Choice and what does not ↗, and must not claim the argument is free merely because it never mentions a well-ordering. Note that the weakest standard principle, The Axiom of Countable Choice ($\mathrm{AC}_\omega$) ↗, is provably not enough, by (b).

• Conditional discipline. Clauses (a), (b) and (d) are relative to the consistency of ZF; clause (c) is an ordinary implication over ZF. Nothing here asserts that Urysohn's lemma is false.