You may ask why I name this chapter with such a title in quiet simplicity. That’s because I HATE this chapter in A Course in Model Theory. Therefore, here is my version of this chapter, which I deleted a lot from and added some into. I hope you like it.

Quantifier Elimination

A method of model theory in the early stage is called quantifier elimination. One can easily understand it by the name that we can find a substitution of one formula with a quantifier free formula. More formally, given a theory $T$, we say $T$ has quantifier elimination if and only if, for every formula $varphi$, there is a quantifier free formula $\psi$ with $T\vdash \varphi\leftrightarrow\psi$, which reads $\varphi$ is equivalent to $\psi$ modulo T. For sake of convenience, in such condition, we say the quantifier of $\varphi$ can be eliminated.

There is a simple characterization of it. We introduce a concept first.

A formula in the prenex normal form is called simple existential if it is in the form

$\exists x_1\cdots\exists x_n\varphi(x_1,\cdots,x_n,y_1,\cdots,y_n),$

and it is called primitive if $\varphi$ is a conjunction of basic formulas.

A remark needs to be given here that a simple existential formula is not an existential formula, which is defined as a formula in negation normal form having no universal quantifiers. An example is $(\exists xP(x))\vee(\exists xQ(x))$, where $P,Q$ are predicates.

A theory $T$ has quantifier elimination if and only if the quantifier of every primitive existential formula $\varphi$ can be eliminated. One can easily prove this by replacing primitive existential formulas with quantifier-free formulas in some order.

Here we give another characterization. For convenience, in this article, we define (Prop.QE) as the proposition that a given theory $T$ has quantifier elimination, and we write (Prop.A) as following with corresponding theory $T$.

(Prop.A): Given models $\mathfrak{M,N}$ of $T$, with common substructure $\mathfrak{A}$, for all primitive existential formulas $\varphi(x_1,\cdots,x_n)$ and parameters $a_1,\cdots,a_n\in A$, we have

$\mathfrak{M}\models\varphi(a_1,\cdots,a_n)\Leftrightarrow\mathfrak{N}\models\varphi(a_1,\cdots,a_n).$

The characterization of quantifier elimination is (Prop.QE) if and only if (Prop.A). This is not that easy to prove, and the direct proof is rather complicated (or maybe just I don’t like it.) I have found a better way to prove it (I hope there is nothing wrong!), and here it is.

Types, Topology, and Proof

To make the proof more understandable, we introduce some new concepts at first.

Types!

Given a structure $\mathfrak{A}$ and $a_1,\cdots,a_n\in A$, we call the set

$\mathrm{tp}_\mathfrak{A}(a_1,\cdots,a_n)=\{\varphi(x_1,\cdots,x_n);\mathfrak{A}\models\varphi(a_1,\cdots,a_n)\}$

an $n$-type. We should give two remarks,

1. an $n$-type is the set of $n$-ary formulas which is maximal finitely satisfiable.
2. there are also formulas with less variables in an $n$-type.

Given a satisfiable theory $T$, the set of all types that contain (one understand this by remark 2) $T$ is denoted by $S_n(T)$, which is exactly the $n$-types in $L$ that consistent with $T$.

The nontriviality of $S_n(T)$ is that it can be equipped with a topology. For a given formula $\varphi$, we define $[\varphi]$ to be the set of all $n$-types containing $\varphi$. One can easily check that $\mathcal{O}=\{[\varphi];\varphi\text{ is a formula}\}$ gives the basic open sets on $S_n(T)$.

Now, we can rewrite the (Prop.A) with the language of types as follows.

(Prop.A’): $\mathfrak{M,N}$ are models of theory $T$, with common substructure $\mathfrak{A}$. For $a_1,\cdots,a_n\in A$, then the primitive existential formulas in $\mathrm{tp}_\mathfrak{M}(a_1,\cdots,a_n),\mathrm{tp}_\mathfrak{N}(a_1,\cdots,a_n)$ are the same.

Topology!

To be totally irresponsible, it’s easy to prove that such a topological space is totally disconnected, Hausdorff, and compact (this is why compactness was discussed in the last chapter).

One should also realize that the closed sets are in the form of

$\{\Sigma\in S_n(T);\Sigma\supset\Sigma'\}$

where $\Sigma'$ is a given set of formulas. The clopen sets are exactly $[\varphi]$.

Let’s prove a lemma. For an $L$-formula $\varphi(a_1,\cdots,a_n)$ and a set $\Sigma$ of formulas which is closed under disjunction and conjunction, the following are equivalent:

1. $T\models\varphi$ or $T\models\neg\varphi$ or $T\models\varphi\leftrightarrow\sigma$ for some formula $\sigma\in\Sigma$.
2. For every $p_1,p_2\in S_n(T)$, if $\varphi\in p_1$ and $\neg\varphi\in p_2$, then there exists $\sigma\in\Sigma$ such that $\sigma\in p_1$ and $\neg\sigma\in p_2$.

We only prove (2 $\Rightarrow$ 1). If 2 holds and neither $T\models\varphi$ nor $T\models\neg\varphi$, we have to prove $T\models\varphi\leftrightarrow\sigma$ for some formula $\sigma\in\Sigma$. This is equivalent to find a $\sigma$ such that $[\sigma]=[\varphi]$.

For any type $p\in[\varphi]$, by condition 2, there is a subset $\Sigma'$ of $\Sigma$ such that $[\varphi]^c\subset\bigcup\{\neg[\sigma'];\sigma'\in\Sigma'\}$. Since the space is compact, there is a finite subcover. By taking disjunction, we have a $\sigma'\in\Sigma$ such that $p\in[\sigma']\subset[\varphi]$. By such process, we find an open cover of $[\varphi]$ generated from $\Sigma$. Again, by compactness and disjunction, we find some $\sigma\in\Sigma$ that we desire. Here, the operation of disjunction is guaranteed by the closure of $\Sigma$, so the reader need not worry about the validity.

By this lemma, one can easily prove the following theorem.

(Prop.QE) if and only if (Prop.B): for each $n\ge 1$, every type in $S_n(T)$ is determined by the quantifier free formula it contains.

Proof!

Now, we can prove the theorem we want. To prove that (Prop.QE) if and only if (Prop.A), we only have to prove that (Prop.A’) is equivalent to (Prop.B).

We prove (Prop.B)$\Rightarrow$(Prop.A’) first. By the definition of substructure, for any quantifier-free formula $\varphi(x_1,\cdots,x_n)$,

$\mathfrak{M}\models\varphi(a_1,\cdots,a_n)\Leftrightarrow\mathfrak{A}\models\varphi(a_1,\cdots,a_n)\Leftrightarrow\mathfrak{N}\models\varphi(a_1,\cdots,a_n),$

where $a_1,\cdots,a_n\in A$. With (Prop.B), $\mathrm{tp}_\mathfrak{M}(a_1,\cdots,a_n)=\mathrm{tp}_\mathfrak{N}(a_1,\cdots,a_n)$, then (Prop.A’) holds vacuously.

Conversely, suppose that (Prop.A’) holds. For two given types $\mathrm{tp}_\mathfrak{M}(a_1,\cdots,a_n)$ and $\mathrm{tp}_\mathfrak{N}(b_1,\cdots,b_n)$ which share the same quantifier-free formulas. Denote $A=\{a_1,\cdots,a_n\},B=\{b_1,\cdots,b_n\}$, then $\langle A\rangle$ is isomorphic to $\langle B \rangle$. It’s clear (one can refer to Lemma 1.1.8 in Tent–Ziegler, A Course in Model Theory) that there is an extension $\mathfrak{M}'$ of $\langle A \rangle$ which is isomorphic to $\mathfrak{N}$. Now, we can assume that $\mathfrak{M}$ and $\mathfrak{N}$ have a common substructure $\mathfrak{A}$ with $a_1,\cdots,a_n\in\mathfrak{A}$ without loss of generality.

We write every simple existential formula in the form $\exists x_1\cdots\exists x_n\bigvee_{i<n}\rho_i$, where $\rho_i$ are conjunctions of basic formulas. Then every simple existential formula is equivalent to a disjunction of primitive existential formulas. Therefore, we can assume $\mathrm{tp}_\mathfrak{M}(a_1,\cdots,a_n)$ and $\mathrm{tp}_\mathfrak{N}(a_1,\cdots,a_n)$ share the same simple existential formula by (Prop.A’).

Now, consider an arbitrary formula. We first rewrite it into prenex normal form, which is $Q_nx_n\cdots Q_1x_1\rho$. If $Q_1$ is $\exists$, then $Q_1x_1\rho$ is either in or not in both $\mathrm{tp}_\mathfrak{M}(a_1,\cdots,a_n)$ and $\mathrm{tp}_\mathfrak{N}(a_1,\cdots,a_n)$. If $Q_1$ is $\forall$, then we rewrite it as $\neg\exists x_1\neg\rho$, which is still either in or not in both $\mathrm{tp}_\mathfrak{M}(a_1,\cdots,a_n)$ and $\mathrm{tp}_\mathfrak{N}(a_1,\cdots,a_n)$. Keeping such a process, we can prove this formula is in both $\mathrm{tp}_\mathfrak{M}(a_1,\cdots,a_n)$ and $\mathrm{tp}_\mathfrak{N}(a_1,\cdots,a_n)$. Hence (Prop.B) holds.

Snacks

Some results should also be given here, which are useful, important, but irrelevant to the main thread of this article.

Another criterion

We have already proved the equivalence of (Prop.QE) and (Prop.A), but there is actually a intermediate proposition there.

(Prop.L): Given two models $\mathfrak{M},\mathfrak{N}$ of $L$ with a common substructure $\mathfrak{A}$, we have $\mathfrak{M}_A\equiv\mathfrak{N}_A$.

Given a sentence $\varphi$ in $L(A)$, we can rewrite it as a formula $\psi(a_1,\cdots,a_n)$ in $L$. And by (Prop.QE), there is a quantifier free formula $\rho(a_1,\cdots,a_n)$ which has the same truth value in models of $L$. Then we have

$$\begin{align*} \mathfrak{M}_A\models\varphi&\Leftrightarrow\mathfrak{M}\models\psi(a_1,\cdots,a_n)\\ &\Leftrightarrow\mathfrak{M}\models\rho(a_1,\cdots,a_n)\\ &\Leftrightarrow \mathfrak{A}\models\rho(a_1,\cdots,a_n)\\ &\Leftrightarrow \mathfrak{N}\models\rho(a_1,\cdots,a_n)\\ &\Leftrightarrow\mathfrak{N}\models\psi(a_1,\cdots,a_n)\Leftrightarrow\mathfrak{N}_A\models\varphi. \end{align*}$$

This shows (Prop.QE)$\Rightarrow$(Prop.L). And (Prop.L)$\Rightarrow$(Prop.A) is obvious. This provides another criterion for quantifier elimination, which is also quite useful.

Prime Structure

A prime structure of $T$ is a structure that can be embedded into all models of $T$. A consistent theory with a prime structure and quantifier elimination is complete.

Suppose the converse. Without loss of generality, we can let $\varphi$ be a sentence and $\mathfrak{M}\models\varphi,\mathfrak{N}\models\neg\varphi$ be two models of $T$ that do not agree on $\varphi$. Then, we can find a quantifier-free formula $\rho$ with no free variables which is equivalent to $\varphi$ modulo $T$. However, $\rho$ must be the same in $\mathfrak{M}$ and $\mathfrak{N}$ since they share the same interpretation of constants, which leads to a contradiction.

Examples

The detailed mathematical structures are important in the early stage of Model Theory. We introduce the theories here and investigate their properties.

Infinite sets

The language here is empty, and infinite sets are axiomatized by sentences

$\exists x_1\cdots\exists x_n\bigwedge_{i<j<n}\neg x_i=x_j,$

for any positive integer $n$.

It’s clear that this theory has quantifier elimination, since the only predicate is ”=“. The empty set is the prime structure of this theory; therefore, it is complete.

Dense Linear Orderings

This theory is called dense linear orderings without endpoints, and abbreviates as $\mathsf{DLO}$. The language only needs a symbol $<$, and the axioms are the following,

1. (Irreflexive) $\forall x(\neg x=x)$,
2. (Transitive) $\forall x\forall y\forall z(x<y\wedge y<z\rightarrow x<z)$,
3. (Trichotomy) $\forall x\forall y(x<y\vee y<x\vee x=y)$,
4. (No endpoints) $\forall x\exists y(x<y)$,
5. (No endpoints) $\forall x\exists y(y<x)$,
6. (Density) $\forall x\forall z\exists y(x<z\rightarrow (x<y\wedge y<z))$.

Now, we prove that this theory has quantifier elimination. Suppose $\mathfrak{M}$ and $\mathfrak{N}$ are two models with a common substructure $\mathfrak{A}$. You will see that the formula $\varphi(a_1,\cdots,a_n)$, where $\varphi(x_1,\cdots,x_n)$ is a primitive existential formula and $a_1,\cdots,a_n\in A$, only cares about the relationships between elements in $A$ and “whether there is something in front of, in the middle of, or after some two elements of $A$“. The truth value of these things—I hope my reader can agree with this without further explanation—is independent of the choice of either $\mathfrak{M}$ or $\mathfrak{N}$. This is exactly (Prop.A).

The reader might note that there are no constants, and this is a proof of the completeness.

Algebraically Closed Field

The language we need here is $L_{\text{ring}}={0,1,+,-,\cdot}$, and the axioms are:

1. $\forall x\forall y\forall z((x+y)+z=x+(y+z))$,
2. $\forall x\forall y(x+y=y+x)$,
3. $\forall x(x+0=x)$,
4. $\forall x(x+(-x)=0)$,
5. $\forall x\forall y\forall z((x\cdot y)\cdot z=x\cdot(y\cdot z))$,
6. $\forall x\forall y(x\cdot y=y\cdot x)$,
7. $\forall x(x\cdot1=x)$,
8. $\forall x (\neg(x=0)\rightarrow \exists y(x\cdot y =1))$,
9. $\forall x\forall y\forall z(x\cdot(y+z)=(x\cdot y+x\cdot z))$,
10. $\neg(0=1)$,
11. for every positive integer $n$, $\forall x_0\cdots\forall x_{n-1}\exists x(x^{n}+x_{n-1}x^{n-1}+\cdots+x_1x+x_0=0)$ (any reader can easily understand this abbreviation).

And now, I’m too lazy to prove the quantifier elimination of it, sorry.