Definíció: f(x,y,...) azt jelöli, hogy f egy formula, amely szabad változói x,y,... T kvantoreliminálható ha minden f(x1,...,xk) formulához található olyan F(x1,...,xk) kvantormentes formula, amelyre T |= f <-> F.
Észrevétel: F(x,y,...) kvantormentes formula azt jelenti, hogy az x,y,... változójelek és konstansjelekből kifejezéseket építünk, majd reláció jelekkel atomi formulákat gyártunk és ezeket az ítéletkalkulus szabálya szerint kombináljuk. Zárt F kvantormentes formula azt jelenti, hogy a konstansjelekből kifejezéseket építünk, majd reláció jelekkel atomi formulákat gyártunk és ezeket az ítéletkalkulus szabálya szerint kombináljuk. Ha a t típus nem tartalmaz konstansokat, akkor zárt F kvantormentes formula azt jelenti, hogy F az `azonosan igaz' vagy az `azonosan hamis' logikai formula.
Észrevétel: T akkor és csak akkor kvantoreliminálható f= (létezik x) g formulákból (ahol g kvantormentes) a kvantor eliminálható.
Jelölés: A f= (létezik x) g formulákat lényegesnek nevezzük.
Bizonyítás: A kvantoreliminálhatóságból természetesen következik a lényeges formulák kvantorának eliminálhatósága.
Fordítva formula indukciót végzünk. Az egyetlen problémás lépést a feltételünk oldja meg.
Lemma: Legyen T egy kvantoreliminálható elmélet. tegyük fel, hogy a következő két feltétel valamelyike teljesül:
Tétel: A sűrű, végpont nélküli rendezések S elmélete kvantoreliminálható.
Bizonyítás: S kifejezései csak a változók. Az f=(létezik x) g lényeges formula kvantormentes g része (y = z) és (y <= z), illetve ezek negáltjaiból építkezik VAGY és ÉS logikai jelek segítségével. Ez átírható úgy, hogy (y =z) és (y < z) alakú atomokból építkezzünk. A fel'epített formulát DNF normálformába írhatjuk. Elég (létezik x) c -ből eliminálni a kvantort, ahol c egy klóz a DNF alakban. Ez könnyen megtehető.
Tétel: Legyen T egy elmélet, ami rendelkezik a következő két tulajdonsággal
Következmény: Legyen Z a 0 karakterisztikájú, algebrailag zárt testek elmélete. Z kvantoeliminálható. Továbbá Z teljes.