I am struggling to understand Quantifier Elimination as it is treated in Hodges' "A Shorter Model Theory". The relevant definitions are :

Definition: Take $K$ to be a class of $L$-structures, for $L$ a first-order language. An elimination set for $K$ is a set of formulas $\Phi \subseteq L$ such that for every formula $\phi (\bar{x}) \in L$ there is a formula $\phi^{*}(\bar{x}) \in \Phi$ which is a boolean combination of formulas in $\Phi$ and $\phi(\bar{x})$ is equivalent to $\phi^{*}(\bar{x})$ in every structure in K

Definition: Let $T$ be a first-order $L$ theory. $T$ has quantifier elimination if the set of quantifier-free formula in $L$ forms an elimination set for all models of $T$.

Hodges talks about a process where starting with a class $K$ of $L$-structures, a theory $T$ serving as a candidate for axiomatization of $K$, and a set of $L$-formula $\Phi$ that serves as a candidate for an elimination set for $K$. And we build up $T$ and $\Phi$ simultaneously, using the following theorem:

Theorem: Suppose that every atomic formula of $L$ is in $\Phi$, and for every formula $\theta(\bar{x}) \in L$ which is of the form $\exists y \bigwedge_{i < n} \psi_{i}(\bar{x}, y)$ with each $\psi_{i}$ in $\Phi$ or a negation of a formula in $\Phi$, there is a formula $\theta^{*}(\bar{x})$ of $L$ which

(i) is a boolean combination of formulas in $\Phi$ and,

(ii) is equivalent in every structure of $K$

Then $\Phi$ is an elimination set for $K$

But I am not sure what is meant specifically or intuitively. If someone could shed some light on this and help me understand what this process looks like or means, I would greatly appreciate it.

  • $\begingroup$ This theorem is just one way to prove quantifier elimination. Can you be more specific about what's confusing you? Is it 1) the meaning of quantifier elimination, 2) the meaning of this theorem, 3) how to use this theorem to establish quantifier elimination, or some combination of the above? $\endgroup$ Commented Mar 3, 2014 at 1:17
  • 1
    $\begingroup$ To be honest I don't really understand the meaning of quantifier elimination. Why is it important that everything about a theory can be expressed without quantifiers? Nor do I understand how finding elimination sets of a class of models gives us a method for finding a theory for the class of models. $\endgroup$
    – EarlyGame
    Commented Mar 3, 2014 at 1:53

2 Answers 2


The intuition is that, in a model with quantifier elimination, the definable sets are likely to be extremely simple.

The easiest example is the theory of dense linear orderings without endpoints. A set definable by a quantifier-free formula will consist of a finite union of individual points and intervals, by inspection of the formula. Because each model $M$ has quantifier elimination (in a signature with a constant for each element), every definable set will be of that simple form. If we do not add constants for elements, the quantifier-free formulas are all equivalent to $\top$ or to $\bot$, and so there are only two definable sets, $|M|$ and $\emptyset$. This also shows - syntactically - that the theory of dense linear orderings without endpoints is complete.

Quantifier elimination is also helpful for proving that theories are decidable. If the quantifier elimination procedure is effective - meaning there is a computable function mapping arbitrary formulas to quantifier-free equivalent formulas - this often gives a proof that the theory is decidable. This is because the function would have to map arbitrary sentences to equivalent quantifier-free sentences, and in many cases the truth of quantifier-free sentences can be decided algorithmically. This is one way to prove the decidability of the theory of the real numbers as an ordered field, for example: there is effective quantifier elimination, and truth of quantifier-free sentences can be decided algorithmically.

  • $\begingroup$ About the first paragraph: it may be worth noting that this is only true if the language is extremely simple. We can just take any theory and extend it to add Skolem functions, yielding a theory with quantifier elimination but possibly rather complicated definable sets. $\endgroup$
    – tomasz
    Commented Mar 3, 2014 at 14:12
  • $\begingroup$ Yes, the "likely to be" is a real caveat. But, for natural theories in their natural signature, a useful intuition is that quantifier elimination is a sign that the definable sets are probably not too complicated. That's what I was hoping to convey. $\endgroup$ Commented Mar 3, 2014 at 14:17
  • 1
    $\begingroup$ Well, that's more or less correct. It might also be worth noting, though, that exploring the properties of these "extremely simple" sets are, in some cases, the main focus of large branches of mathematics, like algebraic geometry. ;) That is to say that, while it is easy to check that a given point is in such a set, we can't assume that we know everything about them. $\endgroup$
    – tomasz
    Commented Mar 3, 2014 at 14:28

Suppose we have a class $K$ of models. That we have quantifier elimination for $K$ means that for every formula $\varphi(x)$ there is a quantifier-free formula $\psi(x,y)$ such that for every $M\in K$ we have $M\models \varphi(x)\leftrightarrow \psi(x,y)$ (where $x,y$ are tuples of finite length).

It does not, however, mean that the theory itself can be expressed without quantifiers, even if we assume that $K$ is an elementary class. This is not the case for the commonly known complete theories with quantifier elimination, such as $DLO_0$ (dense linear orderings without endpoints), $ACF_p$ (algebraically closed fields of characteristic $p$) or $RCF$ (real closed fields with $\leq$). A theory which has q.e. and is axiomatisable without quantifiers will likely be rather dull, though I don't feel like exploring how dull exactly it would be.

The process in the theorem is as follows:

  1. We have a set of formulas $\Phi$ we want to show is an elimination set. This means that any first-order formula in $L$ is equivalent to a boolean combination of elements of $\Phi$.
  2. Every first order formula comes from atomic formulas in a finite sequence of alternating two operations: taking a boolean combination and prefixing an existential quantifier. We can do induction with respect to complexity of formulas defined as the length of this finite sequence.
  3. So, if $\Phi$ contains an atomic formula (base case of induction), and every boolean combination of formulas in $\Phi$ prefixed by an existential quantifier is equivalent to a boolean combination of formulas without said quantifier then by induction we have...?

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .