Games in set theory are usually informally described by describing the rules of the two players and the winning condition. Sometimes we need to describe an interaction between games, which then becomes quite ad hoc, describing certain functions with properties that are desired in the specific proof in question. This is especially prominent in the proof of Borel determinacy, where unraveling coverings are used to transfer determinacy statements between games. I’ll here attempt to describe this framework in a more abstract setting, viewing games as objects in their own right, which at the very least might make the proof of Borel determinacy clearer.
We first have to agree on what a game really is. As we’re working with games from a set-theoretical point of view we focus on 2-player games with perfect information, in which the two players are playing finite ordinals. We also require that one of the two players wins – we don’t allow draws. Such a game are usually described as
Here player I and II are taking turns playing finite ordinals and , respectively. Usually we enforce some rules as well. If we for instance view the finite ordinals as coding chess moves, we would want to make sure that e.g. pawns can only move forwards. Of course for this example to be valid we need to remove the possibility of a draw in the chess game, so say for instance that White (player I) wins if we’re in a “draw scenario”.
To model the rules in set theory, we first take a step back and look at the plays of the game, which we can define as countable sequences of finite ordinals , which is also just an element of the Baire space . Now, if we want to enforce a rule, this simply corresponds to making certain plays illegal, so we’re restricting the possible plays to a subset . This is all well and good when we’re done with playing, but we’d like to say straight away if a rule is broken. Because of this we’re interested in the derived tree of , which is the tree of all partial plays:
We can always recover from by looking at the set of infinite branches of the tree:
This back-and-forth procedure works with all pruned trees, which are trees satisfying that every partial play can be extended — i.e. that whenever we’re at a certain stage of the game, there is some legal move that the current player can play. In other words, we can now tentatively think of a game as simply a pruned tree .
We need to say more than just the legal moves of a game – we need to say what it takes to win the game as well. This can simply be encoded as a subset of the set of all the legal plays, i.e. . The pair thus encodes both the rules and the winning conditions of a given game, so we can model the game as this pair. To help intuition we will write for the game described by and . Also, if we’re not particularly interested in the winning condition at a given time we’ll simply write for the game.
Now, if we want an interaction between games we need to have a notion of a mapping between games. This is where I’ll resort to what Martin calls coverings of games, which is what he used to prove Borel determinacy. Here’s the definition.
Definition. A covering is a pair such that
- is monotone and length-preserving, giving rise to a continuous extension given by ;
- maps partial strategies in to partial strategies in satisfying that if then , which gives rise to an extension taking strategies to strategies given by ;
- If is played according to a strategy then there’s a played according to such that .
It’s a bit of a mouthful, but it basically says that it takes plays and strategies7 from one game to the other, while preserving the relationship between plays and strategies. Here a strategy is “the intuitive notion”, which can be modelled in set theory as a function taking a partial play and giving you a finite ordinal to play next. As the two players are alternating, a strategy for player I takes even-length partial plays as input and a strategy for player II takes odd-length partial plays.
Summing up we now have a rigourous notion of what a game is and what a map between games is. As one could expect, this gives us a category of games. For instance, we can simply compose two coverings and by composing the two component maps: and .
Using this framework we can now describe what goes on in Martin’s proof of Borel determinacy. But this is already a rather big mouthful to take in, so that will have wait until next time.