Gödels Unvollständigkeitssatz ist (nach meinem Verständnis) völlig formal und beruht auf einem Beweissystem, von dem ich annehme, dass es erster Ordnung ist. Macht es für das Theorem einen Unterschied, wenn Logik höherer Ordnung verwendet wird?
Gehe ich richtig in der Annahme, dass dies nicht der Fall ist, weil die Logik erster Ordnung in der Logik höherer Ordnung subsumiert wird?
Vermutlich hat Gödel auch ein Inferenzsystem im Hilbert-Stil verwendet, und es macht keinen Unterschied, ob stattdessen Inferenzsysteme vom Typ natürliche Schlussfolgerung verwendet werden.
Tatsächlich wird Gödels Theorem in der Logik höherer Ordnung ganz natürlich erweitert. Das lange und kurze daran ist, dass, während das Unvollständigkeitstheorem in Bezug auf eine Logik höherer Ordnung gilt, Ihre Intuition, dass es nicht sollte, das Folgende widerspiegelt: dass eine HOL in verschiedene Subsprachen reglementiert werden kann, von denen jede in der Lage ist zu formalisieren die Unvollständigkeit bestimmter Untersprachen von sich aus.
Sei L unsere gegebene Sprache, dann können wir L in eine unendliche Folge von Sprachen L 0 , L 1 , ... , L n ordnen . Jedes L n ist als die Sprache definiert, die sich aus der Erweiterung von L n-1 mit Typ-n-Quantifizierern ergibt, und Typ 0 ist der Typ von Individuen. In jedem L n für n > 0 können wir ein Prädikat Pr n (n) formulieren, das für n genau dann gilt, wenn n die Gödel-Zahl eines in L n beweisbaren Ausdrucks E ist . Wir können auch eine Funktion d n (x) formulieren, die jede Gödel-Zahl p n auf ein Prädikat P n (also einen offenen Satz mit einer freien Variablen "x n-1" vom Typ n-1) auf die Gödelzahl des Ausdrucks P[p/x]. Mit der Gödelzahl von d n ("~Pr n (x)") haben wir einen Ausdruck erreicht, der in L wahr ist n falls es nicht beweisbar ist in L n . Wir können jedoch eine Gödelzahl eines Beweises in L n+1 des Ausdrucks finden, der ~Pr n+1 (d n ("~Pr n
( x)") entspricht arithmetisieren wir den Ausdruck Pr(x), was genau dann gilt, wenn x die Gödelzahl eines in L beweisbaren Ausdrucks ist, befinden wir uns wieder in der bekannten Zwangslage: d("~Pr(x)") ist semantisch wahr, aber nicht beweisbar.
Ihre Annahmen sind diesmal falsch. Gödel verwendete Russells Typentheorie von Principia Mathematica . Daher verwendet Gödel im ursprünglichen Beweis eine Theorie höherer Ordnung (obwohl ich mir nicht sicher bin, ohne einen tiefen Blick darauf zu werfen, wie viel von dem Apparat höherer Ordnung verwendet wird). Tatsächlich lautet der (übersetzte) Titel der Originalarbeit "On Formally Undecidable Propositions of Principia Mathematica and Related Systems" .
Die vollständige Logik zweiter Ordnung ist ebenfalls unvollständig.
Ich glaube, die einzigen Anforderungen an ein System, um Unvollständigkeit zu erhalten, sind die folgenden (mir fehlt möglicherweise etwas):
Sobald diese beiden gelten (modulo meine Sorge, dass ich etwas vergessen könnte), gilt dieses System als unvollständig.
BEARBEITEN:
Meine Aussage, dass dies die einzigen beiden Voraussetzungen sind, halte ich eigentlich für richtig (also waren meine Bedenken fehl am Platz), Gödel formuliert die Bedingungen wie folgt:
Benutzer21820