nLab elimination of quantifiers

Idea

One thinks of existential quantification as projection. A theory eliminates quantifiers when “the projection of a primitive (quantifier-free) definable set is still primitive (quantifier-free).”

For example, suppose we’re working in the theory of a vector space over a fixed field $\mathbb{F}$. Let $A$ be a linear transformation $\mathbb{F}^{n+1} \to \mathbb{F}^m$. Let $\vec{b}$ be an $m$-tuple, $x$ a variable, and $\vec{y}$ an $n$-tuple of variables. Then the solution set for

$$\exists x A(x, \vec{y}) = \vec{b}$$

is the projection of the solution set for

$$A(x, \vec{y}) = \vec{b}$$

to the $\vec{y}$-hyperplane. Since the projection of a (translated) hyperplane is again a (translated) hyperplane, there exists some $B : \mathbb{F}^n \to \mathbb{F}^m$ such that $B(\vec{y}) = \vec{b} \iff (\exists x) \left(A(x, \vec{y}) = \vec{b}\right).$

This is an instance of the fact that the theories of vector spaces over division rings admits quantifier elimination. It’s nice when this happens, and when it doesn’t, one asks for minimal ways to expand the language to make it happen. That ACF eliminates quantifiers is a special case of Chevalley's theorem on constructible sets (“the image of a constructible set is constructible”).

Often, in order to prove quantifier-elimination, one develops an effective procedure for reducing an arbitrary sentence to a quantifier-free one, which shows that the theory is decidable; this is how Tarski proved that the theory RCF? of real closed fields is decidable.

Definition

An $\mathcal{L}$-theory $T$ eliminates quantifiers if every $\mathcal{L}$-formula $\varphi(x)$ is equivalent to a quantifier-free $\mathcal{L}$-formula $\psi(x)$, i.e.

$$T \models \varphi(x) \leftrightarrow \psi(x).$$

Remarks

• Any theory is bi-interpretable with an expanded theory where every definable set is named with a predicate, called its Morleyization, which eliminates quantifiers.

• Therefore, whether or not a structure has quantifier elimination depends on the language being used to describe the structure.

• Quantifier elimination implies model completeness: all submodels are elementary submodels and all models are existentially closed.

• It is an informative exercise to try to prove QE syntactically (a “tractable” case like DLO suffices) to appreciate the usefulness of the semantic/model-theoretic characterization of QE below.

• The characterizations below (and in general important tools in model theory like the compactness theorem, the Lowenheim-Skolem theorem, etc.) only work for infinite models.

• Since quantifier elimination is equivalent to substructure completeness and elementarily equivalent finite structures are isomorphic, (the theory of a) finite first-order structure eliminates quantifiers if and only if it is ultrahomogeneous.

Semantic characterizations of QE

Proposition

A first-order theory $T$ eliminates quantifiers if and only if it is substructure-complete: $T$ plus the quantifier-free diagram of any substructure of any model of $T$ form a complete theory.

Proof

See substructure completeness.

Theorem

Let $T$ be a theory. The following are equivalent:

1. $T$ eliminates quantifiers.

2. For every $M$ and $N$ models of $T$ such that $N$ is $|M|^+$-saturated and every proper substructure $A \subseteq M$ such that there is an embedding $i \colon A \to N$, there exists a proper intermediate substructure $A'$, $A \subsetneq A' \subseteq M$ and an extension $i' \colon A' \to N$ of $i$ to $A'$.

Proof

(1. $\implies$ 2.) Suppose $T$ eliminates quantifiers. Since this is equivalent to substructure-completeness, choose $x \in M \backslash A$, and let $B \overset{df}{=} \langle A \cup \{x\} \rangle$ be the substructure of $M$ generated by $A \cup \{x\}.$ Then, since quantifier-free statements are transferred by embeddings, the type (in model theory) of $x$ over $A$ in $M$ is finitely realized in $N$ and therefore realized via $|M|^+$-saturation by some $x'$.

