# How complicated are 3-player clopen determinacy facts?

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, but I'd be extremely interested in any evidence to the contrary!

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

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.

• 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)? Commented Feb 17, 2023 at 16:37
• Unfortunately not, I answered your question without any prior knowledge of >2 player infinite games. Commented Feb 17, 2023 at 20:08
• 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? Commented Mar 7, 2023 at 19:41
• @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. Commented Mar 7, 2023 at 19:56
• I've taken the liberty of tweaking the opening of this answer. Commented Mar 14, 2023 at 15:17