Generalised Quantifiers Based on Rabin-Mostowski Index

In this work we use (sequential, deterministic, finite-memory) transducers from one alphabet to another. Assume that $A_W$, $A_Y$ are some alphabets. A transducer $\tau$ from $A_W$ to $A_Y$ (denoted $\tau :A_W\twoheadrightarrow A_Y$) is a tuple $\tau =⟨A_W,A_Y,Q_{\tau },{\iota }_{\tau },{\delta }_{\tau }⟩$, where:

• $\mathrm{■}$

  $Q_{\tau }$ is a finite set of states,

• $\mathrm{■}$

  ${\iota }_{\tau }\in Q_{\tau }$ is the initial state,

• $\mathrm{■}$

  ${\delta }_{\tau }:Q_{\tau }\times A_W\to A_Y\times Q_{\tau }$ is the transition function.

Given an input $\omega$-word $\overline{w}=w_0{w}_1{w}_2\mathrm{\cdots }\in {(A_W)}^{\omega }$ we inductively define the run $\overline{\rho }\stackrel{\text{def}}{=}{\rho }_0{\rho }_1{\rho }_2\mathrm{\cdots }\in Q^{\omega }$ and the output $\omega$-word $\tau (\overline{w})\stackrel{\text{def}}{=}{y}_0{y}_1{y}_2\mathrm{\cdots }\in {(A_Y)}^{\omega }$ taking ${\rho }_0\stackrel{\text{def}}{=}{\iota }_{\tau }$ and $(y_n,{\rho }_{n+1})\stackrel{\text{def}}{=}{\delta }_{\tau }({\rho }_n,w_n)$ for all $n\in \mathbb{N}$.

Given two transducers $\tau :A_W\twoheadrightarrow A_Y$ and ${\tau }^{\prime }:A_Y\twoheadrightarrow A_Z$ it is easy to construct the composition of the two, namely a transducer $\theta :A_W\twoheadrightarrow A_Z$ such that for every $\overline{w}\in {(A_W)}^{\omega }$ we have $\theta (\overline{w})={\tau }^{\prime }\left(\tau (\overline{w})\right)$.

Assume that $i,j\in \mathbb{N}$ are natural numbers with $i\le j$. The (strong) parity index $P_{i,j}$ and the weak parity index $W_{i,j}$ are defined by the languages

An index is a pair $ℛ=⟨A_{ℛ},L_{ℛ}⟩$ that is either ${𝒫}_{i,j}=⟨\{i,i+1,\mathrm{\dots },j\},P_{i,j}⟩$ or ${𝒲}_{i,j}=⟨\{i,i+1,\mathrm{\dots },j\},W_{i,j}⟩$ for some $i,j\in \mathbb{N}$ with $i\le j$.

The typical names for indices are: Büchi for ${𝒫}_{1,2}$ (infinitely many times priority $2$), co-Büchi for ${𝒫}_{0,1}$ (finitely many times priority $1$), safety for ${𝒲}_{0,1}$ (reaching priority $1$ implies that we reject), and reachability for ${𝒲}_{1,2}$ (reaching priority $2$ implies that we accept).

A non-deterministic parity $\omega$-word automaton over an alphabet $A$ and of index $ℛ=⟨A_{ℛ},L_{ℛ}⟩$ is a tuple $𝒟=⟨A,ℛ,Q_{𝒟},{\iota }_{𝒟},{\delta }_{𝒟}⟩$, where:

• $\mathrm{■}$

  $Q_{𝒟}$ is a finite set of states,

• $\mathrm{■}$

  ${\iota }_{𝒟}\subseteq Q_{𝒟}$ is the set of initial states,

• $\mathrm{■}$

  ${\delta }_{𝒟}\subseteq Q_{𝒟}\times A\times A_{ℛ}\times Q_{𝒟}$ is the transition relation,

and moreover the automaton is complete¹¹1This technical assumption plays a role when considering weak indices of automata. in the sense that for every $q\in Q_{𝒟}$ and $a\in A$ there is at least one transition of the form $(q,a,k,q^{\prime })\in {\delta }_{𝒟}$.

