Determinacy of (infinite, possibly loopy) combinatorial games

Question

I am looking for references and hopefully enlightening proofs of the following statement(s) concerning the determinacy of not-necessarily-well-founded (i.e., possibly infinite, possibly loopy) combinatorial / perfect-information games:

Let $G$ be a directed graph and $x_0$ a vertex of $G$, and consider the game where two players, starting at $x_0$, take turn in choosing an out-neighbor of the current state, thus producing an oriented path $x_0,x_1,x_2,x_3,\ldots$ in $G$ (i.e., Alice chooses an edge from $x_0$ to $x_1$, then Bob from $x_1$ to $x_2$ then Alice from $x_2$ to $x_3$, etc.): the player who cannot play loses, whereas if the game is continued indefinitely then it is a draw.

Then exactly one of the following three statements holds:

• the first player has a winning strategy,

• the second player has a winning strategy,

• both players have a surviving (i.e., non-losing) strategy.

Furthermore, if $\Phi\colon G \rightharpoonup \{\mathrm{P},\mathrm{N}\}$ is the least (for the partial order given by inclusion=restriction) partial function on $G$ with values in the 2-element set $\{\mathrm{P},\mathrm{N}\}$ such that

• $\Phi(x) = \mathrm{P}$ iff for all all out-neighbors $y$ of $x$ the value $\Phi(y)$ is defined and is $\mathrm{N}$, and

• $\Phi(y) = \mathrm{N}$ iff for all some out-neighbor $y$ of $x$ the value $\Phi(y)$ is defined and is $\mathrm{P}$,

(part of the statement is the fact that this least $\Phi$ is, indeed, well-defined; additionally, we can replace "iff" by "if" in both conditions above and the least $\Phi$ still exists and is the same),

—then the first player has a winning strategy starting from $x_0$ iff $\Phi(x_0) = \mathrm{N}$, the second has one iff $\Phi(x_0) = \mathrm{P}$, and both have a surviving strategy iff $\Phi(x_0)$ is undefined.

By "strategy" in the above I mean a positional strategy (i.e., one which decides the move to be taken in function of the state $x \in G$), but perhaps the equivalence with historical strategies (i.e., strategies which are allowed to depend on the past history) could be considered part of the statement.

These statements are not terribly difficult to prove, but the draws do complicate the matter somewhat in comparison to well-founded (=forward-finite, =terminating) graphs, where one player necessarily has a winning strategy (and $\Phi$ is defined by well-founded induction). The proofs I have found are unpleasantly messy.

So I am looking for precise references with hopefully enlightening proofs. By "enlightening", I mean that I am interested in knowing, for example, how much of the axiom of choice is needed to prove various (weaker, or classically equivalent) forms of the statement, whether the statements can be deduced from fixed point principles (e.g., the existence of $\Phi$ can be deduced from the (constructive) fixed point theorem 3.2 of this paper by Andrej Bauer and Peter LeFanu Lumsdaine), whether we need to mention ordinals, etc.

