# How exactly is axiom of dependent choice used in Baire's Theorem?

I went over the proof of Baire's Theorem for complete metric spaces (that a countable union of closed sets with empty interior has empty interior). In the proof, a decreasing nested sequence of closed balls is constructed. Then we choose a particular point from each of these balls and construct a sequence of those points.

I thought that we used axiom of choice when we chose these points. But then I read in multiple source that we actually don't use axiom of choice and that we use a weaker form, called the axiom of dependent choice. I looked up the definition of dependent choice:

Axiom of dependent choice (DC): Let $$A$$ be a non-empty set and $$R \subseteq A \times A$$ satisfy $$\forall a \in A \; \exists b \in A: a R b$$. Then there exists a sequence $$(a_n)_n$$ such that $$a_n \; R \; a_{n+1} \; \forall n$$.

The problem I have with this is that I don't understand how this axiom was used. First of all, what is the set $$A$$ and relation $$R$$ when we apply DC to prove Baire's Theorem? And secondly, could someone explain in some more details how this axiom is used.

• I wrote a whole chapter about it: arxiv.org/abs/2010.15632 Jan 11, 2022 at 22:02
• And this might also answer your question. Jan 11, 2022 at 22:04
• @AsafKaragila is it possible to prove Baire's Theorem for locally compact hausdorff spaces without DC? If so, could you refer me to a proof that doesn't use it? (I know it isn't possible for complete metric spaces, because they are equivalent). Jan 11, 2022 at 22:32
• Well, assuming BPI it is equivalent to to DC, so you can't. See mathoverflow.net/a/391946/7206 Jan 11, 2022 at 22:40
• Can you share the exact proof that you saw? Jan 11, 2022 at 22:42

Define a sequence of points $$x_n$$ such that $$x_{n+1}$$ is within $$2^{-n}$$ of $$x_n$$. We're applying DC to the relation "$$x_{n+1}$$ is within $$2^{-n}$$ of $$x_n$$". (This answer uses some help from the text that Asaf Karagila linked in the comments, but I have not yet read its explanation of why DC is enough.)