Namespaces
Variants
Actions

Difference between revisions of "Elimination of quantifiers"

From Encyclopedia of Mathematics
Jump to: navigation, search
(Importing text file)
 
(TeX)
Line 1: Line 1:
An [[Elementary theory|elementary theory]] <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e110/e110040/e1100401.png" /> is said to admit elimination of quantifiers if every formula in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e110/e110040/e1100402.png" /> is equivalent in the language of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e110/e110040/e1100403.png" /> to a formula without quantifiers (having the same free variables). This holds if and only if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e110/e110040/e1100404.png" /> is substructure complete, i.e., for every two models <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e110/e110040/e1100405.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e110/e110040/e1100406.png" /> of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e110/e110040/e1100407.png" /> with a common substructure <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e110/e110040/e1100408.png" />, the expansions <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e110/e110040/e1100409.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e110/e110040/e11004010.png" /> are elementarily equivalent in the first-order language of signature <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e110/e110040/e11004011.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e110/e110040/e11004012.png" /> denotes the signature of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e110/e110040/e11004013.png" /> (cf. [[Model theory|Model theory]]; [[Structure(2)|Structure]]). If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e110/e110040/e11004014.png" /> is substructure complete, then it is model complete. To see this, set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e110/e110040/e11004015.png" /> for every model <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e110/e110040/e11004016.png" /> of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e110/e110040/e11004017.png" /> which is a substructure of a model <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e110/e110040/e11004018.png" /> of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e110/e110040/e11004019.png" />.
+
{{TEX|done}}
 +
An [[Elementary theory|elementary theory]] $T$ is said to admit elimination of quantifiers if every formula in $T$ is equivalent in the language of $T$ to a formula without quantifiers (having the same free variables). This holds if and only if $T$ is substructure complete, i.e., for every two models $A$ and $B$ of $T$ with a common substructure $S$, the expansions $(A,|S|)$ and $(B,|S|)$ are elementarily equivalent in the first-order language of signature $\langle\Omega,|S|\rangle$, where $\Omega$ denotes the signature of $T$ (cf. [[Model theory|Model theory]]; [[Structure(2)|Structure]]). If $T$ is substructure complete, then it is model complete. To see this, set $S=A$ for every model $A$ of $T$ which is a substructure of a model $B$ of $T$.
  
For certain elementary theories of fields, the fact that they admit elimination of quantifiers reflects an algebraic [[Elimination theory|elimination theory]]. Examples are the theory of algebraically closed fields (where vanishing of the [[Resultant|resultant]], <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e110/e110040/e11004020.png" />, gives a quantifier-free criterion for the existence of a common zero of two polynomials <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e110/e110040/e11004021.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e110/e110040/e11004022.png" />), and the theory of real closed fields (where the [[Sturm theorem|Sturm theorem]] gives a quantifier-free criterion for a polynomial to admit a root in a given interval, cf. also [[Real closed field|Real closed field]]).
+
For certain elementary theories of fields, the fact that they admit elimination of quantifiers reflects an algebraic [[Elimination theory|elimination theory]]. Examples are the theory of algebraically closed fields (where vanishing of the [[Resultant|resultant]], $R(f,g)=0$, gives a quantifier-free criterion for the existence of a common zero of two polynomials $f$, $g$), and the theory of real closed fields (where the [[Sturm theorem|Sturm theorem]] gives a quantifier-free criterion for a polynomial to admit a root in a given interval, cf. also [[Real closed field|Real closed field]]).
  