A run of an automaton $𝒟$ over an input $\omega$-word $\overline{w}=w_0{w}_1{w}_2\mathrm{\cdots }\in A^{\omega }$ producing output $\omega$-word $\overline{k}=k_0{k}_1{k}_2\mathrm{\cdots }\in {(A_{ℛ})}^{\omega }$ is a sequence of states $\overline{\rho }={\rho }_0{\rho }_1{\rho }_2\mathrm{\cdots }\in {(Q_{𝒟})}^{\omega }$ such that ${\rho }_0\in {\iota }_{𝒟}$ and for every $n\in \mathbb{N}$ we have $({\rho }_n,w_n,k_n,{\rho }_{n+1})\in {\delta }_{𝒟}$. The $\omega$-word $\overline{w}$ is accepted by $𝒟$ if there exists a run of $𝒟$ over $\overline{w}$ producing an $\omega$-word $\overline{k}$ that belongs to $L_{ℛ}$.

The language of such an automaton, denoted $\mathrm{L}(𝒟)\subseteq A^{\omega }$, is the set of $\omega$-words $\overline{w}\in A^{\omega }$ that are accepted by $𝒟$. A language $L\subseteq A^{\omega }$ is $\omega$-regular if it is the language of some automaton.

An automaton is deterministic if ${\iota }_{𝒟}$ is a singleton and the transition relation ${\delta }_{𝒟}$ is in fact a function ${\delta }_{𝒟}:Q_{𝒟}\times A\to A_{ℛ}\times Q_{𝒟}$, in which case there is a unique run of $𝒟$ over every input $\omega$-word $\overline{w}\in A^{\omega }$.

Let $C$ be a finite set of colours. An edge labelling of a set $X$ is a function that to each edge $\{i,j\}\subseteq X$ (where $i\ne j$) assigns a colour from $C$. Given an edge labelling, we say that a set $I\subseteq X$ is monochromatic if all edges $\{i,j\}\subseteq I$ have the same colour.

An algebraic structure $⟨S,(\cdot )⟩$ with an associative binary operation $(\cdot )$ is called a semigroup. A monoid is a semigroup $S$ which contains a neutral element $\epsilon \in S$ such that $\epsilon \cdot s=s\cdot \epsilon =s$ for every $s\in S$. Every semigroup $S$ can be extended into a monoid $S_{+\epsilon }=S\cup \{\epsilon \}$ by adding a formal neutral element $\epsilon$ with product defined appropriately. An idempotent is an element $e\in S$ such that $e\cdot e=e$.

The following fact is a standard application of Ramsey theorem (cf. Theorem 2.2).

In this work we use Wilke algebras as representations of $\omega$-semigroups, as in Perrin and Pin [39]. A Wilke algebra $S$ consists of two sets $(S^{\mathrm{fin}},S^{\inf })$, two product operations

denoted $s\cdot s^{\prime }$ for operands $s,s^{\prime }$, and an operation $S^{\mathrm{fin}}\to S^{\inf }$ denoted $s^{\omega }$ for an operand $s\in S^{\mathrm{fin}}$. Moreover, the operations are required to satisfy natural associativity axioms, in particular $S^{\mathrm{fin}}$ needs to be a semigroup. Each finite Wilke algebra $S$ uniquely determines the infinite product operation $\odot :{(S^{\mathrm{fin}})}^{\omega }\to S^{\inf }$, which is associative. In particular $\odot (sss\mathrm{\cdots })=s^{\omega }$ and $\odot (s_0{s}_1\mathrm{\cdots })=s_0\cdot \odot (s_1{s}_2\mathrm{\cdots })$.

A homomorphism $\alpha$ between two Wilke algebras $S$ and $T$ is a pair of functions ${\alpha }^{\mathrm{fin}}:S^{\mathrm{fin}}\to T^{\mathrm{fin}}$ and ${\alpha }^{\inf }:S^{\inf }\to T^{\inf }$ that commute with all the operations of the algebras and with the infinite product $\odot$.