A standard back-and-forth argument starting at $x'$ lets us build our required extension.

(2. $\implies$ 1.) By possibly transfinitely iterating 2., we obtain an embedding $M \to N.$ As we can always embed a $T$-model inside a larger, arbitrarily saturated $T$-model, we therefore have amalgamation.

This gives model completeness: since model completeness is equivalent to every $T$-submodel being an elementary submodel, it suffices by the Tarski-Vaught test (and an induction on complexity of formulas) to test that whenever $m$ is a tuple from $M$, $\varphi(x,y)$ is a quantifier-free formula, and $N \models \exists x \varphi(x, m)$, then $M \models \exists x \varphi(x,m)$ (i.e. that $M$ is existentially closed.)

Embed $M$ into a sufficiently saturated elementary extension $^*M$ (by taking a large enough ultrapower, if you like). Then by (2.), the elementary embedding $M \preceq ^*M$ extends along the embedding $M \hookrightarrow N$ to an embedding $N \hookrightarrow ^*M$. If $N \models \exists x \varphi(x,m)$, then there is a witness $n \in N$ such that $N \models \varphi(n,m)$. Since $\varphi$ was quantifier-free, this transfers along the embedding $N \hookrightarrow ^*M$, so that $^*M \models \varphi(n,m)$, and therefore $^*M \models \exists x \varphi(x,m).$ This then transfers down the elementary embedding $M \preceq ^*M$, so $M \models \exists x \varphi(x,m).$ Since $M$ and $N$ were arbitrary, $T$ is model complete.

Since model completeness + amalgamation implies substructure completeness and substructure completeness is equivalent to quantifier elimination, the theorem is proved.

Corollary

ACF admits quantifier elimination. Furthermore, the theories $\mathsf{ACF}_p$ (where $p$ is specification of the characteristic) are complete.

Proof

We put ourselves into the situation of the above theorem. Let $E$ and $F$ be algebraically closed fields such that $F$ is $|E|^+$-saturated. Let $R$ be a subring of $E$ with $i : R \to F$ an embedding. As $E$ is a field, $R$ is an integral domain, and thus $E$ contains the fraction field $\operatorname{Frac}(R)$ of $R$. The embedding $i$ extends uniquely to $\operatorname{Frac}(R)$. By a back-and-forth argument, $i$ extends uniquely to $\operatorname{Frac}(R)^{\operatorname{alg}}$. Therefore, we can assume that $R$ is algebraically closed. Let $a \in E \backslash R$. Then $a$ is transcendental over $R$, and by saturation its type is realized by some $b \in F$ which is transcendental over the image $i(R)$ of $R$ under $i$. Then $a \mapsto b$ induces an embedding $R[a] \overset{i'}{\to} i(R)[b]$, which extends $i$. Thus the hypotheses of the theorem are satisfied and ACF admits QE.

That $\mathsf{ACF}$ becomes complete after specifying a characteristic follows from the fact that in any theory with quantifier elimination, naming a substructure (thus passing to the theory of all models which contain a copy of that substructure) makes the theory complete, and every field of characteristic $p$ contains the prime field of characteristic $p$.

QE extends to co-slice categories

Let $T$ eliminate quantifiers. Let $K$ be a substructure (not necessarily a submodel) of some model $A$ of $T$. Then the theory $T/K$ of models of $T$ interpreting a copy of $K$ also has quantifier elimination.

In particular, if we specialize to ACF, this tells us that not only do all algebraically closed fields admit quantifier elimination in the language of rings, but so do all algebraically closed fields containing a fixed ring $R$ (i.e. the geometric points of $\operatorname{Spec}(R)$), in the language of rings with constants for the elements of $R$.

Related concepts

• quantification

• quantifier-free diagram

• decidability

References

• wikipedia quantifier elimination
• Wilfrid Hodges, Model Theory, Cambridge University Press 1993

category: logic, model theory