The fact that the theory of real closed fields admits elimination of quantifiers is commonly known as the Tarski–Seidenberg theorem (see also [[Semi-algebraic set|Semi-algebraic set]]). It implies that the semi-algebraic sets over a real closed field <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e110/e110040/e11004023.png" /> are precisely the definable sets (with parameters from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e110/e110040/e11004024.png" />) in the first-order language of ordered fields. For the history and applications of the Tarski–Seidenberg theorem, and a remarkable discussion of the general technique of elimination of quantifiers, see [[#References|[a2]]] and the literature cited therein. For applications of elimination of quantifiers to real and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e110/e110040/e11004025.png" />-adic semi- and subanalytic sets, see [[#References|[a1]]].
+
The fact that the theory of real closed fields admits elimination of quantifiers is commonly known as the Tarski–Seidenberg theorem (see also [[Semi-algebraic set|Semi-algebraic set]]). It implies that the semi-algebraic sets over a real closed field $K$ are precisely the definable sets (with parameters from $K$) in the first-order language of ordered fields. For the history and applications of the Tarski–Seidenberg theorem, and a remarkable discussion of the general technique of elimination of quantifiers, see [[#References|[a2]]] and the literature cited therein. For applications of elimination of quantifiers to real and $p$-adic semi- and subanalytic sets, see [[#References|[a1]]].
  
 
For certain elementary theories of algebraic systems, elimination of quantifiers implies closure properties of their models (cf. [[#References|[a3]]]).
 
For certain elementary theories of algebraic systems, elimination of quantifiers implies closure properties of their models (cf. [[#References|[a3]]]).
  
 
====References====
 
====References====
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  J. Denef,  L. van den Dries,  "<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e110/e110040/e11004026.png" />-adic and real subanalytic sets"  ''Ann. of Math.'' , '''128'''  (1988)  pp. 79–138</TD></TR><TR><TD valign="top">[a2]</TD> <TD valign="top">  L. van den Dries,  "Alfred Tarski's elimination theory for real closed fields"  ''J. Symb. Logic'' , '''53'''  (1988)  pp. 7–19</TD></TR><TR><TD valign="top">[a3]</TD> <TD valign="top">  L. van den Dries,  A. Macintyre,  K. McKenna,  "Elimination of quantifiers in algebraic structures"  ''Adv. in Math.'' , '''47'''  (1983)  pp. 74–87</TD></TR></table>
+
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  J. Denef,  L. van den Dries,  "$p$-adic and real subanalytic sets"  ''Ann. of Math.'' , '''128'''  (1988)  pp. 79–138</TD></TR><TR><TD valign="top">[a2]</TD> <TD valign="top">  L. van den Dries,  "Alfred Tarski's elimination theory for real closed fields"  ''J. Symb. Logic'' , '''53'''  (1988)  pp. 7–19</TD></TR><TR><TD valign="top">[a3]</TD> <TD valign="top">  L. van den Dries,  A. Macintyre,  K. McKenna,  "Elimination of quantifiers in algebraic structures"  ''Adv. in Math.'' , '''47'''  (1983)  pp. 74–87</TD></TR></table>

Revision as of 19:24, 7 July 2014

An elementary theory $T$ is said to admit elimination of quantifiers if every formula in $T$ is equivalent in the language of $T$ to a formula without quantifiers (having the same free variables). This holds if and only if $T$ is substructure complete, i.e., for every two models $A$ and $B$ of $T$ with a common substructure $S$, the expansions $(A,|S|)$ and $(B,|S|)$ are elementarily equivalent in the first-order language of signature $\langle\Omega,|S|\rangle$, where $\Omega$ denotes the signature of $T$ (cf. Model theory; Structure). If $T$ is substructure complete, then it is model complete. To see this, set $S=A$ for every model $A$ of $T$ which is a substructure of a model $B$ of $T$.

For certain elementary theories of fields, the fact that they admit elimination of quantifiers reflects an algebraic elimination theory. Examples are the theory of algebraically closed fields (where vanishing of the resultant, $R(f,g)=0$, gives a quantifier-free criterion for the existence of a common zero of two polynomials $f$, $g$), and the theory of real closed fields (where the Sturm theorem gives a quantifier-free criterion for a polynomial to admit a root in a given interval, cf. also Real closed field).

The fact that the theory of real closed fields admits elimination of quantifiers is commonly known as the Tarski–Seidenberg theorem (see also Semi-algebraic set). It implies that the semi-algebraic sets over a real closed field $K$ are precisely the definable sets (with parameters from $K$) in the first-order language of ordered fields. For the history and applications of the Tarski–Seidenberg theorem, and a remarkable discussion of the general technique of elimination of quantifiers, see [a2] and the literature cited therein. For applications of elimination of quantifiers to real and $p$-adic semi- and subanalytic sets, see [a1].

For certain elementary theories of algebraic systems, elimination of quantifiers implies closure properties of their models (cf. [a3]).

References

[a1] J. Denef, L. van den Dries, "$p$-adic and real subanalytic sets" Ann. of Math. , 128 (1988) pp. 79–138
[a2] L. van den Dries, "Alfred Tarski's elimination theory for real closed fields" J. Symb. Logic , 53 (1988) pp. 7–19
[a3] L. van den Dries, A. Macintyre, K. McKenna, "Elimination of quantifiers in algebraic structures" Adv. in Math. , 47 (1983) pp. 74–87
How to Cite This Entry:
Elimination of quantifiers. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Elimination_of_quantifiers&oldid=17833
This article was adapted from an original article by F.-V. Kuhlmann (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article