Quantifier elimination

Summary

A theory has quantifier elimination when every formula is equivalent, modulo the theory, to a formula without quantifiers. Then the definable sets of its models are simple to describe, and questions about the theory reduce to questions about quantifier-free formulas. Quantifier elimination often gives completeness and decidability. Classical examples are dense linear orders without endpoints, algebraically closed fields, and real closed fields in the language of ordered rings.