Why the nested-interval proof of Baire category in $\mathbb{R}$ needs no choice, while the general complete-metric statement does

What the proof on this page spends. The proof of Baire category in $\mathbb{R}$, by nested intervals with canonically chosen rational endpoints: a countable intersection of dense open sets is dense, so $\mathbb{R}$ is not a countable union of nowhere dense sets uses exactly four things: the recursion theorem (The recursion theorem), the well-ordering principle for $\mathbb{N}$ (The well-ordering principle), the nested interval property (A nested sequence of nonempty closed bounded intervals has nonempty intersection, and the intersection is a single point exactly when the lengths tend to $0$), and one fixed enumeration of the rationals ($\mathbb{Q}$ is countably infinite, The rationals embed densely in the reals). None of these is a choice principle. The enumeration is a single object, fixed once by one instantiation of an existential statement; the interval used at stage $k$ is the one whose two rational endpoints have least index among those meeting the requirements, and "least" is determined by The well-ordering principle; so the successor rule is a function, and the whole construction is one application of The recursion theorem to it. In particular the proof does not use countable choice (The Axiom of Countable Choice ($\mathrm{AC}_\omega$)), which the neighbouring measure-theoretic results on this page do use.

What the naive proof would spend, and why. The textbook argument says: given the interval produced at stage $k$, choose an interval inside it meeting $U_{k+1}$, and repeat. Each choice is made from a nonempty set that depends on the previous choice, and it is made infinitely often. That pattern is not countable choice, which selects from a family fixed in advance; it is the axiom of dependent choice (The axiom of dependent choice: a relation in which every element is related to something admits an $\mathbb{N}$-indexed chain). Replacing the choice by a canonical rule is the only edit the argument needs, and fixing an enumeration of a dense set in advance is what makes a canonical rule available.

What this does NOT establish. It establishes nothing about the Baire category theorem for complete metric spaces in general. That statement is genuinely stronger, and how much stronger is recorded, with references and without proof, in The Baire category theorem is four inequivalent statements over ZF ‡: over ZF the metric version is equivalent to dependent choice, whereas its restriction to spaces with a countable dense subset is a theorem of ZF, "a fixed countable dense set removes every choice from the construction". The proof of Baire category in $\mathbb{R}$, by nested intervals with canonically chosen rational endpoints: a countable intersection of dense open sets is dense, so $\mathbb{R}$ is not a countable union of nowhere dense sets is precisely that restricted argument, specialised to $\mathbb{R}$ with the rationals as the countable dense set. So the correct summary is:

• the statement proved here, for $\mathbb{R}$, needs no choice principle;
• the general metric statement is not proved here at all, and is not a corollary of what is proved here;
• the strength of that general statement over ZF is quoted from the literature in The Baire category theorem is four inequivalent statements over ZF ‡, which this library does not prove.

Why the distinction is worth a separate item. The two statements are routinely called by the same name, and a reader who has seen "Baire needs dependent choice" may reasonably suspect the proof above of hiding an appeal to it. It does not, and the place to look is the successor rule: it takes a minimum over $\mathbb{N} \times \mathbb{N}$ rather than picking a witness. The same device appears in Every nonempty perfect subset of $\mathbb{R}$ is uncountable, and in both places it is the enumeration of $\mathbb{Q}$ that pays for it.

A note on the surrounding page. Choice is not avoided everywhere here. A countable union of measure-zero sets has measure zero, by countable choice spends countable choice at one clearly marked step, and says so; Every at most countable subset of $\mathbb{R}$ has measure zero and The Cantor set is compact, perfect, uncountable, nowhere dense and of measure zero, and it contains no interval of positive length, so its only nonempty connected subsets are single points spend none. The page is arranged so that each appeal is visible where it happens rather than absorbed into a general convention.