# Quantifier elimination exercise

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?

• $\exists x.y=z$ is not equivalent to $\top$ or to $\bot$. – Derek Elkins May 10 at 17:42
• @DerekElkins The OP handled this case by factoring out literals that don't refer to $x$ (by rewriting $\exists x\, (y = z)$ as $(\exists x\, \top) \land (y = z))$. – Alex Kruckman May 10 at 18:37
• @AlexKruckman It's not completely clear that the OP's argument covers that case, though that would be a super-technical nitpick. Of course, it's straightforward to adapt it to the OP's template while retaining the problem. $\exists x.x=y\land x=z$. – Derek Elkins May 10 at 18:56
• @DerekElkins As in the answer I posted :0) – Alex Kruckman May 10 at 19:00
• @Joachim You should also be somewhat concerned that your "proof" doesn't seem to overtly rely on the axioms of the theory. At minimum, I would expect an informal proof of this to point out where the axioms of the theory are relevant or to show why they aren't relevant. – Derek Elkins May 10 at 19:09

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"...)

• Writing "clearly" can be very useful; it makes it easier for people to find the mistake. – Andreas Blass May 10 at 20:14
• @AndreasBlass Haha - indeed! – Alex Kruckman May 10 at 20:29
• Oh, silly me! Must be the Ramadan... But other than that there are not many more cases? I mean, I have to write it out a bit more detailed, but I don't see any further insight or trick required to solve this problem. Maybe I am confused because it is listed as a difficult exercise. – Joachim May 10 at 20:48
• No, there's no further insight - I agree with you, it's not difficult. @Joachim – Alex Kruckman May 10 at 20:49

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 formula1 $$\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 true2, 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.

1 All formulas, not just closed formulas.

2 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.