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.