I am also interested in knowing the history of the above result (some people seem to attribute it to Zermelo, who proved that the game of chess satisfies a conclusion of this sort, but I don't know exactly what he proved).

More generally, any comments on the matter will be appreciated.

Answer 1

This amounts to the Gale-Stewart theorem showing that open games are determined. The issue of draws can be easily finessed, as I explain below.

Specifically, a game of perfect information is open for a given player, if whenever that player wins a play of the game, then the win was achieved after finitely many moves. There are many proofs in the literature. I give the ordinal-game-value proof, for example, on page 2 of my recent paper, V. Gitman and J. D. Hamkins, Open determinacy for proper class games. That proof can be viewed as a way of fulfilling your $\Phi$ remarks, since when a position has value, then the open player wins by the value-reducing strategy, and otherwise player II wins by the value-maintaining strategy. So we can label the positions with the one who has a winning strategy from that position. See also section 1 of my paper, C.D.A. Evans, J. D. Hamkins and N. Perlmutter, A position in infinite chess with game value $\omega^4$, which goes over the game-value proof of open determinacy.

Notice that infinite chess is an instance of the type of game you describe, since checkmate for either player happens after finitely many moves, and infinite play counts as a draw.

Open games are usually defined without draws, but in fact the issue of draws does not affect the essence of open determinacy, by the following simple argument. We can reduce the question of determinacy for open games with draws to determinacy of open games without draws.

Suppose that we have a game in which wins are determined at a finite stage of play and infinite play counts as a draw.

Consider now the modified game where we simply count a draw as a win for the second player. This modified game is an open game for the first player, since the only way the first player can win is by forcing the play into a win of the original game at a finite stage of play. Thus, by the Gale-Stewart theorem, this game is determined. So either player I can force a win in this game and hence also in the original game, or player II can force a win or a draw in the original game.

Similarly, we may modify the game alternatively by counting a draw as a win for player I. Now, the resulting game is open for player II, and so either player II can force a win in the modified game (and hence a win in the original game), or player I can force a win or a draw in the original game.

Thus, we get your trichotomy. Either one of the players has a winning strategy in the original game, or both players can force a draw or better. The argument is completely general for any game of the form you state, where a winner is determined after finitely many moves, and infinite play is a draw.

Answer 2

Here's an attempt at a self-contained (but perhaps not-so-illuminating) proof that avoids any mention of ordinals (albeit in a possibly contrived way) and makes the use of Choice explicit:

First, consider the set $\mathcal{S}$ of “partial everywhere winning” positional strategies: by this I mean partial functions $s\colon G\rightharpoonup G$ such that $s(x)$ is an out-neighbor of $x$ whenever it is defined and such that, from any such $x$, if the first player plays according to $s$ then $s$ keeps being defined (meaning that if $s(x)$ is defined and $y$ is an out-neighbor of $s(x)$ then $s(y)$ is defined) and the first player wins (the second player is stuck with no legal play after a finite time). We partially order $\mathcal{S}$ by inclusion (restriction) of partial functions.

Observation 1: if $s,s' \in \mathcal{S}$ then there exists $s'' \in \mathcal{S}$ which extends $s$ and is also defined wherever $s'$ is. Indeed, if we define $s''$ by $s''(x) = s(x)$ whenever $s(x)$ is defined and $s''(x) = s'(x)$ if $s(x)$ is not defined but $s'(x)$ is, then it is an element of $\mathcal{S}$ (because any game played by the first player according to $s''$ is either played according to $s'$ all along, or according to $s'$ and then $s$, or according to $s$ all along, but in any case the second player gets stuck in finite time).

Observation 2: if $s_i$ is a family of elements of $\mathcal{S}$ which are compatible in that $s_i(x) = s_j(x)$ whenever both $s_i(x)$ and $s_j(x)$ are defined, then their union $s := \bigcup_i s_i$ is again an element of $\mathcal{S}$. Indeed, any game played by the first player according to $s$ is, in fact, played according to $s_i$ for some $s_i$ for which $s_i$ is defined on the chosen starting position, so the first player wins.

Observation 2 implies that Zorn's lemma applies, so there is a maximal element $s$ of $\mathcal{S}$ for inclusion. Furthermore, observation 1 implies that this $s$ is defined on any $x\in G$ where any element $s'$ of $\mathcal{S}$ is defined (a simple but crucial fact).

Now let $N$ be the set of $x$ such that $s(x)$ is defined, and $P$ the set of $x$ such that all the out-neighbors of $x$ are in $N$. From what has just been said, $N$ is the set of positions from which the first (=Next) player has a winning positional strategy, and $P$ is the set of positions from which the second (=Previous) player has a winning positional strategy. Clearly $N$ and $P$ are disjoint.

Key remarks: (i) $x\in G$ belongs to $N$ iff it has an out-neighbor in $P$, and (ii) $x\in G$ belongs to $P$ iff all its out-neighbors are in $N$. Indeed, here (ii) is just the definition of $P$, so only (i) needs to be proved. But if $x$ belongs to $N$ then $y := s(x)$ is an out-neighbor of $x$ which belongs to $P$ by definition of $\mathcal{S}$. Conversely, if $x$ has an out-neighbor $y$ which belongs to $\mathcal{S}$ and $s(x)$ is not defined, we can extend it by putting $s(x) = y$, contradicting the maximality of $s$, so in fact $s(x)$ must be defined and $x\in N$.

[Comment: the whole point of taking a maximal strategy $s$ is that it's not obvious that if the first player has some positional strategy from every out-neighbor of $x$ then we can unify them in some common positional strategy: this works fine for historical strategy, but for positional strategies it seems to me that some maximality argument is unavoidable.]

Finally, let $D = G\setminus (P\cup N)$ be the set of remaining positions. By the remarks above, $x\in G$ belongs to $D$ iff (i′) all its out-neighbors are in $D$ or $N$ and (ii′) at least one belongs to $D$.

But then, if we define a partial function $t$ on $G$ by $t(x) = s(x)$ if $s(x)$ is defined (i.e., $x\in N$) and if $x\in D$ by choosing for $t(x)$ an out-neighbor of $x$ which belongs to $D$ (which exists because of (ii′)), then $t$ is a positional strategy which guarantees that either player survives (because if $x\in D$ then $t(x) \in D$ and the game will last forever unless some player makes the mistake of moving outside $D$, meaning inside $N$ because of (i′), and whichever player does this loses).

This shows determinacy. Lastly, if $\Psi\colon G\rightharpoonup \{\mathrm{P},\mathrm{N}\}$ is the partial function defined by $\Psi(x) = \mathrm{P}$ iff $x\in P$ and $\Psi(x) = \mathrm{N}$ iff $x\in N$, then it has the properties (i†) $\Psi(x) = \mathrm{N}$ if for some out-neighbor $y$ of $x$ the value $\Psi(y)$ is defined and is $\mathrm{P}$ and (ii†) $\Psi(x) = \mathrm{P}$ if for all out-neighbors $y$ of $x$ the value $\Psi(y)$ is defined and is $\mathrm{N}$; but any intersection of functions satisfying (i†) and (ii†) also does so, so there is a smallest function $\Phi$ satisfying (i†) and (ii†), and clearly if $\Phi(x)$ is undefined then both players have a surviving strategy from there with the same argument as above, so in fact $\Phi = \Psi$ and both “if”s in (i†) and (ii†) can be replaced by “iff”s.