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?

  • $\begingroup$ @hardmath - I edited the link. $\endgroup$ – 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.

  • $\begingroup$ 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.? $\endgroup$ – Nagase May 24 '16 at 0:52
  • $\begingroup$ Yes, that's true! $\endgroup$ – Alex Kruckman May 24 '16 at 1:46
  • $\begingroup$ 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. $\endgroup$ – Nagase Jun 12 '16 at 19:53
  • $\begingroup$ 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? $\endgroup$ – Nagase Jun 12 '16 at 19:54
  • $\begingroup$ 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. $\endgroup$ – Alex Kruckman Jun 12 '16 at 20:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.