Quantifier elimination

Quantifier elimination is a concept of simplification used in mathematical logic, model theory, and theoretical computer science. Informally, a quantified statement "${\displaystyle \exists x}$ such that ${\displaystyle \ldots }$" can be viewed as a question "When is there an ${\displaystyle x}$ such that ${\displaystyle \ldots }$?", and the statement without quantifiers can be viewed as the answer to that question.^[1]

One way of classifying formulas is by the amount of quantification. Formulas with less depth of quantifier alternation are thought of as being simpler, with the quantifier-free formulas as the simplest. A theory has quantifier elimination if for every formula ${\displaystyle \alpha }$, there exists another formula ${\displaystyle \alpha _{QF}}$ without quantifiers that is equivalent to it (modulo this theory).