The theory of real closed fields admits quantifier elimination, meaning every first-order formula over the real numbers is equivalent to one with no quantifiers. Proved by Alfred Tarski and, independently with an algorithmic method, by Abraham Seidenberg, it shows real algebraic geometry is, in a precise sense, decidable.
Facts
StatementThe theorem concerns semialgebraic sets, subsets of real coordinate space defined by finitely many polynomial equations and inequalities, and shows that projecting a semialgebraic set onto fewer coordinates yields another semialgebraic set, giving quantifier elimination for the theory of real closed fields. 1 Proof YearTarski proved this in 1930. Abraham Seidenberg later found an independent proof in the context of constructive mathematics, undated in the cited source. Classification
Statement FormCharacterization Theorem 1 Connections
Sources
1. Tarski-Seidenberg Theorem (Wikipedia)
Wikimedia Foundationlead paragraph, first sentence
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.
history section, attribution sentence
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.
View the Source Reader Challenges (0)
No disputes yet. Spotted an error or a better source? Open the first one.
Sign in to dispute this or suggest a correction.