# Finite Model Property on the First-Order Theory of Two Equivalence Relations

I know that there is a first-order sentence $\varphi$ such that

• $\varphi$ is written in the vocabulary given by just two binary relation symbols $E_1$, $E_2$ (and hence, without the equality symbol*),
• $\varphi$ is satisfiable in a model where $E_1$ and $E_2$ are equivalence relations,
• $\varphi$ is not satisfiable in a finite model where $E_1$ and $E_2$ are equivalence relations.

This has to be true because the first-order theory of two equivalence relations is undecidable (see the paper A. Janiczak, Undecidability of some simple formalized theories, Fundamenta Mathematicae, 1953, 40, 131--139). However, I am not able to find any such formula.

Does anybody know an example of a formula (or a family) with these three properties?

Footnote *: The assumption of not allowing the equality symbol is not important. Indeed, if we know a formula with equality where the last two previous properties hold, then the formula obtained replacing all subformulas $x \approx y$ with the formula $E_1(x,y) \land E_2(x,y)$ also satisfies these two properties.

-
@bounmol: Can you use just one binary symbol $E_1$ and take $E_2 = E_1$? –  PEV Jan 10 '11 at 20:35
@Trevor: The first-order theory of one equivalence relation (effectively, the first-order theory of the equality symbol) is decidable, and any sentence that is satisfiable is satisfiable in a finite model. –  mjqxxxx Jan 10 '11 at 20:47
@mjqxxxx: So for finite models, we look at finite sets essentially? –  PEV Jan 10 '11 at 20:49
@Trevor: Yes, you must look at structures (or models) with finite universe. And as has been pointed above by mjqxxxx it is necessary to use both binary symbols. –  boumol Jan 10 '11 at 21:04
Would $FO^{2}(\sim, <, +1)$ work? –  PEV Jan 10 '11 at 21:18

Let's call two elements $x$ and $y$ $E_1$-neighbors if $(x \neq y \wedge E_1(x, y))$, and $E_2$-neighbors if $(x \neq y \wedge E_2(x, y))$. Then the following assertions should suffice to force an infinite model:
1. Every element has exactly one $E_1$-neighbor.
2. There exists an element with no $E_2$-neighbor; every other element has exactly one $E_2$-neighbor.
In particular, the single element with no $E_2$-neighbor can be identified with $0$; and the remaining natural numbers are generated by alternating conditions 1) and 2).