Complexity of the pure theory of equality

173 Views Asked by At

The first-order pure theory of equality (Monk, Mathematical Logic, 240-242) has the equality predicate as its only (relation) symbol. Furthermore, I assume the convention in logic is that any interpretation of equality over a model should be the diagonal set $\{(m,m). m \in M\}$. If I'm not mistaken the quantifier-free fragment of this theory corresponds to equality logic (Kroening, D., Strichman, O., Decision procedures: an algorithmic point of view, Chapter 3) and there it is stated that it is NP-complete.

What is it known about the complexity of non quantifier-free fragments?

1

There are 1 best solutions below

5
On BEST ANSWER

For first-order logic with only equality as a whole, $\mathsf{PSPACE}$ is an easy upper bound. It turns out to be a lower bound as well, even in a very narrow special case: already the theory of a two-element pure set is $\mathsf{PSPACE}$-complete. See here.

Note that the theory of equality - that is, the set of sentences true in all pure sets, or equivalently the intersection of the theories of the pure sets - inherits the complexity of $Th({\bf 2})$. Specifically, for each equality-only sentence $\varphi$, consider the sentence $$\varphi':\quad[\exists x_1,x_2(x_1\not=x_2\wedge \forall y(y=x_1\vee y=x_2))]\implies\varphi.$$ This $\varphi'$ is trivially true in every pure set of size $\not=2$ and is true in ${\bf 2}$ iff ${\bf 2}\models\varphi$. So we get that $\varphi'$ is in the theory of equality iff $\varphi\in Th({\bf 2})$; since the construction of $\varphi'$ from $\varphi$ is sufficiently simple, this means that the theory of equality is at least as complicated as $Th({\bf 2})$.