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?
You're absolutely right, this is a mistake in Hodges.
No doubt Hodges was only thinking about infinite dense linear orders (or, equivalently, dense linear orders with at least two elements).
It seems to me that you can fix the exercise by either