A canonical example of a Wilke algebra is $A^{𝖶}\stackrel{\text{def}}{=}⟨A^{+},A^{\omega }⟩$, where $A$ is an alphabet. The operations of this Wilke algebra are the concatenation $\cdot$, the infinite repetition $v^{\omega }\stackrel{\text{def}}{=}v\cdot v\cdot v\cdot \mathrm{\dots }\in A^{\omega }$ for $v\in A^{+}$, and the infinite product $\odot (v_0{v}_1{v}_2\mathrm{\cdots })\stackrel{\text{def}}{=}{v}_0\cdot v_1\cdot v_2\cdot \mathrm{\dots }\in A^{\omega }$ for $v_0,v_1,v_2,\mathrm{\dots }\in A^{+}$.

Associativity properties imply that if $\alpha :A^{𝖶}\to S$ is a homomorphism into a finite Wilke algebra then for every sequence of finite words $v_0,v_1,\mathrm{\dots }\in A^{+}$ we have

Note that if a Wilke algebra is finite then it can be represented as an input to an algorithm by providing its list of elements and “multiplication tables” for all the operations. The crucial fact about Wilke algebras is their ability to recognise $\omega$-regular languages, as stated by the following theorem.

Let $\overline{z}=z_0{z}_1{z}_2\mathrm{\cdots }\in {(S_{+\epsilon }^{\mathrm{fin}})}^{\omega }$ (recall that $S_{+\epsilon }^{\mathrm{fin}}$ is $S^{\mathrm{fin}}$ extended with a formal neutral element $\epsilon$). We say that $\overline{z}$ is saturated if it contains infinitely many symbols from $S^{\mathrm{fin}}$, that is, symbols different than $\epsilon$. In this case $\odot (\overline{z})$ is well-defined: we can erase all symbols $\epsilon$ from $\overline{z}$ obtaining an $\omega$-word ${\overline{z}}^{\prime }\in {(S^{\mathrm{fin}})}^{\omega }$ and put $\odot (\overline{z})\stackrel{\text{def}}{=}\odot ({\overline{z}}^{\prime })$. This definition again satisfies the associativity properties as in Formula 2.1.

Assume that $\alpha :A^{𝖶}\to S$ is a homomorphism into a finite Wilke algebra $S=(S^{\mathrm{fin}},S^{\inf })$. For every $\overline{w}=w_0{w}_1{w}_2\mathrm{\cdots }\in A^{\omega }$ this homomorphism defines the lookahead ${\mathrm{𝗅𝗄}}_{\alpha }(\overline{w})\in {(S^{\inf })}^{\omega }$ defined for each position $n\in \mathbb{N}$ as

Note that, while producing a letter on a position $n\in \mathbb{N}$, a transducer uses letters on positions $0,1,\mathrm{\dots },n$. On the other hand, a lookahead at position $n$ depends on positions $n+1,n+2,n+3,\mathrm{\dots }$ To create an output $\omega$-word whose output letters in $A_Y$ depend on both the past and the future of input $\omega$-words, we consider transducers whose output letters are functions $(S^{\inf }\to A_Y)$, and then we apply these functions to letters in $S^{\inf }$ produced by a lookahead.

To simplify the notation, we use the following shorthand: if $\overline{f}=f_0{f}_1{f}_2\mathrm{\cdots }\in {(A_X\to A_Y)}^{\omega }$ and $\overline{x}=x_0{x}_1{x}_2\mathrm{\cdots }\in {(A_X)}^{\omega }$, then $\overline{f}\bullet \overline{x}\in {(A_Y)}^{\omega }$ is defined for each position $n\in \mathbb{N}$ as ${(\overline{f}\bullet \overline{x})}_n=f_n(x_n)$.

A non-deterministic parity tree automaton over an alphabet $A$ and of index $ℛ=⟨A_{ℛ},L_{ℛ}⟩$ is a tuple $𝒜=⟨A,ℛ,Q_{𝒜},{\iota }_{𝒜},{\mathrm{\Delta }}_{𝒜}⟩$, where $Q_{𝒜}$ is a finite set of states, ${\iota }_{𝒜}\subseteq Q_{𝒜}$ a set of initial states, and ${\mathrm{\Delta }}_{𝒜}\subseteq Q\times A\times A_{ℛ}\times Q\times Q$ a transition relation. Again we require the automaton to be complete, that is, for every $q\in Q_{𝒜}$ and $a\in A$ it needs to contain at least one transition $(q,a,k,q_{𝙻},q_{𝚁})\in {\mathrm{\Delta }}_{𝒜}$.

A run of $𝒜$ over a tree $\tilde{t}\in {\mathrm{Tr}}_A$ producing an output tree $\tilde{\eta }\in {\mathrm{Tr}}_{A_{ℛ}}$ is a tree $\tilde{\rho }\in {\mathrm{Tr}}_{Q_{𝒜}}$ such that $\tilde{\rho }(\epsilon )\in {\iota }_{𝒜}$ and $(\tilde{\rho }(v),\tilde{t}(v),\tilde{\eta }(v),\tilde{\rho }(v𝙻),\tilde{\rho }(v𝚁))\in {\mathrm{\Delta }}_{𝒜}$ for all nodes $v\in {\{𝙻,𝚁\}}^{\ast }$. A tree $\tilde{t}\in {\mathrm{Tr}}_A$ is accepted by $𝒜$ if there exists a run of $𝒜$ over $\tilde{t}$ producing a tree $\tilde{\eta }$ such that for every branch $\overline{w}\in {\{𝙻,𝚁\}}^{\omega }$, the sequence $\tilde{\eta }(\overline{w}{\upharpoonright }_0)\tilde{\eta }(\overline{w}{\upharpoonright }_1)\tilde{\eta }(\overline{w}{\upharpoonright }_2)\mathrm{\cdots }\in {(A_{ℛ})}^{\omega }$ belongs to $L_{ℛ}$. The language of an automaton $𝒜$ is the set of trees which it accepts. A language $L\subseteq {\mathrm{Tr}}_A$ is a regular tree language if it is the language of some automaton $𝒜$.

A tree automaton is (top-down) deterministic if ${\iota }_{𝒜}$ is a singleton and ${\mathrm{\Delta }}_{𝒜}:Q\times A\to A_{ℛ}\times Q\times Q$ is a function.

Formulae of the MSO logic are evaluated in an appropriate structure, which in our case is $\mathbb{N}$ with the successor relation (in the case of $\omega$-words) or ${\{𝙻,𝚁\}}^{\ast }$ with the left-child and right-child relations (in the case of trees). Elements of the structure are called positions or nodes. Usually, a monadic variable in MSO represents a set of positions, which can be also seen as a word or a tree over the alphabet $\{0,1\}$, with $1$ indicating positions that are in the set. In this paper, we employ a seemingly more general setting, where each monadic variable $X$ represents a word or a tree over some alphabet $A_X$, possibly larger than $\{0,1\}$. In the sequel, we usually assume a fixed alphabet $A_X$ associated to each variable $X$, but sometimes we explicitly specify the alphabet next to a quantifier (writing e.g., $\exists X\in {(A_X)}^{\omega }.\phi (X)$). Then, for a letter $x\in A_X$ and for a first-order variable $v$ we have an atomic formula $X(v)=x$ checking whether the letter of $X$ at the position $v$ is $x$. This way of seeing monadic variables does not increase the expressive power of MSO, since a variable with values in $A_X$ can be represented by a tuple of $|A_X|$ usual set variables, which should be forced to partition the domain (even $\lceil \log |A_X|\rceil$ set variables suffice).

By equivalence between MSO and regular languages [10, 28, 40], we know that for every MSO formula $\phi (X_1,\mathrm{\dots },X_n)$ we can construct a deterministic parity $\omega$-word automaton (in the case of $\omega$-words) or a non-deterministic parity tree automaton (in the case of trees) over the alphabet $A_{X_1}\times \mathrm{\dots }\times A_{X_n}$ which accepts exactly those $\omega$-words / trees $\overline{w}$ over this alphabet for which $\phi ({\pi }_1(\overline{w}),\mathrm{\dots },{\pi }_n(\overline{w}))$ holds, where each ${\pi }_i(\overline{w})$ is obtained from $\overline{w}$ by projecting labels of all positions to their $i$-th coordinate. Note that the index of the constructed automaton depends on the formula $\phi$ and in general cannot be bounded [5, 34, 48].

