The n-Category Café

To read this post, all you need to know about the statement of the Borel determinacy theorem is that it involves nothing set-theoretically exotic. Here it is:

Theorem (Borel determinacy)   Let $A$ be a set and $X \subseteq A^{\mathbb{N}}$. If something then something.

Neither “something” is remotely sneaky. The highest infinity mentioned is $\mathbb{N}$. Moreover, the set $A$ is often taken to be $\mathbb{N}$ too.

If you want to know more about the theorem, there are plenty of explanations out there by people more qualified than me, including a very nice series of blog posts by Tim Gowers. But perhaps it will create an undeserved aura of mystery if I don’t actually state the theorem, so I will. I’ll indent it for easy ignoring.

Ignorable digression: what Borel determinacy says   Given a set $A$ and a subset $X \subseteq A^\mathbb{N}$, we imagine a two-player game as follows. Player I chooses an element $a_0$ of $A$, then player II chooses an element $a_1$ of $A$, then player I chooses an element $a_2$ of $A$, and so on forever, alternating. If the resulting sequence $(a_0, a_1, a_2, \ldots)$ is in $X$ then player I wins. If not, II wins.

A strategy for player I is a function that takes as its input an even-length finite sequence of elements of $A$ (to be thought of as the moves played so far) and produces as its output a single element of $A$ (to be thought of as the recommended next move for player I). It is a winning strategy if following it guarantees a win for player I, regardless of what II plays. Winning strategies for player II are defined similarly.

Does either of the players have a winning strategy? Clearly they can’t both have one, and clearly the answer depends on $A$ and $X$. If one of the players has a winning strategy, the game is said to be determined.

A negative result: using the axiom of choice, one can construct for any set $A \gt 1$ a subset $X \subseteq A^{\mathbb{N}}$ such that the game is not determined.

Positive results tend to be stated in terms of the product topology on $A^\mathbb{N}$, where $A$ itself is seen as discrete. For example, it’s fairly easy to show that if $X$ is open or closed in $A^\mathbb{N}$ then the game is determined.

A subset of a topological space is Borel if it belongs to the $\sigma$-algebra generated by the open sets, that is, the smallest class of subsets containing the open sets and closed under complements and countable unions.

The Borel determinacy theorem, proved by Donald A. (Tony) Martin in 1975, states that if $X \subseteq A^\mathbb{N}$ is Borel then the game is determined.

What is it that people say about Borel determinacy and replacement? Here are some verbatim quotations from people who surely know more about Borel determinacy than I do.

From the Wikipedia entry on the axiom scheme of replacement:

Harvey Friedman showed that replacement is required to show that Borel sets are determined

(my bold, here and throughout).

From a nice math.stackexchange answer by set theorist Andrés Caicedo:

it [the proof of the Borel determinacy theorem] uses replacement in an unavoidable manner.

From the opening post of that splendid series by Tim Gowers:

In order to iterate the power set operation many times, you have to use the axiom of replacement many times.

Gowers begins by citing two helpful sources, one by Shahzed Ahmed, who writes (p.2):

in 1971 Friedman showed it is not possible to prove Borel Determinacy without the replacement axiom, at least for an initial segment of the universe

…and one by Ross Bryant (p.3):

a proof of Borel Determinacy […] would become the first known theorem realizing the full potency of the Axiom of Replacement. […] Refinements of the proof in [Mar85] revealed a purely inductive proof and the full use of Replacement in the notion of a covering.

(Of all these quotes, this is the only one I’d call factually incorrect.)

From a paper by philosopher Michael Potter (p.185):

There are results about the fine structure of sets of real numbers and how they mesh together which require replacement for their proof. The clearest known example is a result of Martin to the effect that every Borel game is determined, which has been shown by Harvey Friedman to need replacement.

From Martin’s 1975 paper proving the Borel determinacy theorem:

Borel determinacy is probably then the first theorem whose statement does not blatantly involve the axiom of replacement but whose proof is known to require the axiom of replacement.

From philosopher of mathematics Penelope Maddy (Believing the axioms I, p.490):

Recently, however, Martin used Replacement to show that all Borel sets are determined […] Earlier work of Friedman establishes that this use of Replacement is essential.

And from a recent paper by logician Juan Aguilera (p.2):

there are many examples of theorems that cannot be proved without the use of the axiom of replacement. An early example of this was that of Borel determinacy. […] Even before Martin’s Borel determinacy theorem had been proved, it was known that any proof would need essential use of the axiom of replacement.

So there you have it. Experts agree that to prove the Borel determinacy theorem, the axiom scheme of replacement is required, needed, unavoidable, essential. You have to use it. Without replacement, it is not possible to prove Borel determinacy. It cannot be proved otherwise.

I want to argue that this emphasis is misplaced and misleading. It is especially misplaced from the point of view of categorical set theory, or more specifically Lawvere’s Elementary theory of the category of sets (ETCS).

