The Baire category theorem is four inequivalent statements over ZF

Over ZF, "the Baire category theorem" is not one statement. Naming the versions by the class of spaces they quantify over:

(BCT-metric) In a complete metric space, a countable intersection of dense open sets is dense. Over ZF this is equivalent to the axiom of dependent choice (DC). The implication from DC is the usual proof, in which each nested ball is chosen in terms of the previous one; the converse is Blair (1977).

(BCT-separable) The same statement restricted to separable complete metric spaces is a theorem of ZF, with no choice principle at all: a fixed countable dense set removes every choice from the construction.

(BCT-compact-Hausdorff) Every compact Hausdorff space is a Baire space. Over ZF this is equivalent to the principle "every tree has a subtree all of whose levels are finite", introduced by Blass (1979) and known as dependent multiple choice (DMC). The equivalence is Fossy and Morillon (1998).

Separating them. DMC is strictly weaker than each of DC and the axiom of multiple choice, in ZF and in ZFA alike, so BCT-metric and BCT-compact-Hausdorff are genuinely different assumptions. The Boolean prime ideal theorem does not imply DMC either, and so does not give BCT-compact-Hausdorff. The ground for that last point is recorded elsewhere on this page: DMC implies Urysohn's lemma (Blass 1979) while BPI does not (Brunner 1983, in the Mostowski linearly ordered model). The same pair shows DMC is not itself a theorem of ZF, since Urysohn's lemma is not.

If ZF is consistent, none of these principles is a theorem of ZF except BCT-separable, and the non-implications listed are witnessed by models.

• Where the DMC separations are recorded. The two facts about DMC used in "Separating them" are the ones stated in Urysohn's lemma is not a theorem of ZF, nor of ZF plus countable choice ‡: Blass's implication from DMC to Urysohn's lemma, and Brunner's model in which BPI holds and Urysohn's lemma fails.

• Not proved in this library. No direction of any of these equivalences is proved here, and the models witnessing the non-implications are symmetric extensions and permutation models that this library does not build.

• What would prove it. For the equivalences: a careful ZF development of metric and compact Hausdorff spaces together with the combinatorics of trees. For the separations: permutation models with the Jech-Sochor or Pincus transfer theorems, that is, the same track as Cohen 1963: ZF does not prove the Axiom of Choice ‡.

• Why it matters here. Every use of the Baire category theorem in this library must name its version and pay for it. It is easy to write "by Baire" and quietly consume DC where the separable case would have been free, and easy to claim the locally compact or compact Hausdorff case is choice-free when it is not. The accounting pages The choice ledger: what costs the Axiom of Choice and what does not ↗ and What the ultrafilter lemma costs: a choice principle strictly weaker than AC ↗ record principles by name for exactly this reason, and The Axiom of Countable Choice ($\mathrm{AC}_\omega$) ↗ is where the weakest of the relevant principles is defined. What is not affected is availability: nothing about the Baire category theorem needs measure theory or functional analysis, so the theorem is in scope; only its cost is recorded here.

• A variant not asserted here. The locally compact regular form of the theorem is sometimes attributed to Bacsich (1972) with the same equivalence. That attribution was not confirmed against a primary source, so this item does not state it.

• Conditional discipline. The unprovability and non-implication clauses are relative to the consistency of ZF. The two equivalences are ordinary ZF theorems and need no consistency hypothesis; they are on this page because their proofs, not their status, are out of reach here.