Let $T_0$ be a consistent theory. Let ${\cal T}$ be the set of all complete theories that contain $T_0$.

Is it true that if each $T\in{\cal T}$ eliminates quantifiers so does $T_0$?

Note. The point is about uniformity. Assume for every formula $\varphi$ there is a quantifier-free formula $\psi_T$ such that $T\vdash \varphi\leftrightarrow\psi_T$. Is it possible to conclude that $\psi_T$ does not depend on $T$?

Edit. The case when $T_0$ has no finite models, is particularly interesting.


2 Answers 2


No, it is not. Every completion of the empty theory in the empty language has quantifier elimination, but the empty theory itself doesn't.

Why? Well, note that the only data missing from the empty theory is the size of the universe: a completion of the empty theory either is generated by some sentence of the form "there are exactly $n$ many elements," or is generated by the set of sentences "there are at least $n$ distinct elements" for all $n$. Either way, in any model of $T$ the type of a tuple is determined completely by the atomic theory of the tuple (= which coordinates are equal to which others, in this case) so every extension of $T$ has quantifier elimination, but $T$ itself doesn't prove or disprove the quantifier-free sentence $\eta=$"$\exists x\exists y(x\not=y)$", and sinec the only quantifier-free sentences in the empty language are (equivalent to one of) $\perp$ and $\top$, this means that the empty theory doesn't eliminate quantifiers from $\eta$.

Note, however, that by Konig's lemma for any such $T_0$ and any formula $\psi(\overline{x})$, there is a finite set of formulas $\{\theta_1, ..., \theta_n\}$ such that $T_0$ proves $$\bigvee_{1\le i\le n}\forall \overline{x}(\psi(\overline{x})\iff\theta_i(\overline{x})).$$ (This is a good exercise. HINT: consider the usual tree of consistent extensions of $T_0$, and look at the subtree of consistent extensions which do not yet eliminate quantifiers from $\psi$. If that subtree is finite we're done; otherwise, think about what a path through that subtree entails . . .)

EDIT: This can easily be tweaked to avoid finite models. Consider the language consisting of a single unary relation symbol $U$, and the theory $T_0$ consisting only of the axioms asserting that the universe is infinite. A completion of $T_0$ consists of data telling us the size of $U$ and of $\neg U$; it's easy to check that each of these satisfies quantifier elimination, but $T_0$ does not eliminate quantifiers from e.g. the sentence "$\forall x(U(x))$."

This might seem cheap, since a model of $T_0$ basically consists of two models of the theory above placed "side by side," at least one of which is infinite. However, we can produce plenty more examples.

The failure of quantifier elimination in $T_0$ is guaranteed when $T_0$ is complete for quantifier-free sentences but is not complete (since then $T_0$ can't eliminate quantifiers for any sentence it doesn't decide), and this trivially holds if $T_0$ is in a relational language (since then it has no nontrivial quantifier-free sentences); more vaguely, the fact that quantifier elimination holds in all completions of $T_0$ is guaranteed by completions of $T_0$ being generated (over $T_0$) by a "simple" decision, and models of the theory being "combinatorially simple." With this in mind, we can construct many more examples:

  • The theory of dense linear orders possibly with endpoints.

  • The theory of $\overline{\mathbb{Q}}$-vector spaces of unspecified dimension. (Here in order to make linear independence first-order definable, the vector space is construed as a two-sorted structure, with scalars and vectors; if we replaced $\overline{\mathbb{Q}}$ with a finite field, it wouldn't matter how we presented it.)

And so forth.

Another approach is to consider the disjunction of two complete theories which eliminate quantifiers. Given theories $T_1$ and $T_2$ in the same language, let $$T_{1\vee 2}=\{\varphi\vee\psi: \varphi\in T_1, \psi\in T_2\}.$$ Any model of $T_{1\vee 2}$ is either a model of $T_1$ or a model of $T_2$ (suppose not; let $\varphi$ and $\psi$ witness this, and think about $\varphi\vee\psi$ . . .), hence $T_{1\vee 2}$ has exactly two completions, each of which eliminate quantifiers, but in general $T_{1\vee 2}$ itself won't.

For example, work in the language with a single binary relation symbol $R$, let $T_1$ be the theory of the random graph, and $T_2$ be the theory of the dense linear order without endpoints. Then $T_{1\vee 2}$ doesn't decide, and hence (since its only quantifier-free sentences up to semantic equivalence are $\top$ and $\perp$) doesn't eliminate quantifiers from, the sentence "$\exists x, y, z(xRy\wedge yRz\wedge \neg xRz)$".

  • 2
    $\begingroup$ You would appeal to Konig's Lemma instead of the compactness theorem! $\endgroup$ May 28, 2017 at 17:42
  • $\begingroup$ +1 For the example. I forgot about the existence of finite models :( and I have edited my question. $\endgroup$
    – Escherica
    May 28, 2017 at 18:09
  • $\begingroup$ @Escherica Avoiding finite models doesn't help things, see my edit. $\endgroup$ May 28, 2017 at 18:49
  • $\begingroup$ @AlexKruckman Haha, wow, why did I do that? $\endgroup$ May 28, 2017 at 19:05
  • $\begingroup$ @NoahSchweber You give some great examples, but one isn't right. Transcendence degree is not first order (ACF_p is already complete with QE). $\endgroup$ May 28, 2017 at 19:20

This is an addendum to @NoahSchweber'a answer.

The answer is positive in some particular cases (e.g. for $T_0=$ACF and similar cases).

Suppose all completions of $T_0$ are of the form $T_0\cup S$ where $S$ is a set of quantifier-free sentences. Then, if all completion of $T_0$ have quantifier elimination, so does $T_0$.

By compactness (or Köning's lemma), there are finitely many quantifier-free sentences $\sigma_i$ and quantifier-free formulas $\psi_i(x)$ such that

$\displaystyle\qquad\sigma_i\vdash\varphi(x)\leftrightarrow\psi_i(x)$, $\qquad\displaystyle T_0\vdash\bigvee^n_{i=1}\sigma_i$, $\qquad\sigma_i\vdash\neg\sigma_j$ for $i\neq j$.

then $\displaystyle\quad T_0\vdash\varphi(x)\leftrightarrow\bigvee^n_{i=1}\sigma_i\wedge\psi_i(x)$.


You must log in to answer this question.

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