Berechenbarkeitsgesichtspunkt des Unvollständigkeitssatzes von Gödel/Rosser

Hier werde ich sehr einfache berechenbarkeitsbasierte Beweise des Unvollständigkeitssatzes von Gödel/Rosser vorstellen, die nur grundlegende Kenntnisse über Programme erfordern. Ich habe das Gefühl, dass diese Beweise wenig bekannt sind, obwohl sie eine sehr allgemeine Form der Unvollständigkeitstheoreme geben, und auch leicht rigoros zu machen sind, ohne auch nur auf viel Hintergrundwissen in Logik angewiesen zu sein. Typische Beweise verwenden so etwas wie das Fixkomma-Lemma, das im Wesentlichen ein Fixkomma-Kombinator ist, der auf die Beweisbarkeit „angewendet“ wird, aber das ist ein bisschen schwieriger zu verstehen und rigoros zu beweisen als die Unlösbarkeit des Halteproblems. Es genügt zu sagen, dass alle Beweise auf die eine oder andere Weise diagonalisieren.

Nehmen Sie eine beliebige praktische Programmiersprache L, in der Programme grundlegende Operationen an String-/Integer-Variablen und bedingte Sprünge (oder While-Schleifen) ausführen können. Von nun an sind alle Programme , auf die wir uns beziehen, Programme in L. Der Einfachheit halber werden wir auch jede Zeichenkette als ein Programm betrachten. Wenn es normalerweise kein gültiges Programm ist, betrachten wir es als ein Programm, das einfach eine Endlosschleife ausführt. (Jeder Interpreter für L kann leicht modifiziert werden, um dies zu implementieren.)

Zuerst werde ich zeigen, wie die Unlösbarkeit des Halteproblems im Wesentlichen den (ersten) Unvollständigkeitssatz von Gödel impliziert.

Halteproblem

Definieren Sie das Halteproblem wie folgt:
  Gegeben ein Programm P und Eingabe X:
    Wenn P auf X anhält, dann ist die Antwort "wahr".
    Wenn P nicht auf X anhält, dann ist die Antwort "falsch".

Es ist nicht schwer zu beweisen, dass es kein Programm gibt, das das Halteproblem löst. Damit ein Programm das Halteproblem lösen kann, muss es bei jeder Eingabe (P, X) anhalten und auch die richtige Antwort wie im Problem angegeben ausgeben. Wenn Sie den Beweis noch nicht kennen, versuchen Sie es, bevor Sie sich den Beweis unten ansehen!

Gegeben sei ein beliebiges Programm H:
  Sei C das Programm, das bei der Eingabe P Folgendes ausführt:
    Wenn H(P,P) = "false", dann gib "haha" (und halt) aus, andernfalls Endlosschleife (kein Anhalten).
  Wenn H das Halteproblem löst:
    H(C,C) hält an, und daher hält C(C) genau dann an, wenn H(C,C) = "falsch", nach Definition von C.
    Widerspruch zur Definition von H.
  Daher löst H nicht das Halteproblem.

Schlüsseldefinitionen zu formalen Systemen

Nehmen Sie ein beliebiges formales System T. Wir sagen, V ist ein Beweisverifizierer für T genau dann, wenn alle folgenden Aussagen gelten:
  V ist ein Programm.
  Gegeben irgendein Satz φ über T und Beweis x:
    V(φ,x) entscheidet (hält an und antwortet), ob x ein Beweis von φ ist.
Wir sagen, dass T genau dann über Programme schlussfolgern kann :
  Für jedes Programm P, das an einer Eingabe X anhält und Y ausgibt:
    T kann für jede von Y verschiedene Zeichenkette Z Folgendes beweisen:
      „Das Programm P hält an der Eingabe X an.“
      "Das Programm P hält am Eingang X an und gibt Y aus."
      "Es ist nicht wahr, dass das Programm P am Eingang X anhält und Z ausgibt."
      (Hier werden P, X, Y, Z als verschlüsselte Zeichenfolgen eingefügt, aber Sie sollten die Idee verstehen.)
Wir sagen, dass T genau dann konsistent ist , wenn:
  Es gibt keinen Satz φ über Programme, so dass T sowohl φ als auch seine Negation beweist.
Wir sagen, T ist vollständig genau dann, wenn:
  Für jeden Satz φ über Programme gilt, dass T entweder φ oder seine Negation beweist.