To simplify the notation, we identify a structure $\overline{w}$ over such a product alphabet $A_{X_1}\times \mathrm{\dots }\times A_{X_n}$ with the tuple of structures $⟨{\pi }_1(\overline{w}),\mathrm{\dots },{\pi }_n(\overline{w})⟩$ over respective alphabets. In particular, for a formula $\phi (X_1,\mathrm{\dots },X_n)$ we can speak about the language of a formula which is defined as the set of structures $\overline{w}$ over $A_{X_1}\times \mathrm{\dots }\times A_{X_n}$ that satisfy $\phi ({\pi }_1(\overline{w}),\mathrm{\dots },{\pi }_n(\overline{w}))$. Due to the ability of translating formulae into automata, these languages are always regular.

We use the general framework of perfect information games of infinite duration played between two players (typically called Player $\mathrm{I}$ and Player $\mathrm{II}$). Such a game is given by a tuple $𝒢=⟨A,L_{𝒢},V_{𝒢}=V_{𝒢}^{(\mathrm{I})}\bigsqcup V_{𝒢}^{(\mathrm{II})},{\iota }_{𝒢},{\delta }_{𝒢}⟩$ where $A$ is an alphabet, $L_{𝒢}\subseteq A^{\omega }$ is a winning condition, $V_{𝒢}$ is a (possibly infinite) set of positions, partitioned into the positions of the respective players, ${\iota }_{𝒢}\in V_{𝒢}$ is an initial position, and ${\delta }_{𝒢}\subseteq V_{𝒢}\times A\times V_{𝒢}$ is an edge relation (again satisfying completeness property that each $v\in V_{𝒢}$ admits at least one edge $(v,a,v^{\prime })\in {\delta }_{𝒢}$). The letter $a\in A$ is called the label of an edge $(v,a,v^{\prime })\in {\delta }_{𝒢}$.

A play of such a game is played in rounds, with the initial position $v_0={\iota }_{𝒢}$. In round number $n\in \mathbb{N}$ the player $P$ such that $v_n\in V_{𝒢}^{(P)}$ chooses an edge $(v_n,k_n,v_{n+1})\in {\delta }_{𝒢}$ moving to the next position $v_{n+1}$. After an infinite play, Player $\mathrm{II}$ wins if and only if $\overline{k}\stackrel{\text{def}}{=}{k}_0{k}_1{k}_2\mathrm{\cdots }$ belongs to $L_{𝒢}$. Classical theorems [27] imply that if $L_{𝒢}$ is sufficiently simple, then one of the players can ensure to win this game, that is, has a winning strategy. In general such a strategy for a player $P$ is a tree-shaped object but we mostly work with positional strategies, that is, functions ${\sigma }^{(P)}:V_{𝒢}^{(P)}\to {\delta }_{𝒢}$ such that for every $v\in V_{𝒢}^{(P)}$ we have ${\sigma }^{(P)}(v)=(v,k,v^{\prime })$ for some $k\in A$ and $v^{\prime }\in V_{𝒢}$.

A parity game of index $ℛ=⟨A_{ℛ},L_{ℛ}⟩$ is a game $𝒢$ as above where $A=A_{ℛ}$ and $L_{𝒢}=L_{ℛ}$.

Consider a new quantifier ${𝙸}_{ℛ}^{D}X.\phi (W,X)$ where $D\in \{\mathrm{𝖽𝗍},\mathrm{𝗇𝖽}\}$ determines the type of involved automata and $ℛ$ is an index (either a strong parity index ${𝒫}_{i,j}$ or a weak parity index ${𝒲}_{i,j}$). Such a formula holds for a parameter $\overline{w}\in {(A_W)}^{\omega }$ if there exists an automaton ${𝒜}_{\overline{w}}$ of index $ℛ$, which is either deterministic ($D=\mathrm{𝖽𝗍}$) or non-deterministic ($D=\mathrm{𝗇𝖽}$), such that for every $\overline{x}\in {(A_X)}^{\omega }$ the formula $\phi (\overline{w},\overline{x})$ holds if and only if ${𝒜}_{\overline{w}}$ accepts $⟨\overline{w},\overline{x}⟩$.

