Quantifier elimination

In model theory, quantifier elimination denotes a certain property of theories: It is said that a theory has quantifier elimination if every formula within the theory is equivalent to a formula without quantifiers . For example, in a field (e.g. in real numbers ) the formula that says that has a multiplicative inverse element is equivalent to , that is, that . There are no more quantifiers in. If every formula can be transformed into such a quantifier-free formula, then the theory possesses quantifier elimination. In theories with quantifier elimination, any formulas can be transformed into quantifier-free and thus simpler formulas. ${\displaystyle \varphi (x)=\exists y(x\cdot y\doteq 1)}$ ${\displaystyle x}$ ${\displaystyle \rho (x)=\neg (x\doteq 0)}$ ${\displaystyle x\neq 0}$ ${\displaystyle \rho (x)}$

definition

Be a language and a theory (i.e. a set of statements ). Then has quantifier elimination if for all formulas a quantifier- free formula exists with . ${\displaystyle L}$ ${\displaystyle T}$ ${\displaystyle T}$ ${\displaystyle L}$ ${\displaystyle \varphi (x_{1},\ldots ,x_{n})}$ ${\displaystyle L}$ ${\displaystyle \rho (x_{1},\ldots ,x_{n})}$ ${\displaystyle T\vdash \forall x_{1}\ldots \forall x_{n}(\varphi (x_{1},\ldots ,x_{n})\leftrightarrow \rho (x_{1},\ldots ,x_{n}))}$

Simple criterion

In order to check whether a theory has quantifier elimination, it is sufficient to prove this only for a simple type of formula: The universal quantifier can be converted into an existential quantifier with the help of a double negation. This can be removed inductively from the inside to the outside, so that it only has to be proven for formulas of the form with quantifier-free that they are equivalent to a quantifier-free formula. ${\displaystyle \exists x(\rho (x,y_{1},\ldots ,y_{n}))}$ ${\displaystyle \rho (x,y_{1},\ldots ,y_{n})}$

If one brings into disjunctive normal form and pulls the existential quantifier past the disjunction inwards, one sees that one can restrict oneself to such formulas that consist of a conjunction of elementary formulas or negations of such formulas. Formulas of the form in which this shape has are also called primitive existence formulas . ${\displaystyle \rho (x,y_{1},\ldots ,y_{n})}$ ${\displaystyle \rho (x,y_{1},\ldots ,y_{n})}$ ${\displaystyle \exists x(\rho (x,y_{1},\ldots ,y_{n}))}$ ${\displaystyle \rho }$

Examples

Infinite quantities

The theory of infinite sets can be formulated in a language without constant, function and relation symbols: The formula says that there are at least elements. therefore axiomatizes infinite sets. A primitive existence formula has the form where is quantifier-free and has any free variables. If , then the formula is equivalent to. Because the formula says that one is sought that agrees with all , so that only one option remains for. If, on the other hand , the formula is equivalent to , since something different from all is sought, which according to the axioms of the theory of infinite sets always exists. Thus every primitive existential formula is equivalent to a quantifier-free formula; the theory possesses quantifier elimination. ${\displaystyle \varphi _{n}=\exists x_{1},\ldots ,x_{n}\bigwedge _{1\leq i<j\leq n}\neg x_{i}\doteq x_{j}}$ ${\displaystyle n}$ ${\displaystyle T_{\infty }=\{\varphi _{n}|n\in \mathbb {N} \}}$ ${\displaystyle \exists x(\bigwedge _{i\in I}x\doteq y_{i}\wedge \bigwedge _{j\in J}\neg x\doteq z_{j}\wedge \rho )}$ ${\displaystyle \rho }$ ${\displaystyle I\neq \emptyset }$ ${\displaystyle \bigwedge _{i,j\in I}y_{i}\doteq y_{j}\wedge i_{0}\in I\wedge \bigwedge _{j\in J}\neg y_{i_{0}}\doteq z_{j}\wedge \rho }$ ${\displaystyle x}$ ${\displaystyle y_{i}}$ ${\displaystyle x}$ ${\displaystyle I=\emptyset }$ ${\displaystyle \rho }$ ${\displaystyle z_{j}}$ ${\displaystyle x}$

Further examples

Many other theories have quantifier elimination, including the following:

• the theory of algebraically closed bodies
• the theory of dense linear orders with no endpoints
• for a solid body , the theory of infinite - vector spaces ${\displaystyle K}$ ${\displaystyle K}$
• the theory of real closed bodies

Applications

completeness

A consistent theory without constants that has quantifier elimination is automatically complete , that is, it either proves itself or for every statement . This can be seen as follows: in theory, every statement is equivalent to a quantifier-free statement. But since there are no constants, the only quantifier-free statements are the true ( ) and the false ( ) statement. The theory thus proves either or . An example of this case is the theory of infinite sets above. ${\displaystyle \varphi }$ ${\displaystyle \varphi }$ ${\displaystyle \neg \varphi }$ ${\displaystyle \varphi }$ ${\displaystyle \top }$ ${\displaystyle \bot }$ ${\displaystyle \varphi }$ ${\displaystyle \neg \varphi }$

In general, the following applies: A theory with quantifier elimination is model-complete : If there are two models of , then an elementary extension is that the theories and of and agree. Because of the quantifier elimination, this only has to be proven for quantifier-free formulas, but such are only valid in when they are valid in, since the substructure of is. ${\displaystyle {\mathcal {A}}\subset {\mathcal {B}}}$ ${\displaystyle T}$ ${\displaystyle {\mathcal {A}}\prec {\mathcal {B}}}$ ${\displaystyle Th({\mathcal {A}})}$ ${\displaystyle Th({\mathcal {B}})}$ ${\displaystyle {\mathcal {A}}}$ ${\displaystyle {\mathcal {B}}}$ ${\displaystyle {\mathcal {A}}}$ ${\displaystyle {\mathcal {B}}}$ ${\displaystyle {\mathcal {A}}}$ ${\displaystyle {\mathcal {B}}}$

Algebraic Geometry

Algebraic geometry deals with algebraic varieties , the sets of zeros of polynomials. From Chevalley comes the theorem that the projection of such a variety onto a subspace can again be described by polynomials if the basic field is algebraically closed. This can be proven by using the quantifier elimination of the theory of algebraically closed fields: Let the variety be defined as the set of roots of the polynomials for . The projection onto the first coordinates is then given by . This formula is equivalent to a quantifier-free formula, which is a Boolean combination of elementary formulas of the type “Polynomials = 0”, so the projection is a Boolean combination of varieties. ${\displaystyle f_{i}(x_{1},\ldots ,x_{n})}$ ${\displaystyle i=1,\ldots m}$ ${\displaystyle k}$ ${\displaystyle \varphi (x_{1},\ldots ,x_{k})=\exists x_{k+1},\ldots ,x_{n}(f_{1}(x_{1},\ldots ,x_{n})\doteq 0\wedge \ldots \wedge f_{m}(x_{1},\ldots ,x_{n})\doteq 0)}$

Other uses

Even the Hilbert Nullstellensatz has based a proof that on the quantifier theory algebraically closed field. A proof exists for Hilbert's seventeenth problem , which is based on the quantifier elimination of the theory of real closed fields.

literature

• Wilfrid Hodges : Model theory . Cambridge University Press, 1993, ISBN 0-521-30442-3 .

Web links

• Eric W. Weisstein : Quantifier Elimination . In: MathWorld (English).

Individual evidence

1. ↑ ^{a b} Martin Ziegler: Script Model Theory 1 . (PDF; 649 kB) p. 43 ff.