Quelltext der Seite Quantorenelimination

'''Quantorenelimination''' bezeichnet in der [[Modelltheorie]] eine bestimmte Eigenschaft von Theorien: Man sagt, eine Theorie habe Quantorenelimination, wenn jede [[Logische Formel|Formel]] innerhalb der Theorie zu einer Formel ohne [[Quantor]]en äquivalent ist. So ist beispielsweise in einem [[Körper (Algebra)|Körper]] (also etwa in den [[Reelle Zahl|reellen Zahlen]]) die Formel <math>\varphi(x)=\exists y(x\cdot y\doteq 1)</math>, die besagt, dass <math>x</math> ein multiplikatives [[inverses Element]] besitzt, äquivalent zu <math>\rho(x)=\neg(x\doteq 0)</math>, also dazu, dass <math>x\neq 0</math>. In <math>\rho(x)</math> 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.

== Definition ==
Sei <math>L</math> eine [[Elementare Sprache|Sprache]] und <math>T</math> eine Theorie (also eine [[Logische Aussage|Aussagenmenge]]). Dann hat <math>T</math> Quantorenelimination, falls für alle <math>L</math>-Formeln <math>\varphi(x_1,\ldots,x_n)</math> eine quantorenfreie <math>L</math>-Formel <math>\rho(x_1,\ldots,x_n)</math> existiert mit <math>T\vdash\forall x_1\ldots\forall x_n (\varphi(x_1,\ldots,x_n)\leftrightarrow\rho(x_1,\ldots,x_n))</math>.

== Einfaches Kriterium ==
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 <math>\exists x(\rho(x,y_1,\ldots,y_n))</math> mit quantorenfreiem <math>\rho(x,y_1,\ldots,y_n)</math> nachgewiesen werden muss, dass sie äquivalent zu einer quantorenfreien Formel sind.

Bringt man <math>\rho(x,y_1,\ldots,y_n)</math> in [[disjunktive Normalform]] und zieht den Existenzquantor an der [[Disjunktion]] vorbei nach innen, so sieht man, dass man sich dabei auf solche Formeln <math>\rho(x,y_1,\ldots,y_n)</math> beschränken kann, die aus einer [[Konjunktion (Logik)|Konjunktion]] elementarer Formeln oder [[Negation]]en solcher Formeln bestehen.
Formeln der Form <math>\exists x(\rho(x,y_1,\ldots,y_n))</math>, bei denen <math>\rho</math> diese Gestalt hat, nennt man auch primitive Existenzformeln.

== Beispiele ==
=== Unendliche Mengen ===
Die Theorie [[unendlich]]er Mengen lässt sich in einer Sprache ohne Konstanten-, Funktions- und Relationssymbole formulieren: Die Formel <math>\varphi_n=\exists x_1,\ldots,x_n\bigwedge_{1\leq i<j\leq n}\neg x_i\doteq x_j</math> besagt, dass es mindestens <math>n</math> Elemente gibt. <math>T_\infty=\{\varphi_n|n\in\N\}</math> axiomatisiert daher unendliche Mengen. Eine primitive Existenzformel hat die Gestalt <math>\exists x(\bigwedge_{i\in I}x\doteq y_i\wedge\bigwedge_{j\in J}\neg x\doteq z_j\wedge\rho)</math>, wobei <math>\rho</math> quantorenfrei ist und beliebige freie Variablen besitzt. Ist <math>I\neq\empty</math>, so ist die Formel zu <math>\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</math> äquivalent. Denn die Formel sagt aus, dass ein <math>x</math> gesucht ist, das mit allen <math>y_i</math> übereinstimmt, sodass nur noch eine Möglichkeit für <math>x</math> bleibt. Ist dagegen <math>I=\empty</math>, so ist die Formel äquivalent zu <math>\rho</math>, da ein von allen <math>z_j</math> verschiedenes <math>x</math> 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.

=== Weitere Beispiele ===
Viele weitere Theorien besitzen Quantorenelimination, darunter die folgenden:
* die Theorie der [[algebraisch abgeschlossen]]en Körper
* die Theorie der [[Modelltheorie#Dichte Ordnungen|dichten linearen Ordnungen ohne Endpunkte]]
* für einen festen Körper <math>K</math> die Theorie der unendlichen <math>K</math>-[[Vektorraum|Vektorräume]]
* die Theorie der [[Reell abgeschlossener Körper|reell abgeschlossenen Körper]]

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

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

=== Algebraische Geometrie ===
In der algebraischen Geometrie beschäftigt man sich mit [[Algebraische Varietät|algebraischen Varietäten]], den [[Nullstellenmenge]]n von Polynomen. Von [[Claude Chevalley|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 <math>f_i(x_1,\ldots,x_n)</math> für <math>i=1,\ldots m</math>. Die Projektion auf die ersten <math>k</math> Koordinaten ist dann gegeben durch <math>\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)</math>. 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.

=== Weitere Anwendungen ===
Auch der [[Hilbertscher Nullstellensatz|Hilbertsche Nullstellensatz]] hat einen Beweis, der auf der Quantorenelimination der Theorie algebraisch abgeschlossener Körper beruht.<ref name="ziegler">Martin Ziegler: [http://home.mathematik.uni-freiburg.de/ziegler/skripte/modell1.pdf ''Skript Modelltheorie 1''.] (PDF; 649&nbsp;kB) S. 43 ff.</ref>
Für [[Hilbertsche Probleme#Hilberts siebzehntes Problem|Hilberts siebzehntes Problem]] existiert ein Beweis, der auf der Quantorenelimination der Theorie reell abgeschlossener Körper beruht.<ref name="ziegler" />

== Literatur ==
* [[Wilfrid Hodges]]: ''Model theory''. Cambridge University Press, 1993, ISBN 0-521-30442-3.

== Weblinks ==
* {{MathWorld |id=QuantifierElimination |title=Quantifier Elimination}}

== Einzelnachweise ==
<references />

[[Kategorie:Modelltheorie]]