Ein Metasatz, klassisch für die Prädikatenlogik erster Stufe, der aussagt, dass falls eine Formel semantisch aus einer Menge von Sätzen folgt, sie syntaktisch aus diesen Sätzen beweisbar ist; semantische Konsequenz impliziert syntaktische Ableitbarkeit (Σ ⊨ φ ⇒ Σ ⊢ φ).

Prinzip

Alle semantischen Konsequenzen sind durch das Beweissystem erfassbar: für die Logiken, für die der Satz gilt, stimmen modelltheoretische Folgerung und Beweisbarkeit überein.

Demonstration

Gödels Vollständigkeitsbeweis für die Prädikatenlogik erster Stufe konstruiert eine maximal konsistente Menge oder verwendet Henkin-Erweiterungen, um aus einer konsistenten Theorie ein Modell zu bauen, in dem jede semantisch folgende Formel wahr ist, und zeigt so Σ ⊨ φ ⇒ Σ ⊢ φ.

Fehlanwendung

Den Satz mit Gödels Unvollständigkeitssätzen für arithmetische Theorien zu verwechseln oder anzunehmen, Vollständigkeit gelte für höherstufige Logiken oder für Logiken mit nichtstandardmäßigen Semantiken ohne Prüfung.

Konsequenz

Gleicht beweistheoretische und modelltheoretische Methoden für die jeweilige Logik an und ermöglicht Ableitungen wie das Kompaktheitstheorem und Löwenheim–Skolem-Eigenschaften.

Umkehrung

Korrektheit liefert die Umkehrung (Beweisbarkeit impliziert semantische Gültigkeit); zusammen ergeben Korrektheit und Vollständigkeit die Äquivalenz von Syntax und Semantik.

Abgrenzung

Gilt für klassische Prädikatenlogik erster Stufe mit Standardssemantik und geeigneten Beweissystemen; sie kann für höherstufige Logiken, bestimmte modale Semantiken oder für Systeme ohne passende Regeln versagen.

Semantische Spannung

Spannung zwischen Ausdruckskraft und Entscheidbarkeit: Vollständigkeit kann mit dem Verlust von Entscheidbarkeit einhergehen oder mit der Unfähigkeit, intensionalen Gehalt zu erfassen; oft im Kontrast zu Unvollständigkeitsergebnissen in der Arithmetik.

Synthese

Vollständigkeit schließt die vom Korrektheitssatz gelassene Lücke, indem sie sicherstellt, dass semantisch wahre Aussagen (relativ zur spezifizierten Semantik) durch syntaktische Beweise in der Ziel-Logik erreichbar sind; ihre Geltung hängt jedoch von Struktur und Semantik der Logik ab.