Which results on this page spend dependent choice, which spend countable choice, and which are theorems of ZF

This remark extends the choice-strength bookkeeping of The choice ledger: what costs the Axiom of Choice and what does not and of Conventions on this page, and the one implication of the classical chain that is not available at this point in the reading order §4 to the results proved on this page, naming exactly which theorem spends which principle and at which single step, in the spirit both of those items.

The dyadic rationals of $[0,1]$, their finite levels $D_n$, and their density in $[0,1]$ is choice free: its density argument fixes one natural number via The well-ordering principle, a theorem of ZF, and one dyadic rational via a single existential instantiation, never a simultaneous selection.

If $(U_r)_{r \in D}$ are open with $\overline{U_r} \subseteq U_s$ whenever $r < s$ and $U_1 = X$, then $x \mapsto \inf\{ r \in D : x \in U_r \}$ is a continuous map $X \to [0,1]$, and no choice principle is used is choice free by its own statement: given an already constructed family of open sets, producing the continuous function they define costs nothing. It is exactly because this step is free that the choice cost of Urysohn's lemma, under the axiom of dependent choice: in a normal space two disjoint closed sets are separated by a continuous function into $[0,1]$, and conversely such a space is normal can be isolated to the single step that builds the family in the first place.

The converse clauses — that a space whose disjoint closed sets are always separated by a continuous function is normal (Urysohn's lemma, under the axiom of dependent choice: in a normal space two disjoint closed sets are separated by a continuous function into $[0,1]$, and conversely such a space is normal, clause 2), and that a space with the closed-subspace extension property is normal (Tietze's extension theorem, under dependent choice: a continuous map from a closed subspace of a normal space into $[a,b]$ extends continuously to the whole space, and this property characterises normality, clause 2) — use no choice principle: each cuts a given continuous function at the value $1/2$ and reads off two disjoint open sets.

If for every $\varepsilon > 0$ some continuous $g : X \to \mathbb{R}$ satisfies $\lvert f(x) - g(x)\rvert < \varepsilon$ for all $x$, then $f$ is continuous; in particular a uniformly convergent series of continuous real functions has a continuous sum is choice free throughout, including its Weierstrass-type second clause: every existential step draws from a single nonempty set of reals or a single continuous function, never from an infinite family at once.

Urysohn's lemma, under the axiom of dependent choice: in a normal space two disjoint closed sets are separated by a continuous function into $[0,1]$, and conversely such a space is normal, clause 1, spends dependent choice exactly once: the application of The axiom of dependent choice: a relation in which every element is related to something admits an $\mathbb{N}$-indexed chain that strings together the countably many admissible finite-level open-set assignments built in that item's own proof, each extending the one before. Every finite level is itself built by Every natural-number-indexed list of nonempty sets has a choice function on its family of values, a theorem of ZF, so the only place the sequence of levels itself is assembled — rather than any one level — is where DC is spent.

Tietze's extension theorem, under dependent choice: a continuous map from a closed subspace of a normal space into $[a,b]$ extends continuously to the whole space, and this property characterises normality, clause 1, spends dependent choice in the same shape and at the same kind of step: the sequence of approximating pairs $(f_n,g_n)$, where each $g_{n+1}$ is chosen using the particular remainder function $f_{n+1}$ produced from the previous stage. This dependency is genuine — unlike the corresponding step of Under dependent choice a space is perfectly normal if and only if it is normal and every closed set is a zero set below, the relation driving the recursion cannot be replaced by one that ignores its first argument.

The following results on this page assume dependent choice purely by inheritance, through a citation of one of the two results above, and spend no further choice principle of their own: Under dependent choice a normal $T_1$ space is completely regular, so $T_4 \Rightarrow T_{3\frac{1}{2}}$, and together with the implications already proved this is the whole classical chain, Under dependent choice, a continuous real-valued map on a closed subspace of a normal space extends to the whole space, and a map into an open interval extends into that same open interval, Under dependent choice a locally compact Hausdorff space is completely regular, hence Tychonoff, and Under dependent choice a compact Hausdorff space is Tychonoff, and its disjoint closed sets are separated by continuous functions.

The forward direction of Under dependent choice a space is perfectly normal if and only if it is normal and every closed set is a zero set performs a step shaped like the Axiom of Countable Choice (The Axiom of Countable Choice ($\mathrm{AC}_\omega$)): a Urysohn function is selected for every level of a fixed countable presentation $C = \bigcap_n U_n$, and the selection at level $n$ does not depend on the one at any other level. That item's own proof discharges this as a direct instance of dependent choice, using a relation that carries no memory of the previous term, so the theorem is stated under DC alone rather than under DC together with a separately-adopted $\mathrm{AC}_\omega$.

In a metric space every closed set is a zero set and a $G_\delta$, and the distance function separates a point from a closed set, so every metrizable space is Tychonoff and perfectly normal proves the metric case of every property this page's headline theorems assert for a general normal space — Urysohn separation, the zero-set characterisation of perfect normality — entirely free of choice, the distance function supplying every function needed by an explicit formula. The contrast confirms that the choice cost on this page belongs to the passage from a topology to no topology beyond normality, not to the properties themselves.

Assuming countable choice, every perfectly normal space is completely normal: separated sets in a normal space whose open sets are all $F_\sigma$ can be separated by disjoint open sets, by contrast, needs only countable choice, and for a structurally different reason than the one above: its single choice-consuming step selects one open set for each member of a countable family of closed sets that already exists in full before any selection is made, with no member of the family depending on an earlier choice. That is the textbook shape of $\mathrm{AC}_\omega$ with no disguise needed, unlike the two DC arguments on this page.

Nothing here shows dependent choice is necessary for Urysohn's lemma or for Tietze's theorem; that would be an independence result, and this library proves none. What is recorded, with sources, in Urysohn's lemma is not a theorem of ZF, nor of ZF plus countable choice ‡ is that the classical $T_4$ form of Urysohn's lemma is a theorem of neither ZF nor ZF together with countable choice, so the DC hypothesis carried by every theorem on this page cannot be weakened to countable choice without leaving the space of what has been established.