Immerman (Descriptive Complexity, 1999) presents the EF games for existential monadic second order (Ajtai-Fagin games) on page 127. As $\exists$MSO on words is equivalent to regular languages, the game can be written as follows.
A language $L \subseteq \{a, b\}^*$ is regular if and only if Delilah has no winning strategy in the following game:
1. Samson chooses $c, m \in \mathbb{N}$,
2. Delilah chooses $w \in L$,
3. Samson chooses $c$ subsets $C_1^w, \ldots, C_c^w$ of the set of positions in $w$ (i.e. $\{0, \ldots, |w|-1\}$),
4. Delilah chosses $v \not\in L$ and $c$ subsets $C_1^v, \ldots, C_c^v$ of the set of positions in $v$,
5. Samson and Delilah play the $m$-turn EF game on $(\mathfrak{S}(w), C_1^w, \ldots, C_c^w)$ and $(\mathfrak{S}(v), C_1^v, \ldots, C_c^v)$,
where $\mathfrak{S}(w)$ is the structure associated with the word $w$, i.e. :
$$\mathfrak{S}(w) = \langle \{0, \ldots, |w|-1\}, SUCC, Q_a, Q_b \rangle$$
with $Q_l = \{p \;|\; w_p = l\}$, and $SUCC$ is the binary successor predicate.
I have two questions:
- How does one show that $\{a^nb^n \;|\; n \in \mathbb{N}\}$ is not regular, using an EF argument like this,
- Is it easier/harder to play those games (to show non-regularity) when one has an ordering rather than the successor relation? (Those are equivalent in existential MSO).