## [Henkin-Konstruktion](/de/node/61032) Definition 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 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 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 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 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 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 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 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 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.