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?

• @hardmath - I edited the link. – Nagase May 24 '16 at 1:45

There are a few problems with what your definition of $E_0$.

1. 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?

2. 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.

3. 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.

• Thanks, that was immensely helpful. I'll try to work out the details. Incidentally, does that mean that every theory of equivalence relations which specifies that there are exactly $n$ (or infinitely many) classes each of which with infinitely many members, has Q.E.? – Nagase May 24 '16 at 0:52
• Yes, that's true! – Alex Kruckman May 24 '16 at 1:46
• So, is the argument like this: let $\bar{a}$ and $\bar{b}$ be arbitrary tuples which satisfy the same q. f. formulas, and let $c \in A$. Either $c$ is in the same class as one of the $\bar{a}$ or not. If not, then all the $\bar{a}$ are in the same equivalence class (as there are only two), so the corresponding $\bar{b}$ are also in the same class, so choose $d$ from the other class. Otherwise, if $c$ is in the same class as $a_i$ for some $i$, pick $d$ in the corresponding class of $b_i$; as the classes are infinite, there will always be such a $d$ to pick. – Nagase Jun 12 '16 at 19:53
• Question: doesn't the same argument work if we're working with the theory of exactly $n$ equivalence classes each of which with exactly $m$ elements? – Nagase Jun 12 '16 at 19:54
• Yes, that theory will also have QE (for any $n$ and $m$ in $\{1,2,\dots,\infty\}$). Note, however, that as soon as you have two classes of different size such that one is finite, you'll lose QE, since the formula expressing "there are exactly $n$ elements in my equivalence class" won't be equivalent to any quantifier-free formula. – Alex Kruckman Jun 12 '16 at 20:05