Stationary strategies in Choquet games

The (strong) Choquet game on a topological space $X$ is played as follows. There are two players, Empty and Nonempty, who alternate turns for infinitely many rounds. On round $i$, Empty moves first, choosing a point $x_i$ and an open neighborhood $U_i$ of $x_i$ and, if $i \geq 1$, such that $U_i \subseteq V_{i-1}$ (the open set that Nonempty played on the previous round). Then, Nonempty responds with an open neighborhood $V_i$ of the same point $x_i$ such that $V_i \subseteq U_i$. After all the rounds have been played, we obtain a descending sequence of open sets $$U_0 \supseteq V_0 \supseteq U_1 \supseteq V_1 \supseteq U_2 \supseteq V_2 \supseteq \cdots$$ together with a sequence of points $x_0,x_1,x_2,\dots$ Empty wins this play if $\bigcap_{i=0}^\infty V_i = \emptyset$; Nonempty wins if $\bigcap_{i=0}^\infty V_i \neq \emptyset$.

A Choquet space is a topological space $X$ such that Nonempty has a winning strategy in the Choquet game played on the topological space $X$. The Choquet game was originally designed by Choquet to give a topological characterization of which metrizable spaces admit a complete metric. However, not all Choquet spaces are metrizable. In general, the Choquet game turns out to be a good measure of completeness for topological spaces.

In the case of complete metric spaces $X$, Nonempty has a relatively simple winning strategy in the Choquet game on $X$. Once Empty has played the point-neighborhood pair $x_i \in U_i$, Nonempty responds by picking an open ball $V_i$ around $x_i$ that fits inside $U_i$ and has radius no larger than $1/2^i$. This forces Empty to play a Cauchy sequence of points $x_0,x_1,x_2,\dots$ whose limit witnesses that $\bigcap_{i=0}^\infty V_i \neq \emptyset$. Note that to carry out this strategy, Nonempty only needs to know the last move played by Empty and to remember which round is currently being played. In fact, with just a small change in strategy, Nonempty doesn’t even need to remember which round is being played: Nonempty simply needs to pick an open ball $U_i$ around $x_i$ whose radius is no larger than a quarter of the diameter of $V_i$ since that ensures that the radius of each open ball played by Nonempty decreases by at least one half at each step.

A strategy for Nonempty that only uses the last move played by Empty to decide what to play next is called a stationary strategy. Thus, we see that for a metrizable space $X$, the following are equivalent:

  1. $X$ admits a complete metric.
  2. Nonempty has a winning strategy in the Choquet game played on $X$.
  3. Nonempty has a stationary winning strategy in the Choquet game played on $X$.

Since the Choquet game makes sense for arbitrary topological spaces, it makes sense to ask whether items 2 and 3 are equivalent in the general case. This is not the case, but it is known that the equivalence holds for classes of spaces much broader than metrizable spaces.

In our paper [1], Carl Mummert and I show that the equivalence between the existence of general and stationary strategies for Nonempty in the Choquet game holds for an interesting class of spaces, which includes all second-countable T1 spaces. To state our main result, I must introduce an unusual property of topological bases. A base $\mathcal{B}$ for a topology is said to be open-finite if every open set has only finitely many supersets in $\mathcal{B}$. While it is unusual for a base to have this property, it turns out that many spaces happen to have such a base. For example, all second-countable T1 spaces have such a base. The main result of our paper is the following.

Theorem (Dorais–Mummert). Let $X$ be a topological space with an open-finite base. If Nonempty has a winning strategy in the Choquet game on $X$, then Nonempty has a stationary winning strategy in the Choquet game on $X$.

The method for proving this is new and interesting, but you will have to read our paper to find out…

The Choquet game appears to be tied with certain types of representability of topological spaces. Representability issues are very important in the context of reverse mathematics since second-order arithmetic offers very limited resources to talk about large multi-layered objects like topological spaces. In [2], Carl Mummert introduced a broad class of topological spaces that can be represented in second-order arithmetic: countably based maximal filter (MF) spaces. The basic datum for these spaces consists of a countable partial order $(\mathcal{P},{\leq})$, the points of the space is the class $MF(\mathcal{P},{\leq})$ of maximal filters on $(\mathcal{P},{\leq})$, and the basic open sets consist of all classes $U_p = \set{F \in MF(\mathcal{P},{\leq}) : p \in F}$. It is not hard to see that these second-countable spaces are all T1 and Choquet.

A topological characterization of countably based MF spaces was obtained by Carl Mummert and Frank Stephan [3], who established that the countably based MF spaces are precisely the second-countable T1 Choquet spaces. The original proof of this result is long and intricate. The existence of stationary winning strategies for Nonempty in such spaces leads to a much easier proof of this representation theorem. This proof was not included in our paper since it was too far from the main topic and not short enough to include in passing. Therefore, I am recording this proof here for prosperity.

Theorem (Mummert–Stephan). Every second-countable T1 Choquet space is homeomorphic to a countably based MF space.

Proof. Suppose that $X$ is a second-countable T1 Choquet space. Let $\mathcal{B}$ be a countable open-finite base for $X$, and let $\mathfrak{S}$ be a stationary strategy for Nonempty in the Choquet game on $X$. We will define a transitive relation ${\prec}$ on $\mathcal{B}$ such that $X$ is homeomorphic to $MF(\mathcal{B},{\preceq})$. (Although the notation suggests otherwise, the relation ${\prec}$ is not necessarily irreflexive.)

A natural choice for ${\prec}$ would be to define $V \prec U$ to hold if and only if $V \subseteq \mathfrak{S}(x,U)$ for some $x \in V$. However, this relation is not necessarily transitive. To remedy this, we define $V \prec U$ to hold if and only if there is a point $x \in V$ such that $V \subseteq \mathfrak{S}(x,W)$ for every $W \in \mathcal{B}$ such that $U \subseteq W$. This relation is clearly transitive. Moreover, since $\mathcal{B}$ is open-finite, there are only finitely many such $W$, so the intersection of all corresponding $\mathfrak{S}(x,W)$ is an open neighborhood of $x$. This guarantees that for every $x \in U$, there is a $V \in \mathcal{B}$ such that $x \in V$ and $V \prec U$.

We begin by recording a lemma that will be used repeatedly in this proof.

Lemma. For every maximal filter $F$ on $(\mathcal{B},{\preceq})$ there is a descending sequence $$\cdots \prec U_2 \prec U_1 \prec U_0$$ such that $F = \set{W \in \mathcal{B} : (\exists i)(U_i \preceq W)}$.

Proof. Since $F$ is countable and downward directed in $(\mathcal{B},{\preceq})$, it is easy to get a sequence $$\cdots \preceq V_2 \preceq V_1 \preceq V_0$$ such that $F = \set{W \in \mathcal{B} : (\exists i)(V_i \preceq W)}$. If this sequence is not eventually constant, we can eliminate repeated elements to obtain the a sequence as required by the lemma. Otherwise, we may assume that $V_0 = V_i$ for every $i$. As observed above, there must be some $U \in \mathcal{B}$ such that $U \prec V$. Since $F$ is a maximal filter in $(\mathcal{B},{\preceq})$, we must have $U = V$, which means that the constant sequence $U_i = U$ is as required by the lemma. QED

The first step of the proof is to define the map $h:MF(\mathcal{B},{\preceq}) \to X$ that will witness that the two spaces are homeomorphic. Fix $F \in MF(\mathcal{B},{\preceq})$, we will show that $\bigcap F$ is always a singleton, so that we may define $h(F)$ to be the unique point of $X$ that belongs to every element of $F$.

First find a descending sequence $$\cdots \prec U_2 \prec U_1 \prec U_0$$ that generates $F$ as in the above lemma. By definition of $\prec$, we can find corresponding points $x_1,x_2,\dots$ such that $x_i \in U_{i+1}$ and $U_{i+1} \subseteq \mathfrak{S}(x_i,U_i)$. This defines a valid sequence of moves for Empty against Nonempty’s stationary strategy $\mathfrak{S}$ in the Choquet game on $X$. Since $\mathfrak{S}$ is a winning strategy for Nonempty, it follows that $\bigcap_{i=0}^\infty U_i = \bigcap F$ is nonempty.

To see that $\bigcap F$ has only one point, suppose for the sake of contradiction that $\bigcap_{i=0}^\infty U_i$ contains two distinct points $x$ and $y$. Because $X$ is T1, we can find a neighborhood $V_0$ of $x$ in $\mathcal{B}$ that does not contain $y$. Define the descending sequence $$\cdots \prec V_2 \prec V_1 \prec V_0$$ so that $x \in V_{i+1}$ and $V_{i+1} \subseteq \mathfrak{S}(x,W)$ for every $W \in \mathcal{B}$ such that $V_i \cap U_i \subseteq W$. The filter $$G = \set{W \in \mathcal{B} : (\exists i)(V_i \preceq W)}$$ extends $F$ since $V_i \preceq U_i$ for each $i$. Since $V_0 \in G$ but $V_0 \notin F$, this contradicts the maximality of $F$.

Now that $h:MF(\mathcal{B},{\preceq}) \to X$ is properly defined, it remains to show that it is a homeomorhism. We first show that $h$ is a bijection, which we break into two facts:

  • $h$ is injective. Suppose that $F_0$ and $F_1$ are maximal filters that map to the same point $x$. By the lemma, we can find two sequences $$\cdots \prec U_2^d \prec U_1^d \prec U_0^d \qquad (d \in \set{0,1})$$ that generate these two filters. Since $x \in U_i^0 \cap U_i^1$ for each $i$, we can find another sequence $$\cdots V_2 \prec V_1 \prec V_0$$ of neighborhoods of $x$ in $\mathcal{B}$ such that $V_{i+1} \subseteq \mathfrak{S}(x,W)$ for every $W \in \mathcal{B}$ such that $U_i^0 \cap U_i^1 \cap V_i \subseteq W$. Then the filter $$G = \set{W \in \mathcal{B} : (\exists i)(V_i \preceq W)}$$ extends both $F_0$ and $F_1$, which means that $F_0 = G = F_1$.
  • $h$ is surjective. Let $U_0,U_1,U_2,\dots$ be an enumeration of $\mathcal{B}$ (possibly with repetitions). Given $x \in X$, define the descending sequence $$\cdots \preceq V_2 \preceq V_1 \preceq V_0$$ of neighborhoods of $x$ in $\mathcal{B}$ as follows. Pick $V_0 \in \mathcal{B}$ so that $x \in V_0$. If $x \in U_i$ then pick $V_{i+1}$ in such a way that $V_{i+1} \subseteq \mathfrak{S}(x,W)$ for every $W \in \mathcal{B}$ such that $V_i \cap U_i \subseteq W$; if $x \notin U_i$ then simply set $V_{i+1} = V_i$. Since $X$ is T1, we immediately see that $\bigcap_{i=0}^\infty V_i = \set{x}$. Therefore, any maximal filter extending $$F = \set{W \in \mathcal{B} : (\exists i)(V_i \preceq W)}$$ will map to $x$. (In fact, $F$ is already maximal.)

Since the choice of $V_0$ was essentially arbitrary in the process we just used to show that $h$ is surjective, for every $V_0 \in \mathcal{B}$ and every $x \in V_0$ we can find some $F \in MF(\mathcal{B},{\preceq})$ such that $V_0 \in F$ and $h(F) = x$. It follows that $$h(F) \in V_0 \quad\IFF\quad V_0 \in F,$$ which shows that $h$ is a homeomorphism. QED


[1] [doi] F. G. Dorais and C. Mummert, “Stationary and convergent strategies in Choquet games,” Fund. math., vol. 209, iss. 1, pp. 59-79, 2010.
@article {DoraisMummert10,
AUTHOR = {Dorais, Fran{\c{c}}ois G. and Mummert, Carl},
TITLE = {Stationary and convergent strategies in {C}hoquet games},
JOURNAL = {Fund. Math.},
FJOURNAL = {Fundamenta Mathematicae},
VOLUME = {209},
YEAR = {2010},
NUMBER = {1},
PAGES = {59--79},
ISSN = {0016-2736},
MRCLASS = {91A44 (06B35 54D20 54D70 91A24)},
MRNUMBER = {2652592 (2011h:91054)},
MRREVIEWER = {L{\'a}szl{\'o} Zsilinszky},
DOI = {10.4064/fm209-1-5},
URL = {},
EPRINT = {0907.4126}
[2] [doi] C. Mummert, “Reverse mathematics of MF spaces,” J. math. log., vol. 6, iss. 2, pp. 203-232, 2006.
@article {Mummert06,
AUTHOR = {Mummert, Carl},
TITLE = {Reverse mathematics of {MF} spaces},
JOURNAL = {J. Math. Log.},
FJOURNAL = {Journal of Mathematical Logic},
VOLUME = {6},
YEAR = {2006},
NUMBER = {2},
PAGES = {203--232},
ISSN = {0219-0613},
MRCLASS = {03B30 (03D45 03F35 06A06 06B35 54E50)},
MRNUMBER = {2317427 (2008d:03011)},
MRREVIEWER = {Christian Bennet},
DOI = {10.1142/S0219061306000578},
URL = {},
[3] [doi] C. Mummert and F. Stephan, “Topological aspects of poset spaces,” Michigan math. j., vol. 59, iss. 1, pp. 3-24, 2010.
@article {MummertStephan10,
AUTHOR = {Mummert, Carl and Stephan, Frank},
TITLE = {Topological aspects of poset spaces},
JOURNAL = {Michigan Math. J.},
FJOURNAL = {Michigan Mathematical Journal},
VOLUME = {59},
YEAR = {2010},
NUMBER = {1},
PAGES = {3--24},
ISSN = {0026-2285},
MRCLASS = {06E15 (03B30 03E15 54E52 91A44)},
MRNUMBER = {2654139 (2011k:06026)},
MRREVIEWER = {Jimmie D. Lawson},
DOI = {10.1307/mmj/1272376025},
URL = {},
EPRINT = {0912.3191}

A game-theoretic proof of Fraïssé’s Theorem

One of the important outcomes of the Fraïssé approach to model theory is that it is possible, in principle, to develop model theory from a strictly structural perspective, without ever mentioning formulas and their semantics. In practice, nobody really goes that far, but it is very useful to know about this radically different way to think about model theory. The key result that allows one to eliminate formulas is Fraïssé’s Theorem, which gives a combinatorial way to characterize when two structures with the same signature satisfy the same sentences. Ehrenfeucht, a student of Fraïssé, came up with a particularly elegant way to formulate Fraïssé’s ideas in terms of what are now called Ehrenfeucht–Fraïssé (EF) games (defined below).

Fraïssé’s Theorem. Let $A$ and $B$ be two relational structures with the same signature. Duplicator has a winning strategy in the EF game $G_n(A,B)$ if and only if $A$ and $B$ satisfy the same sentences of quantifier depth at most $n$. Therefore, $A$ and $B$ are elementarily equivalent if and only if Duplicator has a winning strategy in all of the EF games $G_n(A,B)$.

There are now many proofs of Fraïssé’s Theorem. Since the theorem mentions formulas and satisfaction, it is impossible to prove this result without talking about syntax and semantics. Most of the proofs I have seen use classical semantics à la Tarski. However, there are some alternatives to classical semantics. One such alternative are game semantics à la Hintikka. Since Fraïssé’s Theorem is so elegantly stated in terms of games, this seems like a very suitable choice.

It turns out that the game-theoretic proof of the forward implication of Fraïssé’s Theorem is rather short and elegant, at least when compared to the classical proof.1 The the approach is certainly not new, but I don’t remember if I got the idea from somewhere or if I pieced it together myself. In any case, since this proof is hard to find, I am posting it here for everyone to enjoy.2

Let’s start with some conventions. Fix a relational first-order language $\mathcal{L}$. (Constants can be added without trouble, but functions are a bit of a pain.) Throughout, $A$ and $B$ will denote two structures for the language $\mathcal{L}$. If $R$ is an atomic relation symbol, write $R^A$ and $R^B$ for the interpretation of $R$ in $A$ and $B$ respectively.

First, recall the definition of the Ehrenfeucht–Fraïssé (EF) game $G_n(A,B)$. This is a $n$-round game between two players Spoiler and Duplicator. On the $i$-th round:

  • Spoiler picks some $a_i \in A$ or some $b_i \in B$.
  • Duplicator picks some $b_i \in B$ or some $a_i \in A$ (the opposite of Spoiler’s choice).

After the $n$ rounds have been played, Duplicator wins if the correspondence $a_i \mapsto b_i$ defines a finite partial isomorphism from $A$ to $B$; otherwise, Spoiler wins. In particular, we need that $a_i = a_j \IFF b_i = b_j$ for this map to be well-defined and injective.

To simplify certain technical issues, we will use the fact that every formula $\phi$ is equivalent to a formula $\phi’$ with the same quantifier depth wherein negations only occur immediately before atomic relation symbols. It follows that it suffices to prove Fraïssé’s Theorem for the class of formulas obtained by closing the literals (atomic relations and their negations) under conjunction, disjunction, universal and existential quantification. We will call these restricted formulas of $\mathcal{L}$.3

Let $\phi$ be a restricted formula of $\mathcal{L}$ with free variables in $v_1,\dots,v_n$ and let $\lbrace v_1/a_1,\dots,v_n/a_n\rbrace$ be a variable assignment in the structure $A$. The semantic game $S_\phi(A)$, between two players True and False, is defined by induction on the complexity of $\phi$.

  • If $\phi \equiv R(v_{i(1)},\dots,v_{i(k)})$ where $R$ is a $k$-ary literal and $i(1),\dots,i(k) \in \set{1,\dots,n}$, then True wins if $R^A(a_{i(1)},\dots,a_{i(k)})$ holds, otherwise False wins.
  • If $\phi \equiv (\psi_1 \land \psi_2)$ then False chooses $i \in \set{1,2}$. Then the two players play the subgame $S_{\psi_i}(A)$.
  • If $\phi \equiv (\psi_1 \lor \psi_2)$ then True chooses $i \in \set{1,2}$. Then the two players play the subgame $S_{\psi_i}(A)$.
  • If $\phi \equiv (\forall v\,\psi)$ then False chooses $a \in A$ and adds $\lbrace v/a \rbrace$ to the variable assignment, replacing any previous assignment to $v$. Then the two players play the subgame $S_{\psi}(A)$.
  • If $\phi \equiv (\exists v\,\psi)$ then True chooses $a \in A$ and adds $\lbrace v/a\rbrace$ to the variable assignment, replacing any previous assignment to $v$. Then the two players play the subgame $S_{\psi}(A)$.

Note that the variable assignment is a tacit parameter to the game $S_\phi(A)$. It is easy to show that True has a winning strategy in the game $S_\phi(A)$ if and only if $A \vDash \phi$ (with the implicit variable assignment).

We are now ready to prove the forward implication of Fraïssé’s Theorem. Suppose that Duplicator has a winning strategy in the game $G_n(A,B)$. Let $\sigma$ be a restricted sentence of $\mathcal{L}$, with quantifier depth at most $n$, such that $A \vDash \sigma$. Then True has a winning strategy in the game $S_\sigma(A)$. We will use this strategy together with Duplicator’s winning strategy in $G_n(A,B)$ to define a winning strategy for True in $S_\phi(B)$. The strategy is defined by deconstructing $\sigma$ and keeping track of a play of the EF game $G_n(A,B)$ on the side.

Since $\sigma$ is a sentence, we start the games $S_\sigma(A)$ and $S_\sigma(B)$ with the empty variable assignment. We will play $S_\sigma(A)$ and $S_\sigma(B)$ in parallel in such a way that both games see the same formula at all times. Suppose we have reached the subformula $\phi$ of $\sigma$.

  • If $\phi \equiv (\psi_1 \land \psi_2)$ then we let False play in $S_\phi(B)$ by choosing $i \in \set{1,2}$, and we copy False’s move to $S_\phi(A)$.
  • If $\phi \equiv (\psi_1 \lor \psi_2)$ then we use True’s strategy in $S_\phi(A)$ to choose $i \in \set{1,2}$, and we copy this move to $S_\phi(B)$ as part of True’s strategy.
  • If $\phi \equiv (\forall v\,\psi)$ then we let False play in $S_\phi(B)$ by choosing $b \in B$. We let this $b \in B$ be Spoiler’s next move in our EF game $G_n(A,B)$. We then use Duplicator’s strategy in $G_n(A,B)$ to pick $a \in A$. We let this $a \in A$ be False’s next move in $S_\phi(A)$.
  • If $\phi \equiv (\exists v\,\psi)$ then we use True’s strategy in $S_\phi(A)$ to choose $a \in A$. We let this $a \in A$ be Spoiler’s next move in our EF game $G_n(A,B)$. We then use Duplicator’s strategy in $G_n(A,B)$ to pick $b \in B$. We choose this $b \in B$ as the next move in True’s strategy for $S_\phi(B)$.

The game ends when $\phi$ is a literal. Since $\sigma$ has quantifier depth at most $n$, we have played at most $n$ moves in the EF game $G_n(A,B)$. (If desired, finish this game by picking arbitrary moves for Spoiler and using Duplicator’s winning strategy to respond.) Suppose $\phi \equiv R(v_{i(1)},\dots,v_{i(k)})$. Since we always used True’s winning strategy to play in $S_\sigma(A)$, we know that $R^A(a_{i(1)},\dots,a_{i(k)})$ holds.

Now observe that by the way we played the quantifier moves, we have the correspondences $a_{i(1)} \mapsto b_{i(1)},\dots,a_{i(k)} \mapsto b_{i(k)}$ in the play of the EF game $G_n(A,B)$. Since we always used Duplicator’s winning strategy in $G_n(A,B)$, this correspondence is a finite partial isomorphism from $A$ to $B$, in particular $R^A(a_{i(1)},\dots,a_{i(k)})$ iff $R^B(b_{i(1)},\dots,b_{i(k)})$. Therefore, $R^B(b_{i(1)},\dots,b_{i(k)})$ and True wins the play of $S_\sigma(B)$. Since we always let False play freely in $S_\sigma(B)$, this shows that we have defined a winning strategy for True. Therefore, $B \vDash \sigma$, as required.


  1. The original version of this post claimed to have a game-theoretic proof of the backward implication of Fraïssé’s Theorem. Unfortunately, that proof was flawed and it has now been deleted.
  2. This proof was originally developed for a REU that I supervised at Cornell University in Summer 2008. It was originally posted on a blog that I used to maintain some years ago. Since I find this proof very interesting, I decided to salvage it and repost it here.
  3. The use of restricted formulas is a little bit of a cheat. The main reason for this was to simplify the definition of the semantic games. Negations can be incorporated in these games by adding the following clause to the definition of $S_\phi$: if $\phi \equiv \lnot\psi$, then True and False swap roles and play the subgame $S_\psi(A)$. The rest of the proof works exactly in the same way, except that because True and False swap roles every time they hit a negation, it becomes tricky to keep track of who is who.