Woher wissen wir, dass wir nicht versehentlich von Nicht-Standard-Ganzzahlen sprechen?

[Ich gehe in dieser Antwort davon aus, dass die Standard-Ganzzahlen in einem gewissen platonischen Sinne "existieren", da mir sonst nicht klar ist, dass Ihre Frage überhaupt sinnvoll ist.]

Du denkst ganz falsch darüber nach. Glauben Sie, dass die Axiome von PA für die Standard-Ganzzahlen wahr sind? Dann sollten Sie auch glauben, dass alles, was Sie von PA beweisen, auch für die Standard-Ganzzahlen gilt. Insbesondere wenn Sie beweisen, dass es eine Ganzzahl mit einer Eigenschaft gibt, ist diese Existenzaussage in den Standard-Ganzzahlen wahr.

Anders ausgedrückt, alles, was Sie anhand Ihrer Axiome beweisen, ist in jedem Modell der Axiome, Standard oder Nichtstandard, wahr. Die Existenz von Nichtstandardmodellen ist also völlig irrelevant. Relevant ist nur, ob das Standardmodell existiert (mit anderen Worten, ob Ihre Axiome für die Standard-Ganzzahlen gelten).

Nun sollte ich darauf hinweisen, dass diese Vorstellung für etwas wie ZFC viel schlüpfriger ist als für etwas wie PA. Aus philosophischer Sicht ist die Idee, dass es tatsächlich ein platonisches "standardmäßiges mengentheoretisches Universum" gibt, das ZFC richtig beschreibt, viel weniger kohärent als die entsprechende Aussage für ganze Zahlen. Soweit wir wissen, ist ZFC möglicherweise tatsächlich inkonsistent und beweist daher alle möglichen falschen Aussagen über die ganzen Zahlen. Oder vielleicht ist es konsistent, aber es beweist immer noch falsche Aussagen über die ganzen Zahlen (weil es nur Nicht-Standard-Modelle hat). Aber wenn Sie glauben, dass die ZFC-Axiome in ihrer beabsichtigten Interpretation wahr sind, dann sollten Sie glauben, dass alle Konsequenzen daraus auch wahr sind (einschließlich Konsequenzen für die ganzen Zahlen).

Um über "Standard"-Ganzzahlen zu sprechen, muss jemand bereits eine Sammlung von "Ganzzahlen" haben, von denen er glaubt, dass sie die "Standardzahlen" sind. Natürlich wissen sie möglicherweise nicht alles über diese Ganzzahlen, aber sie müssen daran denken, dass es eine bestimmte Sammlung von Objekten gibt, die die "Standard-Ganzzahlen" sind. Ebenso könnte jemand eine Sammlung von Objekten haben, von denen er glaubt, dass sie das "Standard" -Modell der Mengenlehre sind.

Wir verwenden den Begriff Ton in Bezug auf eine Reihe von Axiomen, um zu bedeuten, dass die Axiome in unserem bevorzugten „Standardmodell“ (wie im vorherigen Absatz) wahr sind. Dies ist eine andere Bedeutung von Korrektheit als im Korrektheitssatz für die Logik erster Ordnung.

Zum Beispiel werden die Axiome der Peano-Arithmetik (PA) normalerweise als solide in Bezug auf die natürlichen Standardzahlen angesehen, und die Axiome der ZFC werden als solide in Bezug auf das Standardmodell der Mengenlehre angesehen. Das ist die grundlegende Antwort auf die Frage: Wenn wir beweisen, dass eine Turing-Maschine mit einer soliden Theorie anhält, dann hält die Turing-Maschine tatsächlich an, weil per Definition jede Aussage, die in einer soliden Theorie beweisbar ist, über das entsprechende Standardmodell wahr ist.

Wir könnten weiter vordringen und fragen: Wie können wir diese Solidität beweisen ? Eine Möglichkeit ist ein direkter, informeller Appell an die Intuition. Eine andere Möglichkeit besteht darin, die Solidität eines Axiomensystems in einem anderen formalen Axiomensystem zu beweisen – einer Metatheorie.