Note that the parameter $\overline{w}$ occurs in the above definition in two roles. First, the automaton ${𝒜}_{\overline{w}}$ may depend on the parameter $\overline{w}$. Second, the automaton, when verifying whether the given $\overline{x}$ makes $\phi (\overline{w},\overline{x})$ true, has access not only to $\overline{x}$ but also to the parameter $\overline{w}$ (in particular, the automaton is over the alphabet $A_W\times A_X$).

Note that both deterministic and non-deterministic index quantifiers make sense for both $\omega$-words and trees. Let MSO+$𝙸$ denote the extension of monadic second-order logic by index quantifiers.

As a natural way to study the index quantifier, we need to formalise within MSO the concept of the game quantifier $𝙶$ (see [22, § 20.D] and [7, 8, 18, 21, 29, 31]). This quantifier, written $𝙶X[1.0]\to Y$ (alternatively, in some papers the symbol $\mathrm{⅁}$ is used), binds two monadic variables $X$ and $Y$. A formula

holds, given a parameter $\overline{w}\in {(A_W)}^{\omega }$, if Player $\mathrm{II}$ has a winning strategy in the game $𝒢(\overline{w},\phi )$, defined as follows.²²2Classically, in the works of Moschovakis and Kechris [22, 31] the “game quantifier” requires Player $\mathrm{I}$ to win the game, however in automata-theoretic context (e.g., the Church synthesis problem [11, 41]) or Wadge games [47], it is more customary to focus on Player $\mathrm{II}$. The game consists of infinitely many rounds. In a round $n\in \mathbb{N}$, Player $\mathrm{I}$ proposes a letter $x_n\in A_X$ and Player $\mathrm{II}$ answers with a letter $y_n\in A_Y$. At the end, Player $\mathrm{II}$ wins if and only if $\phi (\overline{w},\overline{x},\overline{y})$ holds for $\overline{x}\stackrel{\text{def}}{=}{x}_0{x}_1{x}_2\mathrm{\cdots }\in {(A_X)}^{\omega }$ and $\overline{y}\stackrel{\text{def}}{=}{y}_0{y}_1{y}_2\mathrm{\cdots }\in {(A_Y)}^{\omega }$. This game can easily be represented by a formal game $𝒢$ with positions $V_{𝒢}^{(\mathrm{I})}\stackrel{\text{def}}{=}\mathbb{N}$ and $V_{𝒢}^{(\mathrm{II})}\stackrel{\text{def}}{=}\mathbb{N}\times A_X$ and $L_{𝒢}$ given by $\phi$; however we do not need to study the exact structure of this game.

Typically, one applies the game quantifiers in the context where the involved games are determined, although the definition makes sense even without this assumption.

Let MSO+ $𝙶$ denote the extension of monadic second-order logic by game quantifiers. Note that as it is defined, the game quantifier makes sense only for $\omega$-words, because the shape of the time-structure of a game of infinite duration is $\omega$.

We begin by discussing how game quantifiers introduced above can be viewed as generalised MSO quantifiers over the structure $\mathbb{N}$. To explain the idea, let us first take a simple example in first-order logic. Consider a formula

Clearly, its meaning in a structure $ℳ$ can be viewed as a game of two players, say $\exists$ and $\forall$, consisting of $4$ rounds. Now the block of $4$ quantifiers can be replaced by a single $4$-ary quantifier, so that the formula becomes $𝚀xy{x}^{\prime }{y}^{\prime }.\phi (\overrightarrow{w},x,y,x^{\prime },y^{\prime })$. The semantics of $𝚀$ is specified by a property that a $4$-ary relation $r$ in ${𝚀}^{ℳ}$ should possess. In terms of a game, in which Players $\mathrm{I}$ and $\mathrm{II}$ select in alternation elements of $M$, Player $\mathrm{II}$ should have a strategy to force the selected quadruple into $r$.

