nLab elimination of quantifiers

Redirected from "quantifier elimination".
Contents

Contents

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 AA be a linear transformation 𝔽 n+1𝔽 m\mathbb{F}^{n+1} \to \mathbb{F}^m. Let b\vec{b} be an mm-tuple, xx a variable, and y\vec{y} an nn-tuple of variables. Then the solution set for

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

is the projection of the solution set for

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

to the y\vec{y}-hyperplane. Since the projection of a (translated) hyperplane is again a (translated) hyperplane, there exists some B:𝔽 n𝔽 mB : \mathbb{F}^n \to \mathbb{F}^m such that B(y)=b(x)(A(x,y)=b).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 TT eliminates quantifiers if every \mathcal{L}-formula φ(x)\varphi(x) is equivalent to a quantifier-free \mathcal{L}-formula ψ(x)\psi(x), i.e.

Tφ(x)ψ(x). 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 TT eliminates quantifiers if and only if it is substructure-complete: TT plus the quantifier-free diagram of any substructure of any model of TT form a complete theory.

Theorem

Let TT be a theory. The following are equivalent:

  1. TT eliminates quantifiers.

  2. For every MM and NN models of TT such that NN is |M| +|M|^+-saturated and every proper substructure AMA \subseteq M such that there is an embedding i:ANi \colon A \to N, there exists a proper intermediate substructure AA', AAMA \subsetneq A' \subseteq M and an extension i:ANi' \colon A' \to N of ii to AA'.

Proof

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

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

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

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

Embed MM into a sufficiently saturated elementary extension *M^*M (by taking a large enough ultrapower, if you like). Then by (2.), the elementary embedding M *MM \preceq ^*M extends along the embedding MNM \hookrightarrow N to an embedding N *MN \hookrightarrow ^*M. If Nxφ(x,m)N \models \exists x \varphi(x,m), then there is a witness nNn \in N such that Nφ(n,m)N \models \varphi(n,m). Since φ\varphi was quantifier-free, this transfers along the embedding N *MN \hookrightarrow ^*M, so that *Mφ(n,m)^*M \models \varphi(n,m), and therefore *Mxφ(x,m).^*M \models \exists x \varphi(x,m). This then transfers down the elementary embedding M *MM \preceq ^*M, so Mxφ(x,m).M \models \exists x \varphi(x,m). Since MM and NN were arbitrary, TT 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 ACF p\mathsf{ACF}_p (where pp is specification of the characteristic) are complete.

Proof

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

That ACF\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 pp contains the prime field of characteristic pp.

QE extends to co-slice categories

Let TT eliminate quantifiers. Let KK be a substructure (not necessarily a submodel) of some model AA of TT. Then the theory T/KT/K of models of TT interpreting a copy of KK 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 RR (i.e. the geometric points of Spec(R)\operatorname{Spec}(R)), in the language of rings with constants for the elements of RR.

References

category: logic, model theory

Last revised on August 3, 2017 at 22:57:00. See the history of this page for a list of all contributions to it.