Wir sagen, dass T genau dann korrekt ist, wenn ein Programm anhält,
  wenn T beweist, dass ein Programm bei einer Eingabe anhält, dann hält es wirklich an.

Gödels Unvollständigkeitssatz über das Halteproblem

Nehmen Sie ein beliebiges formales System T mit Beweisverifizierer V, das über Programme schlussfolgern kann.
Sei H das folgende Programm bei Eingabe (P,X):
  Für jeden String s in längenlexikografischer Reihenfolge:
    Wenn V( "Das Programm P hält bei Eingabe X an." , s ) dann Ausgabe "true".
    Wenn V( "Das Programm P wird bei Eingabe X nicht angehalten." , s ) dann "false" ausgeben.
Wenn T vollständig und konsistent ist und für das Anhalten des Programms geeignet ist:
  Gegeben irgendein Programm P und Eingabe X:
    T beweist genau einen der folgenden Sätze:
      A = "Das Programm P hält an der Eingabe X an."
      B = "Das Programm P hält nicht am Eingang X an."
    Somit hält H bei der Eingabe (P,X) an, weil s schließlich ein Beweis von A oder von B sein wird.

      T kann A beweisen, da T über Programme argumentieren kann, und daher H(P,X) = "wahr".
    Wenn P nicht auf X anhält:
      T beweist A nicht durch Korrektheit für das Anhalten des Programms.
      Somit beweist T B und somit H(P,X) = "falsch".
    Daher ist H(P,X) die richtige Antwort darauf, ob P auf X anhält.
  Daher löst H das Halteproblem.
  Widerspruch zur Unlösbarkeit des Halteproblems.
Daher ist T entweder unvollständig oder inkonsistent oder nicht geeignet für das Anhalten des Programms.

Rossers Verstärkung des Gödelschen Unvollständigkeitssatzes

Nachdem Gödels Theorem veröffentlicht wurde, entwickelte Rosser einen Trick, um ihn zu stärken, und ich stieß auf einen Blogbeitrag von Scott Aaronson, der zeigt, dass wir, wenn wir etwas verwenden, das als Zero-Guessing-Problem bezeichnet wird, anstelle des Halteproblems, das bekommen können gleiche Stärkung! Insbesondere können wir dann die Bedingung der Solidität für das Anhalten des Programms fallen lassen. Ich werde eine vereinfachte, in sich geschlossene Version des Zero-Guessing-Problems und den Beweis von Rossers Unvollständigkeitssatz geben, genau parallel dazu, wie die Unlösbarkeit des Halteproblems Gödels Unvollständigkeitssatz impliziert. Wenn Sie eine Herausforderung suchen, können Sie zuerst die Definition des Zero-Guessing-Problems lesen und dann versuchen, den Beweis selbst zu finden, indem Sie den Ideen im früheren Beweis folgen.

Zero-Guessing-Problem

Definieren Sie das Null-Rate-Problem wie folgt:
  Gegeben ein Programm P und Eingabe X:
    Wenn P auf X anhält, dann ist die Antwort 0, wenn P(X) = 0 und andernfalls 1.
    (Wenn P nicht auf X anhält, ist jede Antwort in Ordnung.)

Damit ein Programm das Zero-Guessing-Problem lösen kann, muss es bei jeder Eingabe (P, X) anhalten und auch die richtige Antwort ausgeben, wie im Problem angegeben. Dies impliziert, dass ein Löser beliebigen Unsinn ausgeben darf, wenn P nicht auf X anhält. Wie das Halteproblem kann das Nullratenproblem nicht von einem Programm gelöst werden. Versuchen Sie dies zu beweisen, bevor Sie sich den Beweis unten ansehen!

Gegeben sei ein beliebiges Programm G:
  Sei D das Programm, das bei der Eingabe P Folgendes ausführt:
    Wenn G(P,P) = 0, dann gib 1 aus, sonst gib 0 aus.
  Wenn G das Null-Rate-Problem löst:
    G(D,D) hält an , und daher D(D) ≠ 0 genau dann, wenn G(D,D) = 0, nach Definition von D.
    Widerspruch zur Definition von G.
  Daher löst G das Nullratenproblem nicht.

Beachten Sie, dass die Wahl von 0 und 1 wirklich willkürlich ist. Sie können davon ausgehen, dass 0 und 1 für beliebige feste unterschiedliche Zeichenfolgen stehen, die Sie mögen.

