A procedure or property of a first-order theory or formal language by which every formula that may contain existential or universal quantifiers is transformed into an equivalent formula that contains no quantifiers, relative to the semantics of the theory.

Principle

If a theory admits quantifier elimination then for every formula φ(x) there exists a quantifier-free formula ψ(x) such that φ and ψ define the same set in every model of the theory; the procedure systematically rewrites quantified expressions using the primitives of the language and theory axioms.

Demonstration

In the theory of real closed fields, Tarski's procedure (operationalised by cylindrical algebraic decomposition) transforms a formula with polynomial inequalities and quantifiers into an equivalent quantifier-free Boolean combination of polynomial sign conditions, allowing decision of truth for sentences about real numbers.

Misapplication

Assuming quantifier elimination is available for arbitrary theories (for example Peano arithmetic) or using a 'quantifier-elimination' transform that only preserves satisfiability rather than equivalence; or applying the procedure without checking whether the target language can express the eliminated formula, leading to invalid rewritings.

Consequence

When successfully applied to a theory, quantifier elimination yields an effective decision procedure for sentences, characterisations of definable sets, and simpler formulas for model construction and query answering; it may however entail large blow-ups in formula size or complexity of computation.

Reversal

Introducing quantifiers (or reintroducing them) increases expressive power and can compactly describe families of structures or infinite behaviour that a quantifier-free formula cannot, so the inversion shows loss of succinctness or loss of definitional convenience.

Boundary

Applies to first-order settings and depends on the theory and language; some theories admit full elimination, some admit partial or relative elimination, and higher-order logics or theories with uninterpreted or higher-arity constructs may not admit elimination. Computational cost and representability in the target quantifier-free language are practical limits.

Semantic Tension

Tension arises between quantifier elimination and Skolemization: Skolemization removes existential quantifiers by adding function symbols but preserves satisfiability only, not equivalence; quantifier elimination preserves definitional equivalence but may require richer Boolean or algebraic constructions.

Synthesis

Quantifier elimination is both a semantic property of a theory and a family of syntactic procedures that replace quantified descriptions by equivalent quantifier-free formulas; its presence yields decidability and concrete descriptions of definable sets, while its absence signals inherent expressive or computational barriers.