Elimination of quantifiers

Quantifier elimination is a concept of used in mathematical logic, model theory, and theoretical computer science. 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 formulae 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).

Examples of theories that have been shown decidable using quantifier elimination are Presburger arithmetic,algebraically closed fields, real closed fields, atomless Boolean algebras, term algebras, dense linear orders,abelian groups,random graphs as well as many of their combinations such as Boolean algebra with Presburger arithmetic, and term algebras with queues.

...
Wikipedia