Rossers Unvollständigkeitssatz über das Zero-Guessing-Problem

Nehmen Sie ein beliebiges formales System T mit Beweisverifizierer V, das über Programme schlussfolgern kann.
Sei G das folgende Programm bei Eingabe (P,X):
  Für jeden String s in längenlexikographischer Reihenfolge:
    Wenn V( "Das Programm P stoppt bei Eingabe X und gibt 0 aus." , s ) dann gib 0 aus.
    Wenn V( "Es ist nicht wahr, dass das Programm P bei Eingabe X anhält und 0 ausgibt." , s ) dann Ausgabe 1.
Wenn T vollständig und konsistent ist:
  Gegeben irgendein Programm P und Eingabe X:
    T beweist genau einen der folgenden Sätze:
      A = "Das Programm P hält am Eingang X an und gibt 0 aus."
      B = "Es ist nicht wahr, dass das Programm P am Eingang X und am Ausgang 0 anhält."
    Daher hält G bei der Eingabe (P,X) an, weil s schließlich ein Beweis von A oder von B sein wird.
    Wenn P auf X anhält:
      Erinnere dich daran, dass T die korrekte Ausgabe von P auf X beweisen kann.
      Wenn P(X) = 0, dann kann T A beweisen und somit G(P,X) = 0.
      Wenn P(X) ≠ 0 , dann kann T B beweisen und somit G(P,X) = 1.
  Daher löst G das Zero-Guessing-Problem.
  Widerspruch zur Unlösbarkeit des Zero-Guessing-Problems.
Also ist T entweder nicht vollständig oder nicht konsistent.

Explizit unabhängiger Satz

In den obigen Beweisen haben wir die Unlösbarkeit eines Berechenbarkeitsproblems als Blackbox verwendet, um zu zeigen, dass T unvollständig ist. In beiden Fällen können wir den Unlösbarkeitsbeweis tatsächlich mit dem Unvollständigkeitsbeweis verschmelzen, um explizite Sätze zu erhalten, die unabhängig von T sind, was bedeutet, dass T weder es noch seine Negation beweisen kann.

Sei H das im Beweis des Unvollständigkeitssatzes von Gödel konstruierte Programm.
Sei C das im Beweis konstruierte Programm, dass H das Halteproblem nicht löst.
Sei Q = "Das Programm C hält an der Eingabe C an.".
Sei Q' die Negation von Q.
Wenn T widerspruchsfrei und für das Anhalten von Programmen geeignet ist:
  Wenn C(C) anhält:
    T beweist Q, aber nicht Q', da T über Programme schließen kann.
    Somit ist H(C,C) = "true", und daher hält C(C) nicht an.
    Widerspruch.
  Daher hält C(C) nicht an.
  Somit beweist T Q nicht, da T für das Anhalten des Programms korrekt ist.
  Wenn T Q' beweist:
    H(C,C) = "falsch", und daher hält C(C) an.
    Widerspruch wie oben.

  Somit beweist T weder Q noch Q', sondern Q' ist tatsächlich wahr.

Sei G das im Beweis des Rosserschen Unvollständigkeitssatzes konstruierte Programm.
Sei D das Programm, das im Beweis konstruiert wird, dass G das Zero-Guessing-Problem nicht löst.
Sei W = "Das Programm D hält am Eingang D an und gibt 0 aus.".
Sei W' die Negation von W.
Wenn T konsistent ist:
  Wenn D(D) anhält:
    Erinnere dich daran, dass T über Programme schlussfolgern kann.
    Also beweist T W, wenn D(D) = 0 und T beweist W', wenn D(D) = 1.
    Also G(D,D) = D(D), nach Definition von G.
    Aber D(D) ≠ G( D,D), per Definition von D.
    Widerspruch.
  Daher hält D(D) nicht an.
  Wenn T W oder W' beweist:
    G(D,D) hält an, und daher hält D(D) an.
    Widerspruch wie oben.
  Also beweist T weder W noch W', sondern W' ist tatsächlich wahr.

Aus der Sicht der Berechenbarkeit ist T zwar vollständig für das Anhalten von Programmen (da es über Programme folgern kann), aber für das Nicht-Anhalten von Programmen unvollständig (einige Programme werden bei einigen Eingaben nicht angehalten und T kann diese Tatsache nicht beweisen).

Nullraten versus Anhalten

Beachten Sie, dass wir in den obigen Beweisen auf der Grundlage des Null-Rate-Problems vermeiden, dass T für das Anhalten des Programms gesund sein muss, da es eine schwächere Anforderung als das Anhalteproblem hat, wenn das gegebene Programm P nicht an der gegebenen Eingabe anhält X.

Solidität versus Konsistenz

Es ist üblich anzunehmen, dass T klassisch ist (für Programme), was bedeutet, dass T die Regeln der klassischen Logik verwenden kann, um Sätze über Programme abzuleiten. Aber die obigen Beweise setzen nicht voraus, dass T klassisch ist. Beachten Sie, dass, wenn T klassisch ist (oder zumindest das Explosionsprinzip hat), dann würde die Korrektheit von T für jeden Satz Konsistenz von T implizieren, denn wenn T inkonsistent ist, dann beweist T jeden Satz über Programme. Wenn T klassisch ist, dann ist seine Korrektheit für das Anhalten von Programmen stärker als seine Konsistenz, da es möglich ist (was wir in einem späteren Abschnitt beweisen werden), dass T einen Satz der Form „Das Programm P hält bei Eingabe X“ beweist. und doch hält P in Wirklichkeit nicht am Eingang X an. Beachten Sie auch, dass für klassisches T die Korrektheit von T für das Nichtanhalten von Programmen gleichbedeutend mit der Konsistenz von T ist, denn wenn ein Programm P tatsächlich bei der Eingabe X anhält, kann T diese Tatsache beweisen, und wenn T beweist "The Programm P hält am Eingang X nicht an." dann ist auch T inkonsistent.

Eine weitere Tatsache für klassisches T ist, dass T genau dann konsistent ist, wenn Q' wahr ist. Wir haben bereits gezeigt, dass Q' wahr ist, wenn T konsistent ist. Wenn T widersprüchlich und klassisch ist, dann beweist T nach dem Explosionsprinzip sowohl Q als auch Q', und so hält H(C,C) an, und daher hält C(C) nicht an. Wenn T klassisch ist, dann ist T genau dann konsistent, wenn D(D) nicht anhält.

Um die Behauptung im ersten Absatz zu zeigen, müssen wir ein formales System konstruieren, das klassisch und konsistent ist, aber dennoch für das Anhalten von Programmen ungeeignet ist. Dazu sei S ein formales System, das nur klassisch über endliche binäre Zeichenketten schlussfolgern kann und daher über Programme schlussfolgern kann, weil es über die Ausführung jedes Programms für eine beliebige endliche Anzahl von Schritten schlussfolgern kann. (Wir werden in einem späteren Abschnitt erklären, wie S dies bewerkstelligen kann. Natürlich müssen wir Sätze über Programme in Sätze über endliche binäre Zeichenketten übersetzen, aber es gibt eine natürlich berechenbare Übersetzung.) Wir glauben, dass S für endliche Binärzahlen konsistent und solide ist Saiten und ist daher auch für das Anhalten des Programms geeignet. Wir haben bereits gesehen, dass S weder Q noch Q' beweist, aber Q tatsächlich falsch ist. Sei nun S' S+Q, nämlich dass S' ist das formale System, das jeden Satz beweist, der klassisch aus den Axiomen von S plus Q abgeleitet werden kann. Dann ist S' klassisch und hat einen Beweisverifizierer (Übung für Sie) und ist für das Anhalten des Programms nicht geeignet. Aber S' ist widerspruchsfrei, weil es sonst einen Widerspruchsbeweis über S+Q gibt, der in einen Beweis von Q' über S umgewandelt werden kann. Diese letzte Behauptung ist eine Instanz derAbzugssatz , der für natürliche Deduktion im Fitch-Stil offensichtlich ist .

Gödels ursprünglicher Satz erforderte, dass T ω-konsistent ist , aber sein Beweis erfordert tatsächlich nur, dass T Σ1-stimmig ist . Durch einen Trick von Gödel, der als β-Lemma bezeichnet wird, Σ1-Korrektheit ist im Wesentlichen gleichbedeutend mit Korrektheit für Programm-Anhalten. In diesem genauen Sinne kann man also sagen, dass der schwächere Satz im Wesentlichen äquivalent zu dem Satz ist, der durch Gödels ursprünglichen Beweis gezeigt wird. Tatsächlich wird die Korrektheit des Anhaltens von Programmen für jedes formale System, das wir in der Praxis verwenden, immer als selbstverständlich angesehen, da wir wirklich möchten, dass es keine falschen Sätze über Programme beweist. Aber das stärkere Theorem ist aus der modernen CS-Perspektive schön, da es schwerwiegende grundlegende Einschränkungen in jedem konsistenten formalen System offenbart, das über die endliche Programmausführung nachdenken kann, was in der realen Welt eine sehr konkrete Vorstellung ist!

Kodierung der Programmausführung in einem String

In diesem Abschnitt erklären wir, wie die Programmausführung in einer einzigen endlichen binären Zeichenfolge ausgedrückt werden kann, sodass wir Sätze über diesen Zeichenfolgen verwenden können, um das Programmverhalten, einschließlich des Anhaltens, zu beschreiben. Beachten Sie zunächst, dass Binär keine schwerwiegende Einschränkung darstellt und es viele Möglichkeiten gibt, sie zu umgehen. Der einfachste Weg ist die Verwendung von unären Zahlen (k ist als eine Folge von k Einsen codiert), die durch Nullen getrennt sind, um endliche Folgen von natürlichen Zahlen darzustellen! Diese Darstellung ergibt eine Eins-zu-Eins-Entsprechung zwischen endlicher binärer Zeichenfolge und natürlichen Zeichenfolgen. Beachten Sie als Nächstes, dass wir endliche Folgen natürlicher Zeichenfolgen mit einer einzigen natürlichen Zeichenfolge darstellen können, indem wir jedem Element eins hinzufügen und Nullen als Trennzeichen verwenden. Beispielsweise würde die Folge ((3,1,4),(1),(),(5,9)) durch (4,2,5,0,2,0,0,6,10) dargestellt. Jetzt kann jedes Programm einfach als natürlicher String dargestellt werden. Darüber hinaus kann der gesamte Zustand eines bestimmten Programms, das an einer bestimmten Eingabe ausgeführt wird, durch ein Paar natürlicher Zeichenfolgen erfasst werden, die das Programm und die Eingabe darstellen, wobei der „aktuelle Schritt“ hervorgehoben ist, plus eine Folge von Paaren natürlicher Zeichenfolgen, wobei jedes Paar (x ,v) gibt an, dass die Variable x den Wert v hat. Der gesamte Zustand der Programmausführung kann also durch eine einzige natürliche Zeichenfolge dargestellt werden. Wenn L einfach genug ist, sollten Sie sich vorstellen können, wie man durch einen klassischen Satz über Zeichenketten s,t ausdrücken kann, dass s→t ein gültiger Programmzustandsübergang ist, was bedeutet, dass das Programm nach einem Schritt von Zustand s in Zustand t sein wird . Da eine endliche Folge von Programmzuständen als ein einzelner natürlicher String dargestellt werden kann, können wir durch einen klassischen Satz über Strings p,x,y ausdrücken, dass das Programm p bei Eingabe x anhält und y ausgibt, was im Grunde der Satz ist ( Es gibt eine endliche Folge von Programmzuständen, beginnend mit Programm p mit Eingang x, in dem jedes Paar benachbarter Zustände in dieser Folge ein gültiger Zustandsübergang ist, und endend mit Ausgang y. ). Beachten Sie schließlich, dass, wenn ein Programm p wirklich bei der Eingabe x anhält, jedes formale System S, das über natürliche Zeichenfolgen schlussfolgern kann, jeden Schritt der Ausführung von p auf x beweisen kann und dann alle diese Beweise aneinanderreihen kann, um die Tatsache des Anhaltens zu beweisen .

Im letzten Teil des obigen Absatzes haben wir leicht an unsere Intuition appelliert, dass wir die angemessene Übersetzung dieses Satzes in jeder denkbaren praktischen Programmiersprache vornehmen können. Es ist nicht wirklich erhellend, dies vollständig zu formalisieren, aber es könnte auf viele Arten geschehen. Eine Möglichkeit besteht darin, dies nur für eine bestimmte universelle Variante von Turing-Maschinen zu tun. Eine andere besteht darin, dies nur für eine bestimmte Assembler-ähnliche Sprache zu tun. Eine dritte besteht darin, dies für eine Variante des Lambda-Kalküls zu tun. Was auch immer es ist, es muss Turing-Maschinen entsprechen. Dieses Problem ist dieser Version des Unvollständigkeitssatzes nicht eigen, da der ursprüngliche Satz Systeme betrifft, die über grundlegende Arithmetik schlussfolgern können, was sich aufgrund von Gödels β-Lemma als äquivalent herausstellt. Der Grund Gödel' s Satz von Arithmetik handelte, scheint darauf zurückzuführen zu sein, dass die damaligen Mathematiker dies für grundlegend für die Mathematik hielten. Der Hauptvorteil des Beweises meiner Version des Satzes besteht darin, dass er die Zahlentheorie in Gödels β-Lemma und das Konzept der primitiven Rekursion vermeidet und zeigt, dass nur grundlegende Tatsachen der Stringverkettung (nicht einmal irgendeine Form der Induktion) für die ausreichen Unvollständigkeitsphänomen entstehen und erfordert nicht, dass das formale System auf klassischer Logik basiert.

Beliebte Missverständnisse über Unvollständigkeit

Wenn Menschen zum ersten Mal auf die Aussage über die Unvollständigkeit der Peano-Arithmetik (PA) stoßen, vermuten viele fälschlicherweise verschiedene Aspekte der PA als „Ursache“.

Es ist nicht auf Induktion zurückzuführen, noch nicht einmal auf die unendliche Anzahl von Axiomen von PA. Der Grund ist, dass PA− genug ist und PA− endlich viele Axiome hat. PA− plus Induktion ergibt PA. In ähnlicher Weise hat die hier beschriebene Theorie der Verkettung (TC) , die ein einfacher Kandidat für das obige formale System S ist, das lediglich über endliche binäre Zeichenfolgen schlussfolgern kann, nur endlich viele Axiome.

Es ist nicht auf irgendein tiefes zahlentheoretisches Phänomen zurückzuführen. Ich selbst dachte fälschlicherweise, dass dies der Fall sei, weil die Presburger-Arithmetik konsistent und vollständig ist, bis ich den berechenbaren Beweis oben sah, der für TC gilt, da TC über Programme argumentieren kann. Es ist wahr, dass TC in gewissem Sinne äquivalent zu PA− ist, aber TC hat nichts als Verkettung, und die Axiome von TC sind nur ein paar „offensichtliche“ Tatsachen über Strings.

Das liegt nicht an der klassischen Logik. Dies ist eine gängige 'Kritik' an den Unvollständigkeitssätzen, aber völlig unbegründet. Wie im obigen Beweis gezeigt, gilt es für jedes formale System, das einen Beweisverifizierer hat und über Programme nachdenken kann, unabhängig davon, ob es klassisch ist oder nicht. Beachten Sie, dass ich nirgendwo etwas über syntaktische oder deduktive Regeln gesagt habe, weil es keine geben muss. Das formale System T könnte sogar so verrückt sein, dass, wenn uns ein beliebiges Programm gegeben wird, das bei irgendeiner Eingabe anhält, der einfachste Weg, einen Beweis für diese Tatsache φ über T zu finden, darin besteht, V(φ,x) für jede mögliche Zeichenkette x laufen zu lassen bis Sie eine finden, von der V sagt, dass sie gültig ist! Betrachten Sie für ein triviales, aber relevantes Beispiel das formale System R (für "Läufer"), dessen Beweisverifizierer die folgende gegebene Eingabe (φ,k) macht: Es prüft zuerst, ob φ die Form " (wobei die Sätze in eckigen Klammern optional sind) und führt dann P auf X für Schritte der Länge (k) aus und antwortet dann, dass der Beweis gültig ist, wenn P angehalten hat [und seine Ausgabe wie behauptet ist], und antwortet, dass der Beweis ist in allen anderen Fällen ungültig. Sie sehen, dass R tatsächlich bei jeder Eingabe (φ,k) anhält und nur dann die Gültigkeit des sogenannten Beweises bestätigt, wenn φ tatsächlich wahr und k lang genug ist. Sie können auch sehen, dass R die Gültigkeit eines Beweises nicht bestätigt, wenn φ eine andere Form hat oder P nicht anhält. Somit erfüllt R die Anforderungen des obigen Unvollständigkeitssatzes. Wenn Sie möchten, können Sie R * den Abschluss von R unter intuitionistischer Deduktion sein lassen, und dann wäre R * ein intuitionistisches nicht-klassisches Beispiel. (wobei die Sätze in eckigen Klammern optional sind) und führt dann P auf X für Schritte der Länge (k) aus und antwortet dann, dass der Beweis gültig ist, wenn P angehalten hat [und seine Ausgabe wie behauptet ist], und antwortet, dass der Beweis ist in allen anderen Fällen ungültig. Sie sehen, dass R tatsächlich bei jeder Eingabe (φ,k) anhält und nur dann die Gültigkeit des sogenannten Beweises bestätigt, wenn φ tatsächlich wahr und k lang genug ist. Sie können auch sehen, dass R die Gültigkeit eines Beweises nicht bestätigt, wenn φ eine andere Form hat oder P nicht anhält. Somit erfüllt R die Anforderungen des obigen Unvollständigkeitssatzes. Wenn Sie möchten, können Sie R * den Abschluss von R unter intuitionistischer Deduktion sein lassen, und dann wäre R * ein intuitionistisches nicht-klassisches Beispiel. und antwortet dann, dass der Beweis gültig ist, wenn P angehalten hat [und seine Ausgabe wie behauptet ist], und antwortet, dass der Beweis in allen anderen Fällen ungültig ist. Sie sehen, dass R tatsächlich bei jeder Eingabe (φ,k) anhält und nur dann die Gültigkeit des sogenannten Beweises bestätigt, wenn φ tatsächlich wahr und k lang genug ist. Sie können auch sehen, dass R die Gültigkeit eines Beweises nicht bestätigt, wenn φ eine andere Form hat oder P nicht anhält. Somit erfüllt R die Anforderungen des obigen Unvollständigkeitssatzes. Wenn Sie möchten, können Sie R * den Abschluss von R unter intuitionistischer Deduktion sein lassen, und dann wäre R * ein intuitionistisches nicht-klassisches Beispiel. und antwortet dann, dass der Beweis gültig ist, wenn P angehalten hat [und seine Ausgabe wie behauptet ist], und antwortet, dass der Beweis in allen anderen Fällen ungültig ist. Sie sehen, dass R tatsächlich bei jeder Eingabe (φ,k) anhält und nur dann die Gültigkeit des sogenannten Beweises bestätigt, wenn φ tatsächlich wahr und k lang genug ist. Sie können auch sehen, dass R die Gültigkeit eines Beweises nicht bestätigt, wenn φ eine andere Form hat oder P nicht anhält. Somit erfüllt R die Anforderungen des obigen Unvollständigkeitssatzes. Wenn Sie möchten, können Sie R * den Abschluss von R unter intuitionistischer Deduktion sein lassen, und dann wäre R * ein intuitionistisches nicht-klassisches Beispiel. Sie können auch sehen, dass R die Gültigkeit eines Beweises nicht bestätigt, wenn φ eine andere Form hat oder P nicht anhält. Somit erfüllt R die Anforderungen des obigen Unvollständigkeitssatzes. Wenn Sie möchten, können Sie R * den Abschluss von R unter intuitionistischer Deduktion sein lassen, und dann wäre R * ein intuitionistisches nicht-klassisches Beispiel. Sie können auch sehen, dass R die Gültigkeit eines Beweises nicht bestätigt, wenn φ eine andere Form hat oder P nicht anhält. Somit erfüllt R die Anforderungen des obigen Unvollständigkeitssatzes. Wenn Sie möchten, können Sie R * den Abschluss von R unter intuitionistischer Deduktion sein lassen, und dann wäre R * ein intuitionistisches nicht-klassisches Beispiel.

Meiner Meinung nach ist das Phänomen, das tatsächlich für die Unvollständigkeit „verantwortlich“ ist, die Fähigkeit, über Programme nachzudenken. Jemand hat einmal gesagt, Gödels Beweis sei im Grunde so, als würde man einen Compiler in Arithmetik konstruieren, nur damit er primitive rekursive Programme ausführen kann (solche, die nur for-Schleifen verwenden, deren Zähler innerhalb der Schleife nicht geändert werden können).

Schließlich kann das grundlegende System, das zum Beweis der Unvollständigkeitssätze benötigt wird, sehr schwach sein. Eine Schlüsselannahme ist, dass das Programmverhalten wohldefiniert ist, nämlich dass bei einem beliebigen Programm P und einer Eingabe X entweder P anhält oder P nicht anhält und die Ausgabe, falls vorhanden, eindeutig ist. Diese Annahme ist notwendig, da ansonsten sogar die Konzepte der Konsistenz und Vollständigkeit nicht genau definiert sind. Kurz gesagt, es genügt, klassische Logik für das Programmverhalten zu haben. Da das Programmverhalten als Satz über Strings kodiert werden kann (wie im vorigen Abschnitt), impliziert dies, dass wir gewissermaßen nur klassische Logik für Strings annehmen müssen, um die Unvollständigkeitssätze in kodierter Form beweisen zu können. Wenn Sie es in einer natürlicheren Form beweisen möchten, benötigen Sie das grundlegende System, um die Argumentation über endliche Sequenzen nativ zu unterstützen.

Verallgemeinerung

Wir können die Unvollständigkeitssätze vollständig verallgemeinern, indem wir die Bedingung lockern, dass das formale System T einen Beweisverifizierer V hat, der immer anhält. Es genügt zu fordern, dass V(φ,x) genau dann „ja“ ausgibt, wenn x ein Beweis von φ ist, und es spielt keine Rolle, ob V nicht anhält, wenn x kein Beweis von φ ist! Der Beweis ist derselbe, außer dass Sie einfach das Programm konstruieren müssen, um alle Aufrufe von V zu parallelisieren. In jeder vernünftigen Programmiersprache kann dies wie folgt durchgeführt werden. Jeder Aufruf von V löst eine Schritt-für-Schritt-Simulation der Ausführung von V an den gegebenen Eingaben parallel zum Rest des Programms aus, sodass es jederzeit mehrere (aber endlich viele) fortlaufende Simulationen geben kann. Wenn eine Simulation das Ende erreicht, wird das gesamte Programm beendet und die Ausgabe in dieser Simulation wird als Ausgabe des gesamten Programms zurückgegeben.

Beachten Sie auch, dass diese vollständige Verallgemeinerung gleichbedeutend ist mit dem Ersetzen des Kriteriums, dass T einen Beweisverifizierer hat, durch das Kriterium, dass T einen Theoremgenerator M hat, der ein Programm ist, das ewig läuft und schließlich jeden Theorem von T ausgibt und keinen String ausgibt kein Satz von T. Dann muss das Programm im Beweis nur M simulieren und warten, bis M A oder B erzeugt, und dann das gesamte Programm beenden und entsprechend ausgeben. In den obigen Beweisen habe ich nicht die vollständige Verallgemeinerung verwendet, weil es nicht offensichtlich ist, welche Programmiersprachen stark genug sind, dass Programme in ihnen andere Programme simulieren können, und alle praktischen formalen Systeme sowieso einen Beweisverifizierer haben.

Verallgemeinerung auf unberechenbare formale Systeme

Ein schöner Aspekt dieser auf Berechenbarkeit basierenden Sichtweise ist, dass sie sich automatisch auf jede Art von Klasse Ω von Orakelprogrammen relativiert. Insbesondere liefert derselbe Beweis die Unvollständigkeitssätze für formale Systeme, deren Beweisüberprüfer ein Programm in Ω ist und die über Programme in Ω schließen können. Dieses Ergebnis kann verwendet werden, um zu beweisen, dass die arithmetische Hierarchie auf keiner Ebene zusammenbricht, wie in diesem Beitrag gezeigt .

Weiterlesen

Der Blogbeitrag von Scott Aaronson, der einiges davon inspirierte , zitierte Kleenes Mathematical Logic-Text von 1967 für einen ähnlichen Beweis von Rossers Theorem (Theorem VIII und Corollary I auf den Seiten 286-288).

Eine Arbeit von Emil Post aus dem Jahr 1944, in der ein Beweis skizziert wird, der dem obigen Beweis lose entspricht, über das Halteproblem für formale Systeme, die für das Anhalten von Programmen geeignet sind. (Danke Philipp Weiß!)

Eine formale Version des obigen Beweises des Satzes von Rosser für formale Systeme, die PA− interpretieren .

Eine Diskussion grundlegender Fragen bezüglich des Halteproblems und des Unvollständigkeitssatzes .

Eine Erklärung des Festkommakombinators im λ-Kalkül, der im einleitenden Absatz erwähnt wurde .