Quantifier elimination exercise

Question

Let $L$ be the language $\{c_n : n \in \mathbb{N} \}$, and $T$ the theory $\{c_i \neq c_j : i < j < \omega \}$. I want to show that $T$ has quantifier elimination (QE).

It suffices to show QE for formulas of the form $\exists x \, \varphi(x, \bar{y})$, where $\varphi$ is a conjunction of literals. Moreover, since logically

$$ \exists x(\varphi(x, \bar{y}) \land \psi(\bar{y})) \leftrightarrow \exists x \, \varphi(x, \bar{y}) \land \psi(\bar{y}) $$

we can assume $\varphi$ is a conjunction of atoms $x = y_i$, $x = c_j$, $x \neq y_n$, $x \neq c_m$. But then clearly $\exists x \, \varphi \leftrightarrow \bot$ or $\exists x \, \varphi \leftrightarrow \top$.

I must have misunderstood something, because this is supposed to be a (relatively) tough exercise. Any help?

Answer 1

The formula $$\exists x\, (x = y \land x = z)$$ is not equivalent to $\top$ or $\bot$, it's equivalent to $y = z$. So you have more cases to consider involving variables. I still wouldn't say the exercise is tough, but you have to be very careful not to overlook anything! (It's better to avoid writing "clearly"...)

Answer 2

As it looks like the OP has most or all of the main ideas, I'm just going to give a demonstration of what I would consider a good informal proof.

---

We want to prove that for any formula¹ $\varphi$, there is a formula $\varphi'$ which doesn't contain any quantifiers such that $\varphi$ is logically equivalent to $\varphi'$.

We can eliminate universal quantifiers by reducing them to existential quantifiers via $\forall x.\psi(x)\iff \neg\exists x.\neg\psi(x)$. If we can handle the case $\exists x.\psi(x)$ where $\psi$ has no quantifiers, we can handle the general case by structural induction on formulas, i.e. eliminating quantifiers in a bottom-up fashion. Since $\psi(x)$ is a(n instance of a) propositional formula, we can put it into disjunctive normal form. By distribution of existential quantification over disjunction, this reduce the problem to the case where $\psi(x)$ is a conjunction of literals. Further, via $\exists x.\psi(x)\land\chi\iff(\exists x.\psi(x))\land\chi$ where $x$ does not occur in $\chi$, we can assume that $x$ occurs in all literals. The only literals are then $x=a$ and $x\neq a$ where $a$ is either a constant or a (free) variable

If $x=a$ is a literal, then we can eliminate all occurrences of $x$ by replacing them with $a$ at which point we can eliminate the quantifier via null quantification. (Except when $a$ is $x$ but then we can drop $x=x$ immediately.) The remaining case is then where all literals are of the form of $x\neq a_i$. (If one of the $a_i$ is $x$, then we can immediately reduce the conjunction to $\bot$.) Conceptually, $\psi(x)$ would then correspond to the statement that $x$ is not one of a finite set of terms, namely the $a_i$. Because the theory asserts that we have infinitely many distinct constants, $\exists x.\psi(x)$ is therefore always true², i.e. is equivalent to $\top$ eliminating the quantifier. $\square$

---

If I was communicating with an expert, I would probably just say that we can reduce to a conjunction of formulas of the form $x\neq a_i$ which states that $x$ is not one of a finite set of values, but the theory asserts that there are infinitely many distinct values. All the other quantifiers can be eliminated for purely logical reasons.

¹ All formulas, not just closed formulas.

² This alludes to a semantic argument and then requires completeness if we want to show provability and not just semantic entailment. This could be improved by describing how to actually produce the formal proof. For example, how do we prove $(\exists x.x\neq y)\leftrightarrow \top$? Obviously the idea is that either $y$ is one of the constants and we can just pick any of the others, or $y$ is none of them and we can pick any constant. The problem is that we don't know which (if any) $y$ is. It isn't hard to resolve this, but it is an extra step that is needed depending on the notion of logical equivalence you're using and whether you want to assume completeness or not.