A theory T admits quantifier elimination if there is an algorithm that given a formula F, returns a quantifier-free formula G that is T-equivalent to F. (In this case, T is decidable if the satisfiability of quantifier-free fragment of T is decidable)
- linear integer arithmetic 可以量词消去（由 Presburger arithmetic 的可判定性）
- Tarski’s Theorem 证明了 theory of reals 可以量词消去