Verfahren, mit dessen Hilfe ein logischer Ausdruck aus einer elementaren Sprache unter Zugrundelegung einer elementaren Theorie (deduktiver Abschluß) äquivalent ersetzt werden kann durch einen Ausdruck derselben Sprache, der jedoch keine Quantoren enthält.

Eine elementare Theorie T, formuliert in der elementaren Sprache L, erlaubt die Elimination der Quantoren, wenn es zu jeder L-Formelϕ eine quantorenfreie L-Formel ψ gibt, so daß aus T der Ausdruck ϕ ↔ ψ folgt, d. h., wenn jedes Modell von T auch ein Modell von ϕ ↔ ψ ist.