Ein Verfahren zur Konstruktion eines Modells einer konsistenten erstordentlichen Theorie, indem man die konsistente Formelmenge zu einer maximal konsistenten (Henkin-)Theorie erweitert, die explizite Zeugen-Konstanten für existentielle Formeln enthält, und dann das kanonische Termmodell (oder den Quotienten nach beweisbarer Gleichheit) bildet. Es liegt Beweisen der Vollständigkeit und der Existenz von Modellen zugrunde.

Prinzip

Für jede Formel ∃x φ(x) eine frische Konstante c_φ einführen und das Axiom φ(c_φ) hinzufügen; den Sprache- und Theorieraum so erweitern, dass jede existentielle Formel einen Zeugen hat, dann mittels Zorns Lemma oder Lindenbaum-Argument zu einer maximal konsistenten Menge erweitern und Terme interpretieren, um ein Modell zu erhalten.

Demonstration

Beginne mit einer konsistenten Theorie T in Sprache L. Formuliere eine Aufzählung der Formeln, und wann immer ∃x φ(x) auftaucht, führe eine neue Konstante c ein und füge φ(c) zur Theorie hinzu, dabei die Konsistenz bewahren; wiederhole dies und nehme dann eine maximal konsistente Henkin-Theorie T* in der erweiterten Sprache. Die Menge abgeschlossener Terme modulo beweisbarer Gleichheit bildet ein Modell von T*, dessen Redukt T erfüllt.

Fehlanwendung

Zeugen sorglos hinzufügen ohne Konsistenzprüfung, oder annehmen, Henkinisierung liefere ein Modell in der ursprünglichen Sprache ohne Konservativitätsprüfung. Ein weiterer Missbrauch ist, Henkin-Konstanten außerhalb des konstruierten Modells als bedeutungsvoll zu behandeln, ohne die syntaktische Identifikation zu beachten.

Konsequenz

Ermöglicht einen konstruktiven Zugang zum Vollständigkeitssatz und zur Konstruktion konkreter Modelle aus konsistenten Theorien; liefert Termmodelle und zeigt, dass syntaktische Konsistenz semantische Erfüllbarkeit impliziert in der erstordentlichen Logik.

Umkehrung

Das Entfernen der Henkin-Zeugen und das Bilden des Redukts kann die expliziten Terme verlieren, die existentielle Aussagen realisieren; umgekehrt übersieht die Gleichsetzung der henkinisierten mit der Ursprungs-Theorie, dass neue Symbole eingeführt wurden, um Zeugen zu sichern.

Abgrenzung

Anwendbar in der erstordentlichen Logik und für Theorien, bei denen man systematisch Zeugen hinzufügen kann; Kardinalitäts- oder Auswahlfragen können die Größe der erweiterten Sprache beeinflussen, verhindern aber die Methode nicht unter den üblichen Annahmen. Liefert nicht automatisch Modelle für wirklich zweistellige oder nicht axiomatisierbare Eigenschaften.

Semantische Spannung

Gegenüber semantischen Existenzbeweisen mittels Kompaktheit oder Ultraprodukten: Die Henkin-Konstruktion ist syntaktisch und explizit, während Kompaktheit/Ultraprodukt-Argumente stärker semantisch sind; es besteht ein Spannungsfeld bezüglich der Vorliebe für syntaktische vs. semantische Methoden.

Synthese

Die Henkin-Konstruktion reduziert die Modellsuche auf eine systematische syntaktische Erweiterung: Zeugen-Konstanten für jede existentielle Formel hinzufügen, zu maximaler Konsistenz erweitern und abgeschlossene Terme interpretieren, wodurch beweisbare Konsistenz mit konkreten Strukturen verknüpft wird.