Elimination of quantifiers for the theory of equivalence relations with two infinite classes by back-and-forth As I said in an earlier question, I'm trying to understand how to obtain elimination sets by way of back-and-forth arguments. Since I'm not totally sure I understood how it works, I wanted to check my understanding by working through a rather simple example. Since the theory of equivalence relations is rather simple, I thought I might as well start with it; so I'd be really grateful if someone could point out any mistakes in the following argument. But first, a couple of definitions and a lemma, taken from Hodges's Model Theory (Section 3.3). I'm assuming throughout that every structure is an $\mathcal{L}$-structure and thus that every formula is an $\mathcal{L}$-formula):
Definition 1: An unnested Enhrenfeucht-Fraïssé game of length $k$, in symbols $\mathrm{EF}_k [(\mathcal{A}, \bar{a}), (\mathcal{B}, \bar{b})]$, is a game between two players, $\exists$ and $\forall$, such that, at the $i$th move in the game, $\forall$ must choose an element from either $\mathcal{A}$ or $\mathcal{B}$; then player $\exists$ chooses an element from the other structure. $\exists$ wins the game if, at the end of the play, the players have chosen $k$-tuples $\bar{c}$ and $\bar{d}$ from $\mathcal{A}$ and $\mathcal{B}$, respectively, such that, for every unnested atomic formula $\phi$, $\mathcal{A} \models \phi(\bar{a}, \bar{c})$ iff $\mathcal{B} \models \phi(\bar{b}, \bar{d})$; otherwise, Player $\forall$ wins. If $\exists$ wins, then we write $(\mathcal{A}, \bar{a}) \sim_k (\mathcal{B}, \bar{b})$.
Let now $\mathscr{K}$ be a class of structures. For each $\mathcal{A} \in \mathscr{K}$, let $\mathrm{tup}(\mathcal{A})$ be the set of all pairs $(\mathcal{A}, \bar{a})$, with $\bar{a}$ a tuple from $\mathcal{A}$, and let $\mathrm{tup}(\mathscr{K})$ be the union of all $\mathrm{tup}(\mathcal{A})$ for $\mathcal{A} \in \mathscr{K}$. 
Definition 2: By an unnested graded back-and-forth system for $\mathscr{K}$, we mean a family of equivalence relations $(E_k \; : \; k \in \omega)$ such that:
(1) if $\bar{a} \in \mathrm{tup}(\mathcal{A})$ and $\bar{b} \in \mathrm{tup}(\mathcal{B})$, then $\bar{a}E_0\bar{b}$ iff for every unnested atomic formula $\phi(\bar{x})$, $\mathcal{A} \models \phi(\bar{a})$ iff $\mathcal{B} \models \phi(\bar{b})$;
(2) if $\bar{a} \in \mathrm{tup}(\mathcal{A})$ and $\bar{b} \in \mathrm{tup}(\mathcal{B})$, then $\bar{a}E_{k+1}\bar{b}$ iff for every $c \in A$ there is $d \in B$ such that $\bar{a}cE_k\bar{b}d$.
Lemma 3.3.5: Suppose $(E_k : k \in \omega)$ is a graded back-and-forth system for $\mathscr{K}$. Suppose that, for each $n$ and $k$, $E_k$ has just finitely many equivalence classes on $n$-tuples, and each of these is definable by a formula $\chi_{k, n}(\bar{x})$. Then the set of all formulas  $\chi_{k, n}(\bar{x}) (k, n \in \omega)$ forms an elimination set for $\mathscr{K}$.
Thus, if we're looking for an elimination set, we can just look for graded back-and-forth systems and then use the Fraïssé-Hintikka theorem to obtain the desired set. I want to see if this works for the theory of equivalence relations with two equivalence classes, each of which finite.
So $\mathscr{K}$ be the class of all models of an equivalence relation with two distinct classes, each of which infinite. For any two structures $\mathcal{A}, \mathcal{B} \in \mathscr{K}$,and two tuples $(a_1, a_2), (b_1, b_2)$ taken from $\mathcal{A}, \mathcal{B}$, respectively, define $(a_1, a_2) E_0 (b_1, b_2)$ iff $a_1$ is in the same equivalence class of $a_2$ and $b_1$ is in the same equivalence class of $b_2$, or $a_1 = a_2$ and $b_1 = b_2$. Next, if $\bar{a}, \bar{b}$ are tuples from $\mathcal{A}, \mathcal{B}$, respectively, then $\bar{a} E_{k+1} \bar{b}$ iff for every $c \in A$, if $c$ is in the same equivalence class as one of the $\bar{a}$, then there is a $d \in B$ such that $d$ is in the same equivalence class as one of the $\bar{b}$.
It seems to me that the above is a graded back and forth system, but I'm not very confident. Clearly, if $(a_1, a_2) E_0 (b_1, b_2)$, then $\mathcal{A} \models a_1 \sim a_2$ iff $\mathcal{B} \models b_1 \sim b_2$, and similarly for the equality formulas. But what about the induction step? If $\bar{a} E_{k+1} \bar{b}$ and $c \in A$ is such that it belongs to the equivalence class of one of the $\bar{a}$, then we can always find $d \in B$ which is also in the same equivalence class of $\bar{b}$. The problem is that this argument doesn't use anywhere the fact that the equivalence classes are infinite. Moreover, I'm not sure if each equivalence class of $E_k$ as defined can be defined by a formula (my guess would be a disjunction of atomic formulas). Can anyone help me with this?
 A: There are a few problems with what your definition of $E_0$.


*

*You haven't defined $E_0$ on the class of all tuples, just on the pairs (the $2$-tuples). When should singletons be $E_0$-related? What about triples?

*Your $E_0$ doesn't satisfy condition (1) of Definition 2. Suppose $\lnot (a_1\sim a_2)$ and $\lnot (b_1\sim b_2)$. Then $(a_1,a_2)$ and $(b_1,b_2)$ satisfy all the same atomic formulas (clearly $a_1\neq a_2$ and $b_1\neq b_2$). But according to your definition of $E_0$, $(a_1,a_2)$ and $(b_1,b_2)$ are not in the same $E_0$-class.

*For the same reason, your $E_0$ has infinitely many equivalence classes on $2$-tuples, so you won't be able to apply Lemma 3.3.5. 
Your description of $E_{k+1}$ also isn't very precise... the way you've written it, it doesn't sound like $\overline{a}E_{k+1}\overline{b}$ implies that $\overline{a}$ and $\overline{b}$ satisfy the same atomic formulas, which is a basic requirement (unfolding the inductive definition down to $E_0$).
To define a graded back and forth system for the theory of a single equivalence relation with two infinite classes, you can just take all the $E_k$ to be the same equivalence relation, defined by $\overline{a}E_k\overline{b}$ if and only if $\overline{a}$ and $\overline{b}$ satisfy the same atomic formulas (i.e. $\mathrm{qftp}(\overline{a}) = \mathrm{qftp}(\overline{b})$). You'll have to use infiniteness of the equivalence classes when you check condition (2) of Definition 2.
