Der Vollständigkeitslehrsatz von Gödel ist ein Hauptsatz in der mathematischen Logik, die eine Ähnlichkeit zwischen semantischer Wahrheit und syntaktischem provability in der Logik der ersten Ordnung gründet. Es wurde zuerst von Kurt Gödel 1929 bewiesen.

Eine Formel der ersten Ordnung wird logisch gültig genannt, wenn es in jeder Struktur für seine Sprache wahr ist. Der Vollständigkeitslehrsatz zeigt, dass, wenn eine Formel dann logisch gültig ist, es einen begrenzten Abzug (ein formeller Beweis) der Formel gibt. Der Abzug ist ein begrenzter Gegenstand, der mit der Hand oder Computer nachgeprüft werden kann. Diese Beziehung zwischen Wahrheit und provability gründet eine nahe Verbindung zwischen der Mustertheorie und Probetheorie in der mathematischen Logik.

Eine wichtige Folge des Vollständigkeitslehrsatzes ist, dass es möglich ist, die logischen Folgen jeder wirksamen Theorie der ersten Ordnung, durch das Aufzählen aller richtigen Abzüge mit Axiomen aus der Theorie aufzuzählen.

Der Unvollständigkeitslehrsatz von Gödel, sich auf eine verschiedene Bedeutung der Vollständigkeit beziehend, zeigt, dass, wenn eine genug starke wirksame Theorie der Arithmetik dann entspricht, es eine Formel gibt (abhängig von Theorie), der weder bewiesen werden kann noch disproven innerhalb der Theorie. Dennoch gilt der Vollständigkeitslehrsatz für diese Theorien, zeigend, dass jede logische Folge solch einer Theorie aus der Theorie nachweisbar ist.

Hintergrund

Es gibt zahlreiche deduktive Systeme für die Logik der ersten Ordnung, einschließlich Systeme des natürlichen Abzugs und Hilbert-artiger Systeme. Üblich für alle deduktiven Systeme ist der Begriff eines formellen Abzugs. Das ist eine Folge (oder, in einigen Fällen, ein begrenzter Baum) Formeln mit einem besonders benannten Beschluss. Die Definition eines Abzugs ist solch, dass es begrenzt ist, und dass es möglich ist, algorithmisch nachzuprüfen (durch einen Computer, zum Beispiel, oder mit der Hand), dass eine gegebene Sammlung von Formeln tatsächlich ein Abzug ist.

Eine Formel ist logisch gültig, wenn es in jeder Struktur für die Sprache der Formel wahr ist. Um formell festzusetzen, und sich dann, der Vollständigkeitslehrsatz zu erweisen, ist es notwendig, auch ein deduktives System zu definieren. Ein deduktives System wird abgeschlossen genannt, wenn jede logisch gültige Formel der Beschluss von etwas formellem Abzug ist, und der Vollständigkeitslehrsatz für ein besonderes deduktives System der Lehrsatz ist, dass es in diesem Sinn abgeschlossen ist. So, gewissermaßen, gibt es einen verschiedenen Vollständigkeitslehrsatz für jedes deduktive System.

Behauptung und Folgen

Der Vollständigkeitslehrsatz von Gödel sagt, dass ein deduktives System der Prädikat-Rechnung der ersten Ordnung im Sinn "abgeschlossen" ist, dass keine zusätzlichen Interferenzregeln erforderlich sind, alle logisch gültigen Formeln zu beweisen. Ein gegenteiliger zur Vollständigkeit ist Stichhaltigkeit, die Tatsache, dass nur logisch gültige Formeln im deduktiven System nachweisbar sind. Genommen zusammen deuten diese Lehrsätze an, dass eine Formel logisch gültig ist, wenn, und nur wenn es der Beschluss eines formellen Abzugs ist.

Eine allgemeinere Version des Vollständigkeitslehrsatzes von Gödel hält. Es sagt, dass für jede Theorie T der ersten Ordnung und jeden Satz S auf der Sprache der Theorie es einen formellen Abzug von S von T gibt, wenn, und nur wenn S durch jedes Modell von T zufrieden ist. Dieser allgemeinere Lehrsatz wird implizit zum Beispiel verwendet, wenn, wie man zeigt, ein Satz von den Axiomen der Gruppentheorie durch das Betrachten einer willkürlichen Gruppe und die Vertretung nachweisbar ist, dass der Satz von dieser Gruppe zufrieden ist.

