# Hodges exercise 2.7.1: Quantifier elimination in dense linear orderings

In Hodges' A Shorter Model Theory, exercise 2.7.1 tells you to prove theorem 2.7.1, which says that the following five formulas are an elimination $\Phi$ set for the class of all dense linear orderings (with a signature consisting only of "$<$"):

• There is a first element
• There is a last element
• $x$ is the first element
• $x$ is the last element
• $x<y$

The way it should be done is fairly clear to me, there are some details but the big idea (lemma 2.7.4) is that for every formula $\theta$ of the form $\exists y \bigwedge_{i=1}^n \psi_i$, where each $\psi_i$ is either in $\Phi$ or the negation of a formula in $\Phi$, I have to show that $\theta$ is equivalent (in every DLO) to a boolean combination of the formulas in $\Phi$. This new formula cannot have any other free variables than those in $\theta$.

This is where I run into problems. There are formulas $\theta$ for which I cannot figure out how to eliminate the existential quantifier. Indeed, for which I intuitively feel it should not be possible. For example: $$\theta\longleftrightarrow\exists x \, \lnot(x\text{ is the last element})$$ This expresses that a structure has at least two elements in its domain. I cannot figure out how to express this as only a boolean combination of $\Phi$. I cannot write it trivially as $\top$ or $\bot$, since they must be equivalent to $\theta$ in every DLO, and obviously whether $\theta\leftrightarrow\top$ or $\theta\leftrightarrow\bot$ depends on if the DLO is a singleton or not.

Is there some way to reduce $\theta$ to a boolean combination of $\Phi$, and if not, what am I missing? Why can this formula not have its quantifier eliminated even though I know it is supposed to be possible?