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!