The proof of Borel determinacy doesn’t seem to have the best reputation, as it’s both rather long, quite technical and it’s really easy to lose track of what’s going on. I’ve noticed that the same proof can be presented in a more structural setting, making the core ideas of the proof be slightly clearer. I’ll try here to present what’s going on in the proof, using the structural framework of games I set up in my previous post. The full proof can be found in my determinacy project.
In my previous post I only considered games in which integers were played, but it’s a curious fact that the proof of Borel determinacy needs to consider all possible games to work. Let’s therefore write for the game in which the two players play elements for any set , is the pruned tree of legal moves and is the payoff set. Our previous games are therefore simply . All right, so far so good. Let’s recall what Borel determinacy actually says.
Theorem (Martin). Every Borel game is determined.
As most proofs of determinacy, the strategy is to come up with auxiliary simple games which are determined, and somehow transfer this fact to the game in question – this is where the coverings come into play. Martin defines that a covering unravels a set if is clopen in . A game is then said to be unraveled if there exists a covering unraveling . By playing around with the definition of covering and being unraveled, we get the following fact, which is the reason why we care about unraveled games.
Proposition. Every unraveled game is determined.
The problem is thus reduced to showing that every Borel game is unraveled. This is done inductively, starting with closed () games and then inductively showing that every game is unraveled, for every . The ‘closed case’ is a direct argument, producing an explicit covering of an arbitrary closed game. Here’s a sketch of how it’s constructed.
Given any game we will define an auxiliary game with a covering unraveling the closed set . Since the game is already closed we need to enforce an “open” condition, which is to say that we want to modify so that if player I wins, he will already have won at a finite stage. The way this is done is by making the two players at round play a set of strategies, which they’re then required to follow for the rest of the game.
This means that the game is really over at round , in that if player I (resp player II) wins, then this was already known in the ‘th round. We can then produce the first part of the covering as simply forgetting this extra strategy-information. Constructing the second part is done by considering a series of cases, which I’ll omit here. This finishes the sketch of the following.
Proposition. Every closed game is unraveled.
That finishes the “induction start”. For the limit levels of the induction we need to improve the above-mentioned result. Note that the auxiliary game didn’t depend on which we chose, so we really showed an ostensibly stronger property. We say that a covering is a k-covering if and agree up to level , and that is the identity up to this level.
What the above proof then shows is that given any closed game and we can find a -covering that unravels . The reason why we care about this strengthening is that the -coverings allow us to ensure the existence of certain inverse limits of games, which we will need in our induction.
Proposition (Existence of inverse limits). Let and be a -covering for every . Then there’s a game and -coverings for every such that , and is the universal such game.
The “universal” statement at the end means that if is another game with -coverings such that then there’s a unique covering satisfying for every . In other words, is the “supremum” of the ‘s.
For the inductive argument fix some and let’s assume that we’ve shown that games, and thus also games, are -unraveled for all and . Let be a game, meaning that is a countable union of sets for .
By assumption we get a -covering unravelling where , and $latex T_0:=T, and recursively
is a -covering unravelling , which exists as is closed under continuous preimages for .
We can then take the inverse limit with -coverings . Now is a -covering unravelling every , since
and is continuous. Then is open, so we get a -covering -unravelling . But now
is a -covering unravelling and we’re done. QED
So given any game we find a linear system of coverings of length that collectively unravel . The existence of this linear system requires that we use the axiom of replacement many times, and this was shown by Friedman (1971) to be necessary as well.
Friedman, Harvey (1971). “Higher set theory and mathematical practice”. Annals of Mathematical Logic. 2 (3): 325–357.