Now consider a formula $\phi (W,X,Y)$ interpreted in the structure $\mathbb{N}$, where $W$, $X$, $Y$ are set variables (more generally, they could be some tuples of set variables). Consider an infinite game, in which Players $\mathrm{I}$ and $\mathrm{II}$ select in alternation bits in $\{0,1\}$, so that the result is an infinite sequence

The sequences $x_0,x_1,x_2,\mathrm{\dots }$ and $y_0,y_1,y_2,\mathrm{\dots }$ constitute characteristic functions of some subsets $\overline{x}$ and $\overline{y}$ of $\mathbb{N}$, respectively. Now, for a valuation $W\mapsto \overline{w}$, a formula defined with the game quantifier

holds if Player $\mathrm{II}$ has a strategy to force that the formula $\phi (\overline{w},\overline{x},\overline{y})$ holds in $\mathbb{N}$. The game quantifier $𝙶$ can be defined as a binary generalised MSO quantifier. Its semantics ${𝙶}^{\mathbb{N}}$ is defined by a family of binary relations over $𝖯(\mathbb{N})$ that comprises all relations $R\subseteq 𝖯(\mathbb{N})\times 𝖯(\mathbb{N})$, such that in the game described above, Player $\mathrm{II}$ has a strategy to force the resulting pair $(\overline{x},\overline{y})$ into $R$. Then, indeed, the formula $𝙶X[1.0]\to Y.\phi (\overline{w},X,Y)$ holds precisely when the relation $\{(\overline{x},\overline{y})\mid \phi (\overline{w},\overline{x},\overline{y})\text{ holds in }\mathbb{N}\}$ belongs to ${𝙶}^{\mathbb{N}}$.

To present our new index quantifier ${𝙸}_{ℛ}^{D}X.\phi (\overrightarrow{W},X)$ as a generalised MSO quantifier, let us, for concreteness, focus on the MSO theory of the full binary tree, whose domain is ${\{𝙻,𝚁\}}^{\ast }$. As we have assumed that our automaton reads the values of both $\overrightarrow{W}$ and $X$, the construction does not fit into the unary case, but, like the game quantifier, it can be expressed as a binary quantifier, or more generally, $(k+\mathrm{\ell })$-ary quantifier (if $\overrightarrow{W}$ is a $k$-vector and $X$ an $\mathrm{\ell }$-vector).

For simplicity, let us consider $k=\mathrm{\ell }=1$; an extension to higher $k$, $\mathrm{\ell }$ is straightforward. The key point is to choose a class of binary relations over $𝖯({\{𝙻,𝚁\}}^{\ast })$ that would serve as the intended semantics of the quantifier. For a binary relation $r\subseteq 𝖯({\{𝙻,𝚁\}}^{\ast })\times 𝖯({\{𝙻,𝚁\}}^{\ast })$, and a set $K\in 𝖯({\{𝙻,𝚁\}}^{\ast })$, we define the cut of $r$ by $K$ as the binary relation

Recall that in our quantifier we are interested in automata of type $D$ and index $ℛ$. A pair of sets $(K,L)$ is accepted by an automaton (over the alphabet ${\{0,1\}}^2$) if so is its characteristic function, and a relation $r\subseteq 𝖯({\{𝙻,𝚁\}}^{\ast })\times 𝖯({\{𝙻,𝚁\}}^{\ast })$ is recognised by an automaton if it consists precisely of pairs that the automaton accepts. Now consider the class of relations

Then it is straightforward to see that the formula ${𝙸}_{ℛ}^{D}X.\phi (W,X)$ is equivalent to

where the semantics of the quantifier ${𝚀}_{ℛ}^D$ over trees is given by the class ${𝒞}_{ℛ}^D$.

Clearly, the variable $Z$ above plays only a technical role; therefore, for clarity of notation, in our paper we use the notation ${𝚀}_{ℛ}^{D}X.\phi (W,X)$, without $Z$.

Let us also remark that our proposal is not the only possible approach. One could also consider a unary quantifier ${𝚀}_{ℛ}^{D}X$, where a formula ${𝚀}_{ℛ}^{D}X.\phi (W,X)$ holds for a valuation $W\mapsto \tilde{w}$ if the language of all sets $\tilde{x}$ such that $\phi (\tilde{w},\tilde{x})$ holds is accepted by an automaton (of appropriate kind), without reading the parameter $\tilde{w}$, as discussed in Remark 3.1. That is, the semantics is given simply by a class of all languages accepted by automata of type $D$ and index $ℛ$.

While this may appear quite natural, we believe that such an extension would be less interesting. Not only it brings an undecidable formalism over $\omega$-words as indicated in Remark 3.1 but it additionally restricts available correlation between the involved variables. Indeed, if such a formula is satisfied by some $\tilde{w}$ which is not regular, then it follows from general properties of MSO (namely Regular Tree Theorem) that there is a regular ${\tilde{w}}^{\prime }$, such that the languages $\{\tilde{x}\mid \phi (\tilde{w},\tilde{x})\}$ and $\{\tilde{x}\mid \phi ({\tilde{w}}^{\prime },\tilde{x})\}$ coincide. Thus the relation defined by the formula $\phi (W,X)$, in some sense, necessarily weakly correlates its arguments. These issues require further investigation.

Let $𝒟$ be a deterministic parity automaton over the alphabet $A_W\times A_X\times A_Y$ of a strong parity index $ℛ=⟨\{i,i+1,\mathrm{\dots },j\},P_{i,j}⟩$ that is equivalent to $\phi$, that is, the automaton accepts an $\omega$-word $⟨\overline{w},\overline{x},\overline{y}⟩$ if and only if $\phi (\overline{w},\overline{x},\overline{y})$ holds.

Given an $\omega$-word $\overline{w}=w_0{w}_1{w}_2\mathrm{\cdots }\in {(A_W)}^{\omega }$, we can consider a parity game $𝒢(\overline{w},𝒟)$ obtained as a product of $𝒢(\overline{w},\phi )$ with the automaton $𝒟$, defined as follows.

It is easy to see that $𝒢(\overline{w},𝒟)$ is equivalent to $𝒢(\overline{w},\phi )$ in the sense that a player $P$ wins one game if and only if she wins another: the automaton $𝒟$ is deterministic, so there is a one-to-one correspondence between choices in $𝒢(\overline{w},\phi )$ and choices in $𝒢(\overline{w},𝒟)$, so that strategies from one game can be directly transferred to the other game. Moreover, due to positional determinacy of parity games (see Theorem 2.5), Player $\mathrm{II}$ wins $𝒢(\overline{w},\phi )$ if and only if Player $\mathrm{II}$ has a positional winning strategy in $𝒢(\overline{w},𝒟)$.

A positional strategy ${\sigma }^{(\mathrm{II})}$ of Player $\mathrm{II}$ in $𝒢(\overline{w},𝒟)$ can be represented by an $\omega$-word $\overline{\sigma }={\sigma }_0{\sigma }_1{\sigma }_2\mathrm{\cdots }\in {\left(Q\times A_X\to A_Y\right)}^{\omega }$, where $Q$ is the set of states of $𝒟$: in this $\omega$-word, the letter ${\sigma }_n$ satisfies ${\sigma }_n(q,x)=y$ where ${\sigma }^{(\mathrm{II})}(n,q,x)=((n,q,x),k,(n+1,q^{\prime }))$ with ${\delta }_{𝒟}(q,(w_n,x,y))=(k,q^{\prime })$. The following claim is straightforward, as MSO allows us to quantify over infinite plays in $𝒢(\overline{w},𝒟)$ and can express the parity condition ${𝒫}_{i,j}$.

It follows that the formula $𝙶X[1.0]\to Y.\phi (W,X,Y)$ is equivalent to

where the set $\left(Q\times A_X\to A_Y\right)$ is finite and therefore one can treat it as an alphabet. Consequently, this formula belongs to pure MSO. $◀$

Using the above lemma to inductively eliminate an innermost game quantifier, we immediately obtain the following corollary.

The above remark can be seen as a modern version of a proof of the Büchi-Landweber theorem [11], based on determinacy of parity games. This means that the proposed procedure of elimination of a game quantifier can be seen as a parametrised version of the construction of Büchi and Landweber, where we search for a strategy that may depend on the parameter $\overline{w}\in {(A_W)}^{\omega }$.