# Quantifier elimination for theory of equivalence relations

Let $\mathcal{L}=\{\sim\}$ and $\Sigma_\infty$ be the set of axioms stating that:

(i) $\sim$ is an equivalence relation
(ii) Every equivalence class is infinite
(iii) there are infinitely many equivalence classes

It suffices to show that every $\mathcal{L}$ formula $\exists y\varphi(x,y)$ is $\Sigma_\infty$-equivalent to a quantifier free $\psi(x)$, where $x=(x_1,\ldots,x_n)$ are distinct variables, and $\varphi(x,y)$ is a conjunction of literals. Since it's fairly trivial when $\varphi(x,y)$ has a conjunct of the form $x_i=y$, we can assume we need to reduce $$\exists y (\bigwedge_{i\in I} x_i\not=y\wedge\bigwedge_{j\in J}x_j\sim y\wedge\bigwedge_{h\in H}\neg (x_j\sim y))$$ My question is whether or not the following condition holds:

$$\Sigma_\infty\vdash\exists y (\bigwedge_{i\in I} x_i\not=y\wedge\bigwedge_{j\in J}x_j\sim y\wedge\bigwedge_{h\in H}\neg (x_j\sim y))\leftrightarrow(\bigwedge_{j\in J,h\in H}\neg(x_i\sim x_j)\wedge\bigwedge_{j,j'\in J}x_j\sim x_{j'})$$ I can't think of a reason why it would not, but I'm a bit worried about ignoring the information about non-identical elements in the unreduced formula.

• I think that if you have infinitely many different equivalence classes, you have also infinitely many different elements, since the same element cannot belong to two different classes. Nov 26, 2015 at 5:44

The equivalence holds because the equivalence classes are infinite. If you have $(x_1,…,x_n)$ such that the RHS holds, the set $\{x_j \mid j\in J\}$ is finite. If it is nonempty, there is an element $y$ such that $y\sim x_j$ for $j\in J$ and $y\neq x_j$. If the set is empty, the existence of $y$ is implied by the fact that there are infinitely many equivalence classes, so you can pick a $y$ that is not $\sim$-equivalent to any $x_h,h\in H$.