In mathematics, the Tarski–Seidenberg theorem is a theorem on semialgebraic sets, that is, subsets of real coordinate spaces that can be defined by a finite set of polynomial equations and polynomial inequalities. This theorem was proved by Alfred Tarski in 1930 in view of his proof that the theory of real closed fields is complete (every formula can be proved either as true or as false) and admits quantifier elimination. The theorem was later discovered indepedently by Abraham Seidenberg in the context of constructive mathematics. The theorem states that, given a set S in the (n + 1)-dimensional space, which is defined by polynomial equations and inequalities involving (n + 1) variables, the projection eliminating one of the variables can be defined similarly. In other words, if F ( y , x 1 , … , x n ) {\displaystyle {\mathcal {F}}(y,x_{1},\ldots ,x_{n})} is the formula defining S, there exists a formula G ( x 1 , … , x n ) {\displaystyle {\mathcal {G}}(x_{1},\ldots ,x_{n})} that define the same set as ∃ y ∣ F ( y , x 1 , … , x n ) {\displaystyle \exists y\mid {\mathcal {F}}(y,x_{1},\ldots ,x_{n})} . Although the original proof of the theorem was constructive, the resulting algorithm is galactic, that is, it has a computational complexity that is far too high for using the method on a computer. George E. Collins introduced the algorithm of cylindrical algebraic decomposition, which allows quantifier elimination over the reals in double exponential time. This complexity is optimal, as there are examples where the output has a double exponential number of connected components. Collins's algorithm is therefore fundamental and widely used in computational algebraic geometry.
First order formulas A formula of the first-order theory of the real numbers is a well-formed formula involved only the quantifier ∀ , ∃ {\displaystyle \forall ,\exists } , the logical connectives ∧ , ∨ , ¬ {\displaystyle \land ,\lor ,\lnot } , real numbers and variables representing real numbers, equality and inequality signs = , < , ≤ {\displaystyle =,<,\leq } , and the basic arithmetic operators + , − , × , / {\displaystyle +,-,\times ,/} . A formula is quantifier free if does not involve any quantifier. Two formulas are equivalent if they evaluate to the same truth value for every choice of (real) values for the variables. In particular, a formula is true or false for every values of the variables if it is equivalent to 0 = 0 {\displaystyle 0=0} or 1 = 0 {\displaystyle 1=0} Elimination of quantifiers consists of providing an algorithm that, for every formula computes an equivalent quantifier-free formula. If quantifier elimination occurs, the theory is complete in the sense that one can decide whether a variable-free formula is true of false. Tarski–Seidenberg theorem is that quantifier elimination is possible in the first-order theory of the real numbers, and thus that this theory is complete
Semialgebraic sets
A semialgebraic set is a set defined by a quantifier-free formula of the first-order theory of the real numbers. By standard logical (disjunctive normal form) and algebraic manipulations, it is straightforward to show that a semialgebraic set in Rn is formed by taking a finite union of basic semialgebraic sets. A basic semialgebraic set is the set of all points that simultaneously satisfy a finite number of polynomial equations and inequalities of the form
p ( x 1 , … , x n ) = 0 {\displaystyle p(x_{1},\ldots ,x_{n})=0\,}
and
q ( x 1 , … , x n ) > 0 {\displaystyle q(x_{1},\ldots ,x_{n})>0\,}
for polynomials p and q. For example, a basic semialgebraic set in R {\displaystyle \mathbb {R} } either consists of a finite number of points or is a finite union of open intervals. Conversely a singleton formed by an algebraic number is a basic semialgebraic set, and every interval (open of not) is a semialgebraic set if its end points are algebraic numbers.
… excerpt ends here. Continue reading the full article.
