Quantorenelimination

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 Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \varphi(x)=\exists y(x\cdot y\doteq 1)} , die besagt, dass Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle x} ein multiplikatives inverses Element besitzt, äquivalent zu Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \rho(x)=\neg(x\doteq 0)} , also dazu, dass Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle x\neq 0} . In Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\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.

Definition

Sei $L$ eine Sprache und Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle T} eine Theorie (also eine Aussagenmenge). Dann hat Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle T} Quantorenelimination, falls für alle Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle L} -Formeln Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \varphi(x_1,\ldots,x_n)} eine quantorenfreie Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle L} -Formel Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \rho(x_1,\ldots,x_n)} existiert mit $T\vdash \forall x_{1}\ldots \forall x_{n}(\varphi (x_{1},\ldots ,x_{n})\leftrightarrow \rho (x_{1},\ldots ,x_{n}))$.

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 $\exists x(\rho (x,y_{1},\ldots ,y_{n}))$ mit quantorenfreiem Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \rho(x,y_1,\ldots,y_n)} nachgewiesen werden muss, dass sie äquivalent zu einer quantorenfreien Formel sind.

Bringt man Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\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 Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\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 Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \exists x(\rho(x,y_1,\ldots,y_n))} , bei denen Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \rho} diese Gestalt hat, nennt man auch primitive Existenzformeln.

Beispiele

Unendliche Mengen

Die Theorie unendlicher Mengen lässt sich in einer Sprache ohne Konstanten-, Funktions- und Relationssymbole formulieren: Die Formel Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\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 Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle n} Elemente gibt. $T_{\infty }=\{\varphi _{n}|n\in \mathbb {N} \}$ axiomatisiert daher unendliche Mengen. Eine primitive Existenzformel hat die Gestalt Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \exists x(\bigwedge_{i\in I}x\doteq y_i\wedge\bigwedge_{j\in J}\neg x\doteq z_j\wedge\rho)} , wobei Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \rho} quantorenfrei ist und beliebige freie Variablen besitzt. Ist Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle I\neq\empty} , so ist die Formel zu Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\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 $x$ gesucht ist, das mit allen Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle y_i} übereinstimmt, sodass nur noch eine Möglichkeit für Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle x} bleibt. Ist dagegen Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle I=\empty} , so ist die Formel äquivalent zu Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \rho} , da ein von allen Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle z_j} verschiedenes Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\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.

Weitere Beispiele

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 $K$ die Theorie der unendlichen Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle K} -Vektorräume
• die Theorie der reell abgeschlossenen Körper

Anwendungen

Vollständigkeit

Eine konsistente Theorie ohne Konstanten, die Quantorenelimination besitzt, ist automatisch vollständig, das heißt, sie beweist für jede Aussage Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \varphi} entweder Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \varphi} selbst oder Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \neg\varphi} . Dies sieht man folgendermaßen ein: Jede Aussage $\varphi$ ist in der Theorie äquivalent zu einer quantorenfreien Aussage. Da es aber keine Konstanten gibt, sind die einzigen quantorenfreien Aussagen die wahre (Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \top} ) und die falsche (Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \bot} ) Aussage. Damit beweist die Theorie entweder Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \varphi} oder Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\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 ${\mathcal {A}}\subset {\mathcal {B}}$ zwei Modelle von Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle T} , so ist Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \mathcal A\prec\mathcal B} eine elementare Erweiterung, die Theorien Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle Th(\mathcal A)} und $Th({\mathcal {B}})$ von Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \mathcal A} und Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \mathcal B} stimmen überein. Wegen der Quantorenelimination muss dies nur für quantorenfreie Formeln nachgewiesen werden, solche gelten aber genau dann in Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \mathcal A} , wenn sie in Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \mathcal B} gelten, da Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \mathcal A} Unterstruktur von Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \mathcal B} ist.

Algebraische Geometrie

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 $f_{i}(x_{1},\ldots ,x_{n})$ für Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle i=1,\ldots m} . Die Projektion auf die ersten Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle k} Koordinaten ist dann gegeben durch Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\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.

Weitere Anwendungen

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

Literatur

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

Weblinks

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