The mathematical point is that to prove Borel determinacy, what you need to be able to do is construct the transfinitely iterated power set $\mathcal{P}^W(A)$ for all countable well-ordered sets $W$ (or ordinals if you prefer). That is, you need $\mathcal{P}(A)$, then $\mathcal{P}(\mathcal{P}(A))$, and generally $\mathcal{P}^n(A)$ for all natural numbers $n$, then their supremum $\mathcal{P}^\omega(A)$, then its power set $\mathcal{P}^{\omega + 1}(A)$, and so on through all countable well-ordered exponents.

When I say you “need to be able to do” this, I mean it in a strong sense: Friedman showed in the early 1970s that Borel determinacy can’t be proved otherwise (even, I think, in the case where $|A| = 2$). And when Martin later proved Borel determinacy, his proof used this construction and no more.

If we remove replacement from ZFC then transfinitely iterating the power set construction is impossible, so Borel determinacy cannot be proved. Indeed, Friedman found a model of ZFC-without-replacement in which the Borel determinacy theorem is false. This is the precise result that lies behind the quotes above.

So what’s the problem? It’s that replacement is vastly more than necessary.

Let me tell you a story.

One morning I went for a long walk. Far from home, I started to feel a bit hungry and wanted to buy a snack. But I realized I hadn’t brought any money . What could I do?

Out of nowhere appeared a chef. Somehow, magically, he seemed to know what I needed. “Come into my restaurant!” he cried, beckoning me in. Inside, he showed me a big table heaped with food, enough to feed a wedding party. “This is all for you!”

“But I only want a snack,” I replied.

“It’s all or nothing. Either you eat everything on this table, or you go hungry,” he said, locking the door.

I weighed up the pros and cons.

I made my decision.

I sat down to eat.

Darkness had fallen before I emerged from the restaurant, waddling, belly swollen, beyond queasy. My urge for a snack had been satisfied, but what terrible price had I paid?

In the months that followed, a rumour began to circulate. People said I “required” enough food for fifty. In awed whispers, they told of how my legendary hunger “could not be satisfied” otherwise, that this vast spread was “essential” for me to survive. I “needed” it, they said. Some claimed I had to have the “full table”. Without that gargantuan smorgasbord, the rumour went, it was “not possible” for me to fulfil my urge for a snack.

I ask you, is that fair?

All I actually needed was a snack, and all the Borel determinacy theorem actually needs is the axiom “all beths exist”. This means that the transfinitely iterated power set $\beth_W = \mathcal{P}^W(\mathbb{N})$ exists for all well-ordered sets $W$. As I explained in a recent post, it is equivalent to any of the following conditions.

• Recursive, order-theoretic version: for a well-ordered set $W$, we say that $\beth_W$ exists if there is some infinite set $B$ such that $B \geq 2^{\beth_V}$ for every well-ordered set $V$ smaller than $W$. In that case, $\beth_W$ is defined to be the smallest such set $B$. “All beths exist” means that $\beth_W$ exists for all well-ordered sets $W$.

• Non-recursive, order-theoretic version: “all beths exist” means that for every well-ordered set $W$, there exist a set $X$ and a function $p: X \to W$ with the following property: for $w \in W$, the fibre $p^{-1}(w)$ is the smallest infinite set $\geq 2^{p^{-1}(v)}$ for all $v \lt w$.

• Non-recursive, non-order-theoretic version: “all beths exist” means that for every set $I$, there exist a set $X$ and a function $p: X \to I$ such that for all distinct $i, j \in I$, either $2^{p^{-1}(i)} \leq p^{-1}(j)$ or vice versa.

If all beths exist then for any set $A$ and well-ordered set $W$, we can form the transfinitely iterated power set $\mathcal{P}^W(A)$, which is enough to prove the Borel determinacy theorem.

In fact, for the Borel determinacy theorem, we only need this when $W$ is countable. Moreover, one often assumes that the set $A$ on which the game is played is countable too. In that case, we only need countable beths to exist (where “countable” refers to the $W$ of $\beth_W$, not $\beth_W$ itself).

The axiom that all beths exist is vastly weaker than the axiom scheme of replacement. (And the axiom that all countable beths exist, weaker still.) To give the merest hint of the distance between them, it is consistent with the existence of all beths that there are no beth fixed points, whereas replacement implies the existence of unboundedly many beth fixed points. See the diagram here.

So the take-home message is this:

Borel determinacy does not require replacement. It only requires the existence of all beths.

I now want to say something loud and clear:

Everyone knows this.

Well, not literally everyone, otherwise I wouldn’t be bothering to write this post. (It comes as a surprise to some.) By “everyone” I mean everyone who has worked through a proof of the Borel determinacy theorem, including everyone I’ve quoted and presumably most working set theorists. I’m taking no one for a fool!

First, they know Borel determinacy can’t possibly need the full power of replacement for the simple reason that replacement is an axiom scheme, a bundle of infinitely many axioms, one for each first-order formula of the appropriate kind. Any proof of a non-exotic theorem (I mean, one not quantified over formulas) can use only finitely many of these axioms. But more specifically, for this particular proof, “everyone” knows which instances are needed.

Indeed, many of the people I quoted earlier made this point too, often in the same sources I quoted from. To be fair to all concerned, I’ll show them doing so. Here’s Andrés Caicedo:

the [set needed] is something like $\mathcal{P}^\alpha(\mathbb{N})$ if the original Borel set was at level $\alpha$.

Juan Aguilera (p.2):

Friedman’s work showed that any proof of Borel determinacy would require the use of arbitrarily large countable iterations of the power set operator, and Martin’s work showed that this suffices. A convenient slogan is that Borel determinacy captures the strength of countably iterated powersets.

Tony Martin (p.1):

Later (in §2.3) we will use results from §1.4 in analyzing level by level how much of the Power Set and Replacement Axioms is needed for our proof of the determinacy of Borel games.

Set theorist Asaf Karagila:

Even the famous Borel determinacy result (which is the usual appeal of Replacement outside of set theory […]) only requires $\beth_{\omega_1}$ which is far, far below the least [beth] fixed point.

And Penelope Maddy (p.489, shortly before she gets on to Borel determinacy specifically):

Around 1922, both Fraenkel and Skolem noticed that Zermelo’s axioms did not imply the existence of

$$\{ N, \mathcal{P}(N), \mathcal{P}(\mathcal{P}(N)), \ldots \}$$

or the cardinal number $\aleph_\omega$. These were so much in the spirit of informal set theory that Skolem proposed an Axiom of Replacement to provide for them.

Did you notice something about that last quotation? Maddy goes straight from the existence of $\aleph_\omega$ and $\beth_\omega$ to the full axiom scheme of replacement. To be fair, she’s recounting history rather than doing mathematics. But it’s like saying “Skolem needed a snack, so he ate enough for an entire wedding party”.

In summary, it seems to be common for people (especially set theorists) to state explicitly that replacement is required or necessary or essential to prove Borel determinacy — that it cannot be proved without replacement — while fully aware that only a minuscule fragment of replacement is, in fact, needed.

I’ve said that I think this is misleading, but it also strikes me as curious. Those who do this, many of them experts, are eliding the difference between a light snack and a health-threateningly huge food mountain. Why would they do that?

My theory is that it’s down to the success of ZFC. Now that the axioms are fixed and published in hundreds of textbooks, it’s natural to think of each axiom in take-it-or-leave-it terms. We include replacement or we don’t. It’s the same choice the chef gave me: the full table or nothing.

Membership-based set theorists do study fragments of replacement, including in this context. This conversation began when David Roberts pointed out Corollary 2.3.8 and Remark (i) after it in Martin’s book draft, which concern exactly this point. But there are orders of magnitude fewer people who read technical side-notes like Martin’s than who read and repeat the simple but misleading message “Borel determinacy requires replacement”.

For those of us whose favourite set theory is ETCS, replacement is just one of many possible axioms with which one could supplement the core system. There are many others. “All beths exist” is one of them — a far weaker one — which is perfectly natural and perfect for the job at hand. Reflexively reaching for replacement just isn’t such a temptation in categorical set theory.

All of that leaves a question:

Is there any prominent result in mathematics, outside logic and set theory, that can be proved using replacement but cannot be proved using “all beths exist”?

I don’t know. People ask questions similar to this on MathOverflow from time to time (although I don’t think anyone’s asked exactly this one). I haven’t been through the answers systematically. But I will note that in Wikipedia’s list of applications of replacement, Borel determinacy is the only entry that could be said to lie outside set theory. (And the remainder are meaningless in an isomorphism-invariant approach to set theory, largely involving the distinction between ordinals and well-ordered sets.) So if there’s an answer to my question, someone should tell the world.

Postscript (28 July 2024)   Judging by some of the reactions I’ve encountered in the last three years, this post has been widely misunderstood. I don’t blame anyone for that but myself, but I’d like to clarify.

Some people seem to think that the point of this post is to quibble over the use of words like “necessary”. Not really.

First, I’m sure I too have said things like “the axiom of choice is necessary to prove the existence of nontrivial ultrafilters”, while knowing perfectly well that the statement on ultrafilters is strictly weaker. It’s a natural way of speaking.

Second, as I detailed in the post, the people I quoted know perfectly well that replacement isn’t “necessary” for Borel determinacy in the sense of “necesssary and sufficient”. In other words, they’re well aware that only a fragment of replacement is needed to prove Borel determinacy. As I wrote, “I’m taking no one for a fool”.

So if the point wasn’t to nitpick over words like “necessary”, what was it?

The point was to emphasize the vast distance between Borel determinacy and replacement. (Hence the food metaphor.) To the extent that Borel determinacy is used as a justification for including replacement as an axiom, I wanted to highlight how flimsy that argument is.

Again, if you’re used to ZFC and its variants then it’s natural to see replacement in take-it-or-leave-it terms: without it, you can’t prove Borel determinacy, and with it, you can, so words like “necessary” are more natural.

But from the viewpoint of ETCS, there’s a whole spectrum of possible extra axioms that one can add to the core system, in which one of the weakest (“all beths exist”) suffices to prove Borel determinacy and replacement is one of the stronger ones. From that perspective, it would feel weird and misleading to say that replacement is necessary to prove Borel determinacy. This viewpoint is clarified by the diagram in Large Sets 13 and, really, by the whole of that series.