Choice strengths of Baire category principles 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).

Comparing them. DC implies DMC over ZF, but whether DMC implies DC over ZF is open, so no ZF strictness between BCT-metric and BCT-compact-Hausdorff is asserted here. In ZFA, Fraenkel's second model satisfies DMC and refutes DC, so the two principles are separated there. The Boolean prime ideal theorem does not imply DMC over ZF, 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. The ZF nonimplication from BPI to DMC and the ZFA nonimplication from DMC to DC are witnessed by models; no ZF separation of DMC from DC is claimed.

• Where the BPI separation is recorded. The two facts about DMC used for the BPI comparison 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 proved choice ledger: hypotheses, equivalences, and upper bounds ↗ and The proved choice cost of the ultrafilter lemma ↗ record principles by name for exactly this reason, and The Axiom of Countable Choice (${\mathrm{A}\mathrm{C}}_{\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 their ambient base theory. The two equivalences and the implication from DC to DMC 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.