Definable sets + quantifier elimination

Theory T admits QE iff every formula equivalent to quantifier-free. Tarski-Seidenberg (RCF) / ACF / Presburger (linear arithmetic over ℤ). Foundation of decidability + complexity in logic.