Let $R$ be an ordered field. A semialgebraic set is a subset of a product space $R^n$ that is a Boolean combination of sets defined by polynomial inequalities:
In other words, a semialgebraic set is a finite union of loci defined by systems of polynomial inequalities
The fundamental theorem for semialgebraic sets over real closed fields $R$ is as follows.
(Tarski-Seidenberg) The image of a semialgebraic set in $R^{n+1}$ under the projection map
is also a semi-algebraic set.
This remarkable theorem has far-reaching consequences for the theory of ordered fields. For one, it is called a “quantifier elimination” result because it says that any first-order predicate in the theory of ordered fields (with signature $(0, 1, +, -, \cdot, \lt)$) is equivalent to a predicate which is quantifier-free. This follows from a straightforward induction coupled with the observation that the Tarski–Seidenberg theorem directly says that if a predicate $R(x_1, \ldots, x_n, y)$ is a Boolean combination of atomic formulas (thus defining a semi-algebraic set), then
is also definable by a Boolean combination of atomic formulas; hence the existential quantifier can be eliminated.
From here, it may be shown that the theory of real closed fields is decidable: that each sentence in the theory is provably true or provably false. In fact, a real closed field is elementarily equivalent to the ordered field of real numbers, and so the theory of the real numbers (as ordered field) is decidable. As special cases, we have that
Euclidean geometry is decidable.
Differential calculus over the real numbers is decidable.
The collection of semialgebraic sets is the archetypal example of an o-minimal structure.
A semialgebraic relation of arity $m \to n$ is an ordered triple $(m, n, R)$ where $R$ is a semialgebraic subset of $R^{m+n}$.
The composite of two semialgebraic relations $R: m \to n$, $S: n \to p$ is the triple $(m, p, S \circ R)$ where
here $S \circ R$ is semialgebraic by the Tarski-Seidenberg theorem. In brief, semialgebraic relations form a cartesian bicategory of relations.
Last revised on April 18, 2013 at 18:33:12. See the history of this page for a list of all contributions to it.