Dies führt zu einer ähnlichen Situation wie das bekannte Problem, die Konsistenz eines grundlegenden Axiomensystems zu beweisen. Gödels Unvollständigkeitssätze zeigen, dass unsere wichtigsten grundlegenden Theorien ihre eigene Konsistenz nicht beweisen können. Ebenso können diese Theorien ihre eigene Stichhaltigkeit nicht beweisen (nicht einmal ausdrücken). Wenn wir jedoch von einer ausreichend starken Metatheorie ausgehen, können wir die Metatheorie verwenden, um die Stichhaltigkeit einer grundlegenden Theorie zu beweisen .

Zum Beispiel beweist ZFC, dass die Peano-Arithmetik solide ist, und die Morse-Kelley-Mengentheorie beweist, dass die ZFC-Mengentheorie solide ist. Die Herausforderung besteht hier, wie auch bei der Konsistenz, darin, dass es eine Art Rückschritt gibt. Um zu beweisen, dass die Morse-Kelley-Mengentheorie solide ist, müssten wir eine noch stärkere Metatheorie annehmen, und um zu beweisen, dass sie solide ist, müssen wir eine noch stärkere als diese annehmen.

Dann wird die Option „Direkter Appell an die Intuition“ attraktiver. Genauso wie wir glauben könnten, dass die Axiome der Euklidischen Geometrie für die Ebene wahr sind$\mathbb{R}^2$ohne dies in einer bestimmten Metatheorie zu beweisen, könnten wir im Prinzip glauben, dass PA und ZFC gesund sind, ohne uns Gedanken darüber zu machen, in welcher Metatheorie die Solidität bewiesen werden kann. Dies würde davon abhängen, dass wir glauben, dass die Axiome dieser formalen Systeme alle wahre Aussagen über unsere sind bevorzugte "Standard"-Modelle.

Wir wissen, dass jedes formale System die natürlichen Zahlen nicht vollständig festlegen kann.

Genau das habe ich übrigens hier gesagt . Abgesehen von dem, was ich in diesem Beitrag gesagt habe, möchte ich auf die folgenden Punkte näher eingehen:

• Eine verallgemeinerte Version des Gödel-Rosser-Unvollständigkeitssatzes zeigt überzeugend, dass es kein praktisches formales System gibt, das die natürlichen Zahlen festschreiben kann. Insbesondere können wir leicht ein Programm schreiben, das bei einem gegebenen Proof-Verifier-Programm für ein formales System, das Arithmetik interpretiert, einen expliziten arithmetischen Satz erzeugt, der von diesem System weder bewiesen noch widerlegt werden kann. Wie überzeugend? Wenn wir den Unvollständigkeitssatz auf eine bestimmte Weise formulieren, kann er sogar in der intuitionistischen Logik bewiesen werden. Aber wir müssen immer noch in einem Metasystem arbeiten, das Zugang zu einem PA-Modell oder Äquivalent hat, sonst können wir nicht einmal über endliche Zeichenfolgen sprechen, die die Grundbausteine ​​​​jedes praktischen formalen Systems sind.

• Das philosophische Problem ist, dass die empirischen Beweise in Bezug auf die reale Welt darauf hindeuten, dass es kein reales Modell der PA gibt, was teilweise auf die endliche Größe des beobachtbaren Universums, aber auch auf die Tatsache zurückzuführen ist, dass es sich um ein physisches Speichergerät handelt mit extrem großer Kapazität (in der Größenordnung des beobachtbaren Universums) wird schneller abgebaut, als Sie es nutzen können! Es gibt also ein seltsames philosophisches Problem mit dem vorhergehenden Punkt, denn wenn man nicht glaubt, dass sich die Sammlung endlicher Strings in die reale Welt einbettet, dann gelten die Unvollständigkeitstheoreme nicht wirklich ...

• Andererseits gibt es unbestreitbar große empirische Beweise dafür, dass die Theoreme von PA, wenn sie in Aussagen über reale Programme übersetzt werden, auf menschlicher Ebene korrekt sind. Nur zum Beispiel gibt es kein bekanntes Gegenbeispiel zu den Sätzen, die der RSA-Entschlüsselung zugrunde liegen, die auf dem kleinen Satz von Fermat und anderen grundlegenden zahlentheoretischen Sätzen beruhen, die auf natürliche Zahlen in der Größenordnung von angewendet werden$2^{2048}$. Man muss also immer noch die unglaubliche Genauigkeit von PA im kleinen Maßstab erklären, auch wenn es kein reales Modell geben kann.

Aber wenn wir den philosophischen Unglauben aufheben und in einem schwachen formalen System namens ACA arbeiten, das praktisch jeder Logiker für solide hält (in Bezug auf die reale Welt), gibt es viele Dinge, die wir tatsächlich mit Sicherheit sagen können (abgesehen vom Unvollständigkeitssatz). Beantworten Sie Ihre Frage (wenn ACA gesund ist).

Angenommen, das gilt für eine bestimmte Turing-Maschine$Z$, das habe ich bewiesen$Z$stoppt [nach einer Zahl$N$von Schritten. Wie kann ich das sicher wissen?$N$ist eine normale natürliche Zahl und keine nicht standardmäßige?

Ihr Beweis wird innerhalb eines formalen Systems durchgeführt$S$. Wenn$S$Ist$Σ_1$-Sound (in Bezug auf die reale Welt), dann können Sie das sicher wissen$Z$hält wirklich an. Das ist durchaus möglich$S$ist nicht$Σ_1$-Sound, und dass Sie es nie herausfinden können. Zum Beispiel bei jedem praktischen formalen System$S$die Arithmetik interpretiert, let$S' = S + \neg \text{Con}(S)$. Wenn$S$ist dann konsequent$S'$ist aber auch konsequent$Σ_1$-ungesund. Insbesondere weist es nach, dass der Proof-Verifizierer z$S$hält an einem angeblichen Widerspruchsbeweis vorbei$S$, das ist genau die Art von Frage, die Sie beschäftigt!

Schlimmer noch, die arithmetische Unzuverlässigkeit eines formalen Systems kann auf jeder Ebene der arithmetischen Hierarchie liegen, wie in diesem Beitrag konstruktiv gezeigt wird . Genau, wenn$S$Ist$Σ_n$-Sound dann gibt es eine$Σ_n$-Sound-Erweiterung von$S$das ist$Σ_{n+1}$-ungesund.

Dies impliziert, dass es schwierig sein kann, ohne eine philosophische Rechtfertigung Vertrauen in die Solidität eines formalen Systems zu haben. Erstens kann die Unzulänglichkeit nicht durch die Prüfung auf einen Beweis der Widersprüchlichkeit festgestellt werden. Nun, wenn$S$ausreichend ausdrucksstark ist, können wir vielleicht sagen "$S$ist rechnerisch einwandfrei" vorbei$S$, in diesem Fall können wir nach einem Beweis seiner Negation over suchen$S$, und wenn ja, wissen wir, dass etwas wirklich nicht stimmt. Aber selbst aus reiner Konsistenz, wenn wir (endlos) alle möglichen Beweise aufzählen und nie einen Widerspruch finden, haben wir immer noch nur einen ‚unendlich kleinen‘ Bruchteil aller möglichen Beweise aufgezählt, viel zu wenig, um sicher zu sein, dass es wirklich keinen Widerspruch gibt.

Es wird schlimmer. Folgendes berücksichtigen:

Lassen$Q$etwas sein$Π_1$-Satz so, dass$S$beweist ($Q$ist wahr, wenn es keinen Beweis dafür gibt$Q$über$S$mit weniger als$2^{10000}$Symbole).

Es stellt sich heraus, dass wir einen solchen Satz tatsächlich leicht konstruieren können$Q$, unter Verwendung der Standard-Gödel-Codierungstricks und des Fixpunktsatzes. Was für diejenigen, die damit nicht vertraut sind, schockierend sein mag, ist das$Q$ist eigentlich ziemlich kurz (weniger als eine Milliarde Symbole, wenn$S$ist so etwas wie ZFC), und wenn$S$Ist$Σ_1$- also komplett$Q$ist nachweisbar vorbei$S$(Weil$S$kann jeden möglichen Beweis mit weniger als überprüfen$2^{10000}$Symbole), aber sein kürzester Beweis hat zumindest$2^{10000}$Symbole!

Nun lass$T = S + \neg Q$, Wo$S$hat irgendein vernünftiges deduktives System. Zuerst,$T$ist inkonsistent. Zweitens liegt der kürzeste Beweis seiner Widersprüchlichkeit in der Größenordnung von$2^{10000}/len(Q)$, weil es in einen Beweis von ($\neg Q \to \bot$) über$S$, was nach endlich vielen zusätzlichen Schritten einen Beweis liefern würde$Q$über$S$.

Zusammenfassend könnte ein formales System eine ziemlich kleine Beschreibung haben, aber eine Inkonsistenz haben, deren Beweis so lang ist, dass wir sie niemals in der physischen Welt speichern können ...

Endlich:

Ich verstehe, dass die Antwort darauf von der Art des Beweises abhängen könnte$Z$hält, was ich nicht angegeben habe. Wenn dies der Fall ist, welche Arten von Beweisen sind für dieses Problem anfällig und welche nicht?

Aus all dem oben Genannten sollte klar sein, dass dies tatsächlich der Fall ist. Um es zu wiederholen, Sie brauchen den Beweis dafür$Z$innerhalb eines formellen Systems zu tun ist$Σ_1$-Klang. Wie konntest du das wissen? Nun, wir können so etwas nicht mit Sicherheit wissen. Fast alle Logiker glauben, dass ACA arithmetisch solide ist, aber verschiedene Logiker beginnen an verschiedenen Stellen, die Solidität zu bezweifeln, wenn Sie in der Hierarchie formaler Systeme aufsteigen. Einige bezweifeln die vollständige Arithmetik zweiter Ordnung, Z2 genannt, wegen ihres imprädikativen Verständnisaxioms. Andere finden es immer noch in Ordnung, bezweifeln aber ZFC. Einige denken, dass ZFC in Ordnung ist, zweifeln jedoch an einigen großen Kardinalsaxiomen.

Weil Sie eine explizite formale Beschreibung von (wie zu codieren) Turing-Maschinen und ihrer Ausführung haben.

Zu den Merkmalen dieser formalen Beschreibung gehören:

• die Stellen auf dem Tonband sind durch die natürlichen Zahlen indiziert
• die Schritte eines Ausführungstrace werden durch natürliche Zahlen indiziert
• Die Interpretation von Zeichenfolgen als Zahlen erzeugt eine Ausgabe natürlicher Zahlen

Sie können also sicher sein, dass, welches Analysemodell ^* Sie auch immer als Eingabe für die Berechnungstheorie verwendet haben, die Zahlen, die Ihre Maschine ausgeben wird, alle die natürlichen Zahlen dieses Modells sein werden.

_{*: Mit "Analysemodell" meine ich im Grunde das Modell einer beliebigen begrenzten Menge an Mengentheorie / Typentheorie / Logik höherer Ordnung / was auch immer Sie zum Argumentieren benötigen.}

Sie können jedoch die Berechnungstheorie in einem nicht standardmäßigen Analysemodell entwickeln. Die natürlichen Zahlen, die eine solche Maschine berechnen kann, können natürlich durchaus vom Standard abweichen.

Es sollte jedoch möglich sein, eine Standard-Turing-Maschine zu nehmen und sie in eine Nicht-Standard-Maschine umzuwandeln. Und es ist durchaus möglich, dass Sie eine Standard-Turing-Maschine und ein nicht standardmäßiges Analysemodell haben, für das die Standardmaschine möglicherweise ewig läuft, aber die nicht standardmäßige Version davon anhält.

Ich denke, es ist sogar möglich, dass ein nicht standardmäßiges Modell sagt, dass Ihre Standardmaschine anhält, und ein anderes nicht standardmäßiges Modell sagt, dass die Maschine nicht nur für immer läuft, sondern für immer in jeder nicht standardmäßigen Erweiterung dieses Modells läuft!