Der Zweig der mathematischen Logik, die sich damit befasst, was in verschiedenen Modellen wahr ist, wird Mustertheorie genannt. Der Zweig hat Probetheorie-Studien genannt, was in besonderen formellen Systemen formell bewiesen werden kann. Der Vollständigkeitslehrsatz stellt eine grundsätzliche Verbindung zwischen diesen zwei Zweigen her, eine Verbindung zwischen der Semantik und Syntax gebend. Der Vollständigkeitslehrsatz sollte jedoch als das Auswischen des Unterschieds zwischen diesen zwei Konzepten nicht missdeutet werden; tatsächlich zeigt der Unvollständigkeitslehrsatz von Gödel, ein anderes berühmtes Ergebnis, dass es innewohnende Beschränkungen darin gibt, was mit formellen Beweisen in der Mathematik erreicht werden kann. Der Name für den Unvollständigkeitslehrsatz bezieht sich auf eine andere Bedeutung von ganzen (sieh Mustertheorie - das Verwenden der Kompaktheits- und Vollständigkeitslehrsätze). Insbesondere der Vollständigkeitslehrsatz von Gödel befasst sich mit Formeln, die logische Folgen einer Theorie der ersten Ordnung sind, während der Unvollständigkeitslehrsatz Formeln baut, die nicht logische Folgen von bestimmten Theorien sind.

Eine wichtige Folge des Vollständigkeitslehrsatzes ist, dass der Satz von logischen Folgen einer wirksamen Theorie der ersten Ordnung ein Enumerable-Satz ist. Die Definition der logischen Folge misst über alle Strukturen auf einer besonderen Sprache, und gibt so keine unmittelbare Methode, um algorithmisch zu prüfen, ob eine Formel logisch gültig ist. Außerdem ist eine Folge des Unvollständigkeitslehrsatzes von Gödel, dass der Satz von logisch gültigen Formeln nicht entscheidbar ist. Aber der Vollständigkeitslehrsatz deutet an, dass der Satz von Folgen einer wirksamen Theorie enumerable ist; der Algorithmus soll zuerst eine Enumeration aller formellen Abzüge aus der Theorie bauen, und das verwenden, um eine Enumeration ihrer Beschlüsse zu erzeugen. Der finitary, die syntaktische Natur von formellen Abzügen macht es möglich, sie aufzuzählen.

Beziehung zum Kompaktheitslehrsatz

Der Vollständigkeitslehrsatz und der Kompaktheitslehrsatz sind zwei Ecksteine der Logik der ersten Ordnung. Während keiner dieser Lehrsätze auf eine völlig wirksame Weise bewiesen werden kann, kann jeder beim anderen effektiv erhalten werden.

Der Kompaktheitslehrsatz sagt, dass, wenn eine Formel φ eine logische Folge (vielleicht unendlich) Satz von Formeln Γ dann ist, es eine logische Folge einer begrenzten Teilmenge von Γ ist. Das ist eine unmittelbare Folge des Vollständigkeitslehrsatzes, weil nur eine begrenzte Zahl von Axiomen von Γ in einem formellen Abzug von φ erwähnt werden kann, und die Stichhaltigkeit des Abzug-Systems dann andeutet, dass φ eine logische Folge dieses begrenzten Satzes ist. Dieser Beweis des Kompaktheitslehrsatzes ist ursprünglich wegen Gödel.

Umgekehrt, für viele deduktive Systeme, ist es möglich, den Vollständigkeitslehrsatz als eine wirksame Folge des Kompaktheitslehrsatzes zu beweisen.

Die Unwirksamkeit des Vollständigkeitslehrsatzes kann entlang den Linien der Rückmathematik gemessen werden. Wenn betrachtet, über eine zählbare Sprache sind die Vollständigkeits- und Kompaktheitslehrsätze zu einander gleichwertig und zu einer schwachen Form der Wahl gleichwertig, die als das Lemma des schwachen Königs mit der Gleichwertigkeit bekannt ist, die in RCA (eine Variante der zweiten Ordnung der Arithmetik von Peano nachweisbar ist, die auf die Induktion über Σ Formeln eingeschränkt ist). Das Lemma des schwachen Königs ist in ZF, dem System der Zermelo-Fraenkel Mengenlehre ohne Axiom der Wahl nachweisbar, und so sind die Vollständigkeits- und Kompaktheitslehrsätze für zählbare Sprachen in ZF nachweisbar. Jedoch ist die Situation verschieden, wenn die Sprache willkürlichen großen cardinality seitdem ist, obwohl die Vollständigkeits- und Kompaktheitslehrsätze nachweisbar gleichwertig zu einander in ZF bleiben, sind sie auch zu einer schwachen Form des Axioms der als das Ultrafilterlemma bekannten Wahl nachweisbar gleichwertig. Insbesondere keine Theorie, die ZF erweitert, kann entweder die Vollständigkeits- oder Kompaktheitslehrsätze über den willkürlichen (vielleicht unzählbar) Sprachen beweisen, ohne auch das Ultrafilterlemma auf einer Reihe derselben cardinality zu beweisen, wissend, dass auf zählbaren Sätzen das Ultrafilterlemma gleichwertig zum Lemma des schwachen Königs wird. Außerdem, obwohl jede konsequente, zählbare Theorie der ersten Ordnung ein begrenztes oder zählbares Modell hat (demzufolge des Vollständigkeitslehrsatzes und des Löwenheim-Skolem Lehrsatzes), ist es bekannt, dass es wirksame konsequente Theorien der ersten Ordnung gibt, die berechenbare Modelle nicht haben.

Vollständigkeit in anderer Logik

Der Vollständigkeitslehrsatz ist ein Haupteigentum der Logik der ersten Ordnung, die für die ganze Logik nicht hält. Logik der zweiten Ordnung hat zum Beispiel keinen Vollständigkeitslehrsatz für seine Standardsemantik (aber hat wirklich das Vollständigkeitseigentum für die Semantik von Henkin), und dasselbe trifft auf die ganze höherwertige Logik zu. Es ist möglich, gesunde deduktive Systeme für die höherwertige Logik zu erzeugen, aber kein solches System kann abgeschlossen sein. Der Satz von logisch gültigen Formeln in der Logik der zweiten Ordnung ist nicht enumerable.

Der Lehrsatz von Lindström stellt fest, dass Logik der ersten Ordnung (Thema bestimmten Einschränkungen) Logik am stärksten ist, die sowohl Kompaktheit als auch Vollständigkeit befriedigt.

Ein Vollständigkeitslehrsatz kann für die modale Logik oder intuitionistic Logik in Bezug auf die Semantik von Kripke bewiesen werden.

Beweise

Der ursprüngliche Beweis von Gödel des Lehrsatzes ist durch das Reduzieren des Problems auf einen speziellen Fall für Formeln in einer bestimmten syntaktischen Form, und dann das Berühren dieser Form mit einem Ad-Hoc-Argument weitergegangen.

In modernen Logiktexten wird der Vollständigkeitslehrsatz von Gödel gewöhnlich mit dem Beweis von Henkin, aber nicht mit dem ursprünglichen Beweis von Gödel bewiesen. Der Beweis von Henkin baut direkt ein Begriff-Modell für jede konsequente Theorie der ersten Ordnung. James Margetson (2004) hat einen computerisierten formellen Beweis mit dem Lehrsatz von Isabelle prover entwickelt. http://afp.sourceforge.net/entries/Completeness-paper.pdf sind Andere Beweise auch bekannt.

Siehe auch

• Die Unvollständigkeitslehrsätze von Gödel
• Ursprünglicher Beweis des Vollständigkeitslehrsatzes von Gödel

Weiterführende Literatur

• Der erste Beweis des Vollständigkeitslehrsatzes.

• Dasselbe Material wie die Doktorarbeit, außer mit kürzeren Beweisen, mehr kurz gefassten Erklärungen und dem Auslassen der langen Einführung.

Links

• Enzyklopädie von Stanford der Philosophie: "Kurt Gödel" - durch Juliette Kennedy.
• Lebensbeschreibung von MacTutor: Kurt Gödel.
• Detlovs, Vilnis, und Podnieks, Karlis, "Einführung in die mathematische Logik."