Quantifier Elimination

Quantifier elimination is the property that every formula in a theory is equivalent to one without quantifiers, a powerful structural feature that yields decision procedures and a clear description of definable sets.

Definition

A theory admits quantifier elimination if every formula is equivalent, modulo the theory, to a quantifier-free formula in the same free variables; this means the definable sets are exactly the Boolean combinations of those defined by atomic formulas.

Scope

This topic covers the definition of quantifier elimination, criteria for establishing it, the related notion of model completeness, and the canonical examples of dense linear orders, algebraically closed fields, real closed fields, and Presburger arithmetic, along with the decidability results these examples imply.

Core questions

• When can quantifiers be systematically removed from formulas of a theory?
• How does quantifier elimination describe the definable sets of a structure?
• Why does quantifier elimination often yield decidability?
• Which classical algebraic theories admit quantifier elimination?

Key theories

Quantifier elimination test

It suffices to eliminate a single existential quantifier from conjunctions of atomic and negated atomic formulas, reducing the property to a manageable local condition often checked via embeddings of substructures.

Algebraically and real closed fields

The theories of algebraically closed fields and of real closed fields admit quantifier elimination, so their definable sets are the constructible and the semialgebraic sets respectively, recovering classical geometry.

Tarski decision procedure

Quantifier elimination for real closed fields gives an algorithm deciding the truth of any first-order statement about the real numbers in the language of ordered fields, so elementary algebra and geometry are decidable.

Clinical relevance

Quantifier elimination converts logical questions into algebra: it provides decision procedures used in computer algebra and verification, and its geometric content, such as the semialgebraic nature of definable sets over the reals, connects model theory to real algebraic geometry and o-minimality.

History

Quantifier elimination was used by Skolem, Langford, and Presburger in the 1920s and 1930s to decide specific theories, and Tarski established it for real closed fields, yielding his celebrated decision procedure for elementary algebra and geometry. Robinson recast the surrounding ideas through model completeness, making the technique a staple of applied model theory.

Key figures

• Alfred Tarski
• Thoralf Skolem
• Abraham Robinson
• Mojzesz Presburger

Seminal works

• marker2002
• hodges1993
• tarski1951

Frequently asked questions

Why does quantifier elimination make a theory decidable?

A sentence has no free variables, so eliminating its quantifiers leaves a quantifier-free sentence built from atomic statements about the constants, whose truth can be checked directly. If elimination is effective, this gives an algorithm to decide every sentence.

Does every theory admit quantifier elimination?

No. Many theories do not, and one can sometimes add definable predicates to the language to obtain it. Quantifier elimination is a special and useful property, characteristic of theories with a particularly transparent description of their definable sets.