Quantorenelimination bezeichnet in der Modelltheorie eine bestimmte Eigenschaft von Theorien: Man sagt, eine Theorie habe Quantorenelimination, wenn jede Formel innerhalb der Theorie zu einer Formel ohne Quantoren äquivalent ist. So ist beispielsweise in einem Körper (also etwa in den reellen Zahlen) die Formel ${\displaystyle \varphi (x)=\exists y(x\cdot y\doteq 1)}$, die besagt, dass ${\displaystyle x}$ ein multiplikatives inverses Element besitzt, äquivalent zu ${\displaystyle \rho (x)=\neg (x\doteq 0)}$, also dazu, dass ${\displaystyle x\neq 0}$. In ${\displaystyle \rho (x)}$ kommen keine Quantoren mehr vor. Lässt sich jede Formel in eine solche quantorenfreie Formel umformen, so besitzt die Theorie Quantorenelimination. In Theorien mit Quantorenelimination können also beliebige Formeln in quantorenfreie und damit einfachere Formeln umgeformt werden.

Sei ${\displaystyle L}$ eine Sprache und ${\displaystyle T}$ eine Theorie (also eine Aussagenmenge). Dann hat ${\displaystyle T}$ Quantorenelimination, falls für alle ${\displaystyle L}$-Formeln ${\displaystyle \varphi (x_{1},\ldots ,x_{n})}$ eine quantorenfreie ${\displaystyle L}$-Formel ${\displaystyle \rho (x_{1},\ldots ,x_{n})}$ existiert mit ${\displaystyle T\vdash \forall x_{1}\ldots \forall x_{n}(\varphi (x_{1},\ldots ,x_{n})\leftrightarrow \rho (x_{1},\ldots ,x_{n}))}$.

Um zu überprüfen, ob eine Theorie Quantorenelimination besitzt, genügt es, dies nur für eine einfache Art von Formeln nachzuweisen: Der Allquantor kann mit Hilfe einer doppelten Negation in einen Existenzquantor überführt werden. Diese kann man induktiv von innen nach außen entfernen, sodass nur für Formeln der Gestalt ${\displaystyle \exists x(\rho (x,y_{1},\ldots ,y_{n}))}$ mit quantorenfreiem ${\displaystyle \rho (x,y_{1},\ldots ,y_{n})}$ nachgewiesen werden muss, dass sie äquivalent zu einer quantorenfreien Formel sind.

Bringt man ${\displaystyle \rho (x,y_{1},\ldots ,y_{n})}$ in disjunktive Normalform und zieht den Existenzquantor an der Disjunktion vorbei nach innen, so sieht man, dass man sich dabei auf solche Formeln ${\displaystyle \rho (x,y_{1},\ldots ,y_{n})}$ beschränken kann, die aus einer Konjunktion elementarer Formeln oder Negationen solcher Formeln bestehen. Formeln der Form ${\displaystyle \exists x(\rho (x,y_{1},\ldots ,y_{n}))}$, bei denen ${\displaystyle \rho }$ diese Gestalt hat, nennt man auch primitive Existenzformeln.

Die Theorie unendlicher Mengen lässt sich in einer Sprache ohne Konstanten-, Funktions- und Relationssymbole formulieren: Die Formel ${\displaystyle \varphi _{n}=\exists x_{1},\ldots ,x_{n}\bigwedge _{1\leq i<j\leq n}\neg x_{i}\doteq x_{j}}$ besagt, dass es mindestens ${\displaystyle n}$ Elemente gibt. ${\displaystyle T_{\infty }=\{\varphi _{n}|n\in \mathbb {N} \}}$ axiomatisiert daher unendliche Mengen. Eine primitive Existenzformel hat die Gestalt ${\displaystyle \exists x(\bigwedge _{i\in I}x\doteq y_{i}\wedge \bigwedge _{j\in J}\neg x\doteq z_{j}\wedge \rho )}$, wobei ${\displaystyle \rho }$ quantorenfrei ist und beliebige freie Variablen besitzt. Ist ${\displaystyle I\neq \emptyset }$, so ist die Formel zu ${\displaystyle \bigwedge _{i,j\in I}y_{i}\doteq y_{j}\wedge i_{0}\in I\wedge \bigwedge _{j\in J}\neg y_{i_{0}}\doteq z_{j}\wedge \rho }$ äquivalent. Denn die Formel sagt aus, dass ein ${\displaystyle x}$ gesucht ist, das mit allen ${\displaystyle y_{i}}$ übereinstimmt, sodass nur noch eine Möglichkeit für ${\displaystyle x}$ bleibt. Ist dagegen ${\displaystyle I=\emptyset }$, so ist die Formel äquivalent zu ${\displaystyle \rho }$, da ein von allen ${\displaystyle z_{j}}$ verschiedenes ${\displaystyle x}$ gesucht ist, das nach den Axiomen der Theorie unendlicher Mengen immer existiert. Somit ist jede primitive Existenzformel zu einer quantorenfreien Formel äquivalent; die Theorie besitzt Quantorenelimination.

Viele weitere Theorien besitzen Quantorenelimination, darunter die folgenden:

• die Theorie der algebraisch abgeschlossenen Körper
• die Theorie der dichten linearen Ordnungen ohne Endpunkte
• für einen festen Körper ${\displaystyle K}$ die Theorie der unendlichen ${\displaystyle K}$-Vektorräume
• die Theorie der reell abgeschlossenen Körper

Eine konsistente Theorie ohne Konstanten, die Quantorenelimination besitzt, ist automatisch vollständig, das heißt, sie beweist für jede Aussage ${\displaystyle \varphi }$ entweder ${\displaystyle \varphi }$ selbst oder ${\displaystyle \neg \varphi }$. Dies sieht man folgendermaßen ein: Jede Aussage ${\displaystyle \varphi }$ ist in der Theorie äquivalent zu einer quantorenfreien Aussage. Da es aber keine Konstanten gibt, sind die einzigen quantorenfreien Aussagen die wahre (${\displaystyle \top }$) und die falsche (${\displaystyle \bot }$) Aussage. Damit beweist die Theorie entweder ${\displaystyle \varphi }$ oder ${\displaystyle \neg \varphi }$. Ein Beispiel für diesen Fall ist die obige Theorie unendlicher Mengen.

Allgemein gilt: Eine Theorie mit Quantorenelimination ist modellvollständig: Sind ${\displaystyle {\mathcal {A}}\subset {\mathcal {B}}}$ zwei Modelle von ${\displaystyle T}$, so ist ${\displaystyle {\mathcal {A}}\prec {\mathcal {B}}}$ eine elementare Erweiterung, die Theorien ${\displaystyle Th({\mathcal {A}})}$ und ${\displaystyle Th({\mathcal {B}})}$ von ${\displaystyle {\mathcal {A}}}$ und ${\displaystyle {\mathcal {B}}}$ stimmen überein. Wegen der Quantorenelimination muss dies nur für quantorenfreie Formeln nachgewiesen werden, solche gelten aber genau dann in ${\displaystyle {\mathcal {A}}}$, wenn sie in ${\displaystyle {\mathcal {B}}}$ gelten, da ${\displaystyle {\mathcal {A}}}$ Unterstruktur von ${\displaystyle {\mathcal {B}}}$ ist.

In der algebraischen Geometrie beschäftigt man sich mit algebraischen Varietäten, den Nullstellenmengen von Polynomen. Von Chevalley stammt der Satz, dass die Projektion einer solchen Varietät auf einen Unterraum wieder durch Polynome beschrieben werden kann, falls der Grundkörper algebraisch abgeschlossen ist. Dies lässt sich beweisen, indem man die Quantorenelimination der Theorie der algebraisch abgeschlossenen Körper verwendet: Sei die Varietät definiert als die Nullstellenmenge der Polynome ${\displaystyle f_{i}(x_{1},\ldots ,x_{n})}$ für ${\displaystyle i=1,\ldots m}$. Die Projektion auf die ersten ${\displaystyle k}$ Koordinaten ist dann gegeben durch ${\displaystyle \varphi (x_{1},\ldots ,x_{k})=\exists x_{k+1},\ldots ,x_{n}(f_{1}(x_{1},\ldots ,x_{n})\doteq 0\wedge \ldots \wedge f_{m}(x_{1},\ldots ,x_{n})\doteq 0)}$. Diese Formel ist äquivalent zu einer quantorenfreien Formel, welche eine boolesche Kombination von elementaren Formeln der Art „Polynome = 0“ ist, die Projektion ist also eine boolesche Kombination von Varietäten.

Auch der Hilbertsche Nullstellensatz hat einen Beweis, der auf der Quantorenelimination der Theorie algebraisch abgeschlossener Körper beruht.^[1] Für Hilberts siebzehntes Problem existiert ein Beweis, der auf der Quantorenelimination der Theorie reell abgeschlossener Körper beruht.^[1]

• Wilfrid Hodges: Model theory. Cambridge University Press, 1993, ISBN 0-521-30442-3.

• Eric W. Weisstein: Quantifier Elimination. In: MathWorld (englisch).

1. ↑ ^{a b} Martin Ziegler: Skript Modelltheorie 1. (PDF; 649 kB) S. 43 ff.