Quantifier elimination

Quantifier elimination is the property that every formula in a theory is equivalent to a quantifier-free formula, or a procedure that finds such formulas. It often turns logical definability into explicit algebraic or geometric conditions.

Model theory: The study of mathematical structures and the first-order languages used to describe them. Quantifier elimination is a central model-theoretic property of theories.
Algebraically closed field: A field in which every nonconstant polynomial has a root. In this theory, formulas reduce to Boolean combinations of polynomial equations.
Alfred Tarski: A Polish-American logician and mathematician who made foundational contributions to logic, algebra, and geometry. Tarski developed elimination methods for real closed fields and proved their decidability.
Skolemization: A transformation replacing existential quantifiers with function symbols in a first-order formula. It changes the language and preserves satisfiability rather than producing an equivalent quantifier-free formula.
Semialgebraic set: A subset of real coordinate space defined by finitely many polynomial equations and inequalities combined with Boolean operations. Quantifier elimination proves that projections of such sets remain semialgebraic.
Definable set: A set specified by a formula with parameters in a mathematical structure. Elimination shows that definable sets can sometimes be described without quantified variables.
Real closed field: An ordered field with the algebraic properties of the real numbers. Its theory eliminates quantifiers using polynomial equalities and inequalities.
Tarski–Seidenberg theorem: The projection of a semialgebraic set over the real numbers is semialgebraic. It is the geometric form of quantifier elimination for real closed fields.
Prenex normal form: A first-order formula written with all quantifiers in a leading prefix. It rearranges quantifiers instead of removing them.
Real algebraic geometry: The study of algebraic varieties and polynomial inequalities over real numbers. Elimination supplies a logical foundation for describing projections and deciding polynomial conditions.

Linked from 5 pages