Definition
Eine Verfeinerung einer prädikatenlogischen Theorie T, die eine Theorie T* (falls existent) erzeugt, deren Modelle genau die existential-abgeschlossenen Modelle von T sind; T* ist modellvollständig, wenn jede Einbettung zwischen Modellen von T* elementar ist, äquivalent dazu ist jede Formel in T* äquivalent zu einer existentiellen Formel.
Prinzip
Prinzip
Man identifiziert die Klasse existential-abgeschlossener Modelle innerhalb der Modelle von T und axiomatisiert deren Theorie T* so, dass für Modelle M ⊆ N von T* die Inklusion elementar ist; die Modellkompletion liefert, falls vorhanden, Quantorreduktion bis zu existentiellen Formeln und starke Transfereigenschaften für Einbettungen.
Demonstration
Demonstration
Die Theorie der algebraisch abgeschlossenen Körper ist die Modellkompletion der Theorie der Körper: Jeder Körper lässt sich in einen algebraisch abgeschlossenen Körper einbetten, der für polynomiale Gleichungen existential-abgeschlossen ist, und algebraisch abgeschlossene Körper machen Einbettungen elementar, was Modellvollständigkeit ergibt.
Fehlanwendung
Fehlanwendung
Ohne Konstruktion oder Eindeutigkeitsbeweis anzunehmen, dass für eine beliebige Theorie eine Modellkompletion existiert, ist irreführend — viele Theorien besitzen keine Modellkompletion, und das Erzwingen eines Kandidaten ohne Prüfung der existentialen Abschlossenheit oder Elementarität führt zu falschen modelltheoretischen Aussagen.
Konsequenz
Konsequenz
Existiert eine Modellkompletion, gewinnt man ein einheitliches modelltheoretisches Kontrollinstrument: Quantorreduktion, starke Homogenität der Modelle, Entscheidbarkeit und Transfer von Eigenschaften über Einbettungen sowie eine kanonische Beschreibung existential-genericer Strukturen innerhalb der Ausgangstheorie.
Umkehrung
Umkehrung
Die umgekehrte Sicht ist das Studieren eines Modellbegleiters oder einer konservativen Erweiterung: Anstatt T zu seinen existential-abgeschlossenen Modellen zu vervollständigen, beschränkt man sich auf bestimmte nicht-existential-abgeschlossene Unterklassen oder betrachtet konservative Erweiterungen, die mehr Syntax bewahren, aber keine Modellvollständigkeit bieten.
Abgrenzung
Abgrenzung
Gilt für prädikatenlogische Theorien und betrifft ihre modelltheoretische Hülle von existential-abgeschlossenen Modellen; schließt Nicht-erstordnungslogiken aus, sofern nicht umformuliert, und nicht jede Theorie besitzt eine Modellkompletion oder einen Modellbegleiter.
Semantische Spannung
Semantische Spannung
Modellkompletion wird leicht mit Quantorenelimination, Modellbegleiter oder algebraischem Abschluss verwechselt; die Spannung liegt darin, dass Modellvollständigkeit eine semantische Eigenschaft über Einbettungen und existentiale Abschlossenheit ist, während Quantorenelimination eine stärkere syntaktische Forderung darstellt.
Synthese
Synthese
Modellkompletion charakterisiert die maximale Theorie zu T, deren Modelle existential-abgeschlossen sind: Falls T* existiert, macht sie Einbettungen elementar und vereinfacht die Theorie, indem sie den Fokus auf generische existentielle Lösungen legt und Quantoren vereinfacht.