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

  1. Restricting the class to infinite dense linear orders, or
  2. Adding sentences "There are no elements" and "There is exactly one element" to your elimination set (Hodges explicitly allows empty structures).
  • $\begingroup$ Actually, now that I thought of looking it up, in chapter 2.2 Hodges has a list of axiomatizations of various structures. Among them are the dense linear orderings, and they are indeed defined to have at least two points... $\endgroup$ – elWanderero Dec 12 '15 at 19:24
  • $\begingroup$ Really? In my copy only "linear orders" and "dense linear orders without endpoints" are axiomatized (and the latter are obviously always infinite). $\endgroup$ – Alex Kruckman Dec 12 '15 at 19:34
  • $\begingroup$ Sorry you're right. Wishful reading on my part. $\endgroup$ – elWanderero Dec 12 '15 at 20:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.