Say that a clopen 3-player game is a well-founded tree $T\subseteq\omega^{<\omega}$; intuitively, starting with player $1$ and continuing cyclically, the players $1,2,3$ alternately play natural numbers for $\omega$-many rounds. Together they build an element $\xi$ of $\omega^\omega$, which is then a "$1$-win," "$2$-win," or "$3$-win" depending on the mod-$3$ value of the smallest $n$ with $\xi\upharpoonright n\not\in T$ (this is the "misere" version of what one might normally expect, but it seems ultimately simpler to think about unique winners than unique losers).

"3-player clopen determinacy" is a bit tricky to formulate. It's certainly not true that some player must have a non-losing strategy: consider the game $\mathsf{Spite}$ in which (essentially) player $1$ decides which of players $2$ or $3$ will win. However, let $\Sigma$ be the set of formulas built from three propositional atoms $w_1,w_2,w_3$, three modalities $\Diamond_1,\Diamond_2,\Diamond_3$, negation, and countable conjunctions and disjunctions. Each clopen 3-player game $T$ determines a Kripke frame + valuation for $\Sigma$ as follows:

  • The worlds of the frame are the sets $(P_1,P_2,P_3)$ with $P_i$ a quasistrategy for player $i$.

  • There are three accessibility relations, with the $i$th accessibility relation corresponding to player $i$ refining their quasistrategy, e.g. $$(P_1,P_2,P_3)\rightarrow_2(Q_1,Q_2,Q_3)\quad\iff\quad P_1=Q_1,P_2\supseteq Q_2, P_3=Q_3.$$ The semantics for $\Diamond_i$ follows $\rightarrow_i$ in the usual way.

  • The propositional atom $w_k$ is true at the world $(P_1,P_2,P_3)$ iff some play in which player $i$ follows $P_i$ results in a win for player $k$ (= player $k$ is first to "fall off $T$").

Let $M_T$ be the set of formulas in $\Sigma$ true in the Kripke frame + valuation gotten from $T$ in the manner above. For example, allowing the usual abbreviations, $M_{\mathsf{Spite}}$ contains the sentence $$\Diamond_1\Box_2 w_3\wedge\Diamond_1\Box_3w_2.$$

Finally, let $$M_{\mathsf{all}}=\bigcap_{T\in\mathbb{WF}}M_T$$ (where $\mathbb{WF}$ is the set of all well-founded trees on $\omega$) be the set of countable infinitary modal sentences true of all clopen 3-player games in the above sense.

My question is essentially: what is the complexity of $M_{\mathsf{all}}$? There are a few ways to make this precise, and the following seems most natural to me. Identifying $\Sigma$ with an appropriate coanalytic subset of $\omega^\omega$ as usual, I'd like to know if $M_{\mathsf{all}}$ is "Borel-on-the-codes" (a la Dougherty-Kechris):

Is there a Borel set $B$ such that $B\cap \Sigma=M_{\mathsf{all}}$?

I suspect that the answer is yes, and that in fact $M_{\mathsf{all}}$ is about as simple as it could conceivably be, but I don't immediately see how to prove that.

Of course the only thing special about $3$ here is that it is greater than $2$; I suspect there is no real difference between $3$ and $n$ for $3<n<\omega$, but I'd be extremely interested in any evidence to the contrary!

  • $\begingroup$ This is hopefully more tractable than a couple earlier questions of mine (1, 2), which focused on 2-player but worse-than-clopen games. $\endgroup$ Commented Feb 15, 2023 at 18:45

1 Answer 1


The "finitary part" $M_{\mathsf{fin}}$ of $M_{\mathsf{all}}$ is decidable (which may be evidence that the answer to the full question is yes). Namely, there is an effective translation mapping finitary $3$-modal formulas to monadic sentences of $\mathsf{MSO}(2^{<\omega},S_0,S_1)$ (monadic second-order theory of full binary tree; decidable by a classical result of Rabin[1]), such that the original formula is in $M_{\mathsf{fin}}$ iff its translation is true.

We represent a well-founded tree $T\subseteq \omega^{<\omega}$ as a binary tree $T'\subseteq 2^{<\omega}$, $$T'=\{(1^{k_0},0,\ldots,0,1^{k_{n-1}}),(1^{k_0},0,\ldots,0,1^{k_{n-1}},0) \mid (k_0,\ldots,k_{n-1})\in T\}.$$ A quasi-strategy on $T$ is represented as a subset $P$ of $T'$ s.t. for any non-leaf $(1^{k_0},0,\ldots,0,1^{k_{n-1}},0)\in T'$ there is some $(1^{k_0},0,\ldots,0,1^{k_{n-1}},0,1^{k_n})\in P$ (indicating possible moves from given positions). A play $X$ is a path through $2^{<\omega}$ that does not end with an infinite sequence of $1$'s. A play is compatible with a quasi-strategy $P$ if for any $s$, $s0\in X$ implies that for some $s01^k\in P$ we have $s01^k0\in X$. Thus we could express the property of three quasi-strategies to lead to a win for a player $i$. Hence we obtained an interpretation parametrized by representation of well-founded trees of the desired Kripke frames in $\mathsf{MSO}(2^{<\omega},S_0,S_1)$.

Now we obtain the desired translation as simply the standard translation of modal formulas over a Kripke model to first-order formulas over the same Kripke model treated as a first-order structure where we put on top the quantifier over Kripke models.

[1] Rabin, M. O. (1969). Decidability of second-order theories and automata on infinite trees. Transactions of the american Mathematical Society, 141, 1-35.

  • $\begingroup$ As always this is quite nice. Thanks! Do you happen to know of any further sources on the three-player-modal stuff a la the OP (I have a bunch of probably-easy questions but I'd like to avoid reinventing wheels)? $\endgroup$ Commented Feb 17, 2023 at 16:37
  • $\begingroup$ Unfortunately not, I answered your question without any prior knowledge of >2 player infinite games. $\endgroup$ Commented Feb 17, 2023 at 20:08
  • $\begingroup$ Belatedly, I just realized I misremembered my own question: I'm asking about an infinitary propositional modal logic, and this answer just addresses the finitary fragment (it doesn't actually make sense to say that $M_{all}$ is decidable). Do you know if these arguments can extend to address the full question? $\endgroup$ Commented Mar 7, 2023 at 19:41
  • $\begingroup$ @NoahSchweber I don't know. Pretty much sure it wouldn't be possible to simply apply Rabin Tree Theorem. Perhaps, one could try to extract some insight from one of the proofs of the theorem. But I do not immediately see how to do this. $\endgroup$ Commented Mar 7, 2023 at 19:56
  • $\begingroup$ I've taken the liberty of tweaking the opening of this answer. $\endgroup$ Commented Mar 14, 2023 at 15:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.