The complete-metric Baire principle over ZF

Work in ZF. Let $(X,d)$ be a metric space. Closure, interior and density are as in Interior, closure, boundary, limit point, isolated point and dense subset of a metric space, with all complements relative to $X$. Families indexed by $\omega$ are functions, as in An indexed family $(A_i{)}_{i\in I}$ is a function with domain $I$; $\{A_i:i\in I\}$ is its range, and their unions and intersections are those of ${\bigcup }_{i\in I}{A}_i:=\bigcup \{A_i:i\in I\}$, and ${\bigcap }_{i\in I}{A}_i:=\bigcap \{A_i:i\in I\}$ for $I\mathrm{\ne }\mathrm{\varnothing }$.

A set $N\subseteq X$ is nowhere dense if ${\mathrm{int}}_X(\bar{N})=\mathrm{\varnothing }$. A set $M\subseteq X$ is meagre if there exists a sequence $(N_n{)}_{n\in \omega }$ of nowhere dense subsets of $X$ such that $M\subseteq {\bigcup }_{n\in \omega }{N}_n$. A set $C\subseteq X$ is comeagre if $X\setminus C$ is meagre.

The space is Baire if, for every sequence $(U_n{)}_{n\in \omega }$ of open dense subsets of $X$, the intersection ${\bigcap }_{n\in \omega }{U}_n$ is dense in $X$. The complete-metric Baire principle (CM-Baire) asserts that every complete metric space, in the sense of Complete metric space: every Cauchy sequence converges in the space, is Baire.

This includes the empty space: its only subset is open and dense, its $\omega$-indexed intersection is empty and dense in that space, and there are no Cauchy sequences into it. The empty set is meagre in every space, witnessed by $N_n=\mathrm{\varnothing }$ for every $n$.

A witness is an actual sequence of nowhere dense sets. These definitions do not assert that a countable union of sets merely known to be meagre is meagre: choosing one decomposition for each such set would require a separate argument. Miller, Definitions 4.2–4.4, p.8, motivates the convention; Karagila's warning after Theorem 16, p.10, identifies the decomposition-selection issue. We use containment in a union, so meagre subsets need not themselves be closed-set unions.