How complicated are 3-player clopen determinacy facts?

Question

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!

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.