Peano-Arithmetik ist hinreichend, weil Peano-Arithmetik Berechnungen kodieren kann

• Peano-Arithmetik (PA) kann mechanische Rechenprozesse ausdrücken, daher lässt sich das Ende jeder einzelnen Goodstein-Folge in PA beweisen
• Mithilfe der Cantor-Normalform und hereditären Zahlendarstellung lassen sich Goodstein-Folgen und ihre Abwärtsbewegung ausdrücken, wodurch sich Beweise mit endlicher Länge konstruieren lassen
• Durch Induktion (starke Induktion/transfinite Induktion) lassen sich die Beweise jeweils bis zu Ordinalzahlen bestimmter Ordnung erweitern
• PA kann für jede natürliche Zahl n beweisen, dass „G(n) 0 erreicht“, aber ein umfassender Beweis des gesamten Goodstein-Theorems (für alle n) ist nicht möglich
• In PA lassen sich Berechnungen, Datenstrukturen (List, Pair usw.) und sogar die Kodierung einer Programmiersprache (Lisp) selbst sowie die Kodierung ihres eigenen Beweisverfahrens hinreichend umsetzen

---

Einleitung und Hintergrund des Problems

• Dieser Text beschreibt, dass Peano-Arithmetik (PA) beweisen kann, dass die Goodstein-Folge „für jedes n 0 erreicht (G(n) terminiert)”
• Für Logiker mag das selbstverständlich erscheinen, hier wird es jedoch aus der Perspektive der Kodierung von Berechnungen so erklärt, dass Programmierer es nachvollziehen können
• Für jeden einzelnen Fall einer Goodstein-Folge lässt sich innerhalb von PA eine konkrete Beweisroutine konstruieren

Ordinals(Ordinalzahlen) und Goodstein-Folgen

• Mit der Von-Neumann-Methode werden Ordinalzahlen (Sets as Ordinals) erzeugt
  • 0 ist die leere Menge, 1 ist {0}, 2 ist {0,1}, ω ist {0,1,2,…}, ω+1 ist {0,1,2,…,ω} usw.; die Ordnung ist wohldefiniert
• Goodstein-Folgen werden mithilfe einer hereditären Stellenwertdarstellung unter Verwendung der Cantor-Normalform beschrieben
  • Beispiel: ω^ω ist ((1,ω)), also ((1,(1,1)))
  • Die Ordnung < wird durch lexikographischen Vergleich der Ordinalzahlen/Koeffizienten jedes Terms bestimmt

Induktion und transfinite Induktion

• Induktion in der Peano-Arithmetik: Gilt eine Aussage für 0 und gilt sie für n→n+1, dann gilt sie für alle natürlichen Zahlen
• Starke Induktion ist ebenfalls in PA beweisbar
• Transfinite Induktion: In ZFC usw. lässt sie sich auf unendliche Ordinalzahlen erweitern und auf in Cantor-Normalform geschriebene Zahlen anwenden
  • Theorem 1: Jede absteigende Folge in Cantor-Normalform ist stets endlich
  • Theorem 2: Für Zahlen in Cantor-Normalform kann transfinite Induktion verwendet werden

Transfinite Induktion in PA und die Länge von Beweisen für Goodstein-Folgen

• PA kann für beliebige n einen Beweis für das Ende der Goodstein-Folge erzeugen
  • Je nach Turmhöhe m=O(log* n) (iterierter Logarithmus) der Cantor-Normalform lässt sich der Beweis konstruieren
  • Durch Kombination von m Beweisen pro Schritt ergibt sich eine Gesamtbeweislänge von O(m^2), oder mit Einführung einer speziellen Notation (ω[m]) verkürzt auf O(m log m)
• Allerdings ist ein Beweis des gesamten Goodstein-Theorems (für alle n) in PA unmöglich (keine transfinite Induktion über ε0)
  • Wäre dies möglich, ließe sich auch die Widerspruchsfreiheit von PA beweisen, was mit Gödels zweitem Unvollständigkeitssatz kollidieren würde

Kodierung von Programmen und Datenstrukturen in PA

• PA kann Berechnungen/Programme/Datenstrukturen (Zahlen, Paare, Listen und alle weiteren Strukturen) hinreichend kodieren
• Auf folgende Weise lassen sich verschiedene Funktionen umsetzen:
  • grundlegende Logik und Operationen (+, *, pow, //, %, min, max usw.)
  • Pattern Matching und bedingte Verzweigungen (if, cond usw.)
  • Kodierung einer Zahl als zwei Zahlen (Paar) und rekursive Erweiterung von Paaren zu komplexeren Strukturen wie Listen (rekursive Listen, Bäume, Text usw.)
• Mit dieser Kodierung von Datenstrukturen lässt sich sogar ein Interpreter für eine beliebige virtuelle Maschine/Programmiersprache (Lisp usw.) konstruieren

Bootstrapping nach Lisp und Kodierung

• Am Beispiel von Lisp wird erläutert, wie sich grundlegende numerische und logische Operationen, Datenstrukturen sowie ein Sprach-Interpreter/Interpreter implementieren lassen
• Die gesamte Struktur von Lisp (Zuordnung von Befehlen/Argumenten, Spezialformen, macro usw.) kann in PA durch geeignete Kombinationen von Funktionen implementiert werden
• Darüber hinaus lassen sich innerhalb von PA sogar der Beweisprozess von PA selbst, logische Beweisverfahren und selbstreferenzielle Strukturen vollständig symbolisch kodieren und umsetzen

Kodierung der Logik selbst innerhalb von PA

• In der mathematischen Logik lässt sich der Beweisprozess der First-Order Logic als Datensatz aus PA-Zahlen kodieren
• Jeder Beweisschritt, jede Aussage, jede Schlussregel und die Prüfung der Korrektheit eines Beweises lassen sich als Folge numerischer Funktionen bzw. Listenverarbeitung erkennen und verarbeiten
• Diese metaartige, selbstreferenzielle Kodierung führt direkt zu Gödels Unvollständigkeit und dem Beweis des Halteproblems

Fazit

• Berechnungen, Datenstrukturen, Programme und sogar logische Beweisprozesse lassen sich in PA hinreichend kodieren, beweisen und interpretieren
• Daher lässt sich jede beliebige Goodstein-Folge (für n gilt: G(n) terminiert) innerhalb von PA konkret beweisen
• Ein Beweis des gesamten Goodstein-Theorems (für alle n) im Sinne von „PA beweist das Goodstein-Theorem innerhalb von PA“ ist wegen der Grenzen der Logik jedoch nicht möglich
• Aus Sicht von Programmierern ist PA eine vollständige logische Grundlage, die Berechnung selbst kodieren kann

[GN⁺]

Hacker-News-Kommentare

• Dieser Beitrag ist eine Ausarbeitung einer Frage, die ich auf Stack Overflow gestellt habe. Er erklärt die Grenzen dessen, was sich im Peano-Axiomensystem beweisen lässt, und wie man Lisp innerhalb der Peano-Arithmetik bootstrappen könnte. Die meisten Witze stehen im zweiten Abschnitt. Korrekturen oder weitere Fragen sind willkommen.
  • Beim Lesen ist mir im Abschnitt "Why Lisp?" aufgefallen, dass eine Klammer nicht stimmt (siehe das Beispiel (defun not (x) (if x false true)). Sobald jemand anfängt, Klammern zu verwenden, prüfe ich instinktiv, ob sie korrekt geschlossen sind. Später die Bemerkung zu lesen, dass sich „mit einem Computer leicht programmieren lässt, ob Klammern ausgeglichen sind“, hat mich laut lachen lassen. Ich fand diese Art Witz wirklich großartig, und auch der Kommentar ; After a while, you stop noticing that stack of closing parens. im Abschnitt "Basic Number Theory" ist mir im Gedächtnis geblieben. Es war schön, nach langer Zeit wieder einmal etwas mit Lisp zu lesen, und der Beitrag hat wirklich Spaß gemacht.
  • Das ist wirklich interessant. Ich habe bisher nur die Einleitung gelesen, aber ich finde es faszinierend, dass man innerhalb der Peano-Arithmetik (PA) für jeden einzelnen Spezialfall einer Goodstein-Folge beweisen kann, dass er 0 erreicht, aber nicht beweisen kann, dass dies für „alle“ Fälle gilt. Das ist zwar im Grunde ein naheliegendes Resultat, aber trotzdem spannend. Und dass man allein in der Peano-Arithmetik Berechnung kodieren kann, ist wirklich seltsam – prinzipiell natürlich naheliegend, aber ich hatte vorher nicht noch einmal über diese Selbstreferenzialität nachgedacht. Ich habe zufällig vor Kurzem versucht, mich etwas tiefer in die Mengenlehre einzuarbeiten, und bin im Lehrbuch Intro to Set Theory gerade bis zum Abschnitt über Goodstein-Folgen gekommen. Falls jemand ein empfehlenswertes fortgeschrittenes Lehrbuch zur Mengenlehre oder eines, das tiefer in die Peano-Arithmetik einsteigt, empfehlen kann, wäre ich dankbar. Mein kleines Ziel ist es zu verstehen, warum PA für den Beweis des Goodstein-Theorems nicht ausreicht, aber ich bin auch für andere Wege dankbar.
  • An zwei Stellen beim Omega fehlt ein \omega.
• Das ist der Boyer-Moore-Theorie sehr ähnlich. Diese Theorie baut Mathematik auf dem Niveau der Peano-Axiome auf. Boyer und Moore entwickelten einen automatischen Theorembeweiser, der diese Theorie implementiert, und es gibt auch eine Kopie, die unter GNU Common LISP läuft. Sowohl der Aufsatz "A Computational Logic" als auch die nqthm-Implementierung sind sehenswert. Eindrucksvoll ist im Aufsatz zum Beispiel, dass beim Start mit den Peano-Axiomen komplexe Sätze wie die Multiplikation von Primzahlen schwierig sind, aber der Kommutativsatz der Addition, das Distributivgesetz der Multiplikation und Sätze über die GCD-Funktion durchaus beweisbar sind.
• Ich habe einen Hintergrund sowohl in Mathematik als auch im Programmieren, und persönlich finde ich den Teil über die Unabhängigkeit des Goodstein-Theorems noch interessanter, weil er sich selbstreferenziell zu umgehen scheint. Ich vermute, dass man das Goodstein-Theorem beweisen könnte, wenn man zu PA noch die Annahme „PA ist omega-konsistent“ hinzunimmt, und vielleicht ließe sich damit auch transfinite Induktion bis epsilon_0 durchführen. EDIT: Vielleicht reicht sogar schon „PA ist konsistent“?
  • Leider nicht. Und nicht nur Con(PA), sondern auch eine beliebige universell quantifizierte Formel reicht nicht aus. Siehe diese Math-StackExchange-Antwort. Zur ersten Frage würde mich interessieren, wie man Omega-Konsistenz als Formel von PA kodiert. Das fällt mir nicht sofort ein, daher macht mich das neugierig.
  • Ich bin der Fragesteller von Stack Overflow. Ich habe der Frage noch ein paar Links auf Antworten hinzugefügt. Im Wesentlichen reicht „PA ist konsistent“ nicht aus, aber eine Art „uniformes Reflexionsprinzip“ – also „wenn etwas in PA beweisbar ist, dann ist es wahr“ – würde ausreichen. Ich bin nicht sicher, ob dieses Prinzip vollständig mit Omega-Konsistenz zusammenfällt, aber die Erklärung auf Wikipedia lese ich so. Wenn T omega-konsistent ist, bedeutet das, dass „T + RFN_T + die Menge aller wahren Formeln konsistent ist“, und das lässt sich so interpretieren, dass es äquivalent dazu ist, dass „T + RFN_T wahr ist“.
  • Ich mag auch diese induktive (rekursive) Struktur. Letztlich baut man einen Meta-Beweis darüber, was PA beweist, und wenn man PA vertraut, kann man auch diesem Meta-Beweis vertrauen. Den Teil, dass einfach „PA ist konsistent“ genügen soll, verstehe ich allerdings nicht sicher. Ich denke, PA+„PA ist konsistent“ würde zulassen, dass es Modelle gibt, in denen das Goodstein-Theorem für die standardmäßigen natürlichen Zahlen wahr ist, aber zugleich auch Modelle, in denen es für irgendeine nichtstandardmäßige ganze Zahl N falsch ist. Ich würde erwarten, dass die stärkere Aussage der Omega-Konsistenz solche Fälle ausschließt.
  • In dem Math-Exchange-Beitrag heißt es, dass ein Beweis von PA+transfiniter Induktion (epsilon_0) PA selbst beweist. Ich denke, dass man mit PA+„PA ist konsistent“ transfinite Induktion bis epsilon_0 beweisen können sollte.
  • Ich glaube, das geht jetzt über die Details hinaus, zu denen ich mich noch sicher äußern kann. Laut ChatGPT reicht „PA + PA-Konsistenz“ allein nicht aus. Da ChatGPT offenbar sehr viele Logikbücher verarbeitet hat, klingt das nach einer Behauptung, der man wohl trauen kann.
• Ein Kommentar, den ich auf Stack Overflow an JoJoModding geschrieben habe, ist nicht korrekt. Ich hatte gesagt: „In nichtstandardmäßigen PA-Modellen gibt es unendliche natürliche Zahlen, deshalb kann PA, selbst wenn es beweist, dass es einen bestimmten Beweis erzeugt hat, nicht beweisen, dass dieser endliche Länge hat.“ Tatsächlich gilt aber: Wenn PA beweist, dass „PA X bewiesen hat“, dann beweist PA auch X selbst. Entscheidend ist nicht die Existenz nichtstandardmäßiger Modelle, sondern dass das Standardmodell der natürlichen Zahlen ein Modell von PA ist. Wenn PA also „beweist, dass es X beweist“, dann wird damit effektiv ein Beweis erzeugt, der einer standardmäßig endlichen natürlichen Zahl entspricht, und mit dieser Zahl kann man innerhalb von PA einen tatsächlichen Beweis von X konstruieren.
  • Ich habe gerade keine Zeit, die Logik im Detail zu prüfen, aber in natürlicher Sprache scheint der entscheidende Unterschied zu sein, dass es nicht heißt „PA beweist forall n, G(n)“, sondern „PA beweist forall n, Provable(G(n))“. Ich bin nicht besonders stark in Logik; wenn jemand konkret erklären könnte, warum man aus einem Beweis von forall n, Provable(P(n)) nicht auf einen Beweis von Provable(forall n, P(n)) schließen kann, wäre ich dankbar.
  • Die Aussage „Wenn PA beweist, dass ‚PA X beweist‘, dann beweist PA X“ stimmt nicht. Man kann in PA eine Funktion definieren, die alle möglichen Beweise durchsucht, und ich habe diese Vorgehensweise im letzten Teil der Antwort skizziert. Daraus kann man auch Funktionen wie will-return und opposite-return bauen; das entspricht dem Standardbeweis des Halteproblems. Betrachte den Fall opposite-return(opposite-return, opposite-return): Wenn PA beweist, dass opposite-return zurückkehrt, dann beweist es damit auch, dass es tatsächlich nicht zurückkehrt; und wenn es beweist, dass es nicht zurückkehrt, dann beweist es, dass es zurückkehrt. Wenn PA die stärkere Aussage akzeptieren würde, dass „alles, was beweisbar ist, auch tatsächlich beweisbar ist“, dann wäre das im Grunde Gödels zweiter Unvollständigkeitssatz und würde bedeuten, dass PA widersprüchlich ist. Deshalb muss man streng zwischen „PA beweist X“ und „PA beweist, dass es X beweist“ unterscheiden.
• Schon reiner Lambda-Kalkül reicht aus, weil der Lambda-Kalkül selbst Berechnung kodiert.
• Ich habe mit jemandem über induktive Datentypen gesprochen und dabei die Nat-Definition mit zero/succ gezeigt, wie man sie in Lean oder Rocq sieht. Die andere Person fragte sich: „Reicht das allein?“, „Braucht man wirklich die Peano-Arithmetik? Gibt es etwas noch Primitiveres als induktive Datentypen?“ Das hat mich daran erinnert, dass man die Peano-Arithmetik nicht als etwas Wesentliches oder Selbstverständliches betrachten sollte, sondern als eine konkrete Designentscheidung.
  • Auf die Frage „Gibt es etwas Grundlegenderes als induktive Datentypen?“ würde ich antworten, dass natürliche Zahlen selbst primitiver sind als induktive Datentypen. Jeder induktive Datentyp lässt sich aus natürlichen Zahlen und einigen wenigen primitiven Typkonstruktoren (Π, Σ, =, Ω) aufbauen.
• Siehe auch dieses Q&A zum Kirby-Paris-Theorem.
• Zum Thema PA-Konsistenz hier ein Video dazu, was innerhalb von PA beweisbar ist: YouTube-Link
  • Das ist etwas, das man Nicht-Logikern unbedingt erklären muss. Nach Gödels zweitem Unvollständigkeitssatz gilt: Wenn PA seine eigene Konsistenz beweisen könnte, dann wäre PA widersprüchlich (und könnte damit inklusive falscher Aussagen alles beweisen). Dieses Video beweist nicht, dass PA widersprüchlich ist, sondern zeigt, dass PA in einem schwächeren Sinn ihre „eigene Konsistenz“ beweisen kann. Ohne Grundkenntnisse in Logik ist das schwer präzise zu verstehen, aber es ist auf jeden Fall interessant.
• Dieses Thema hat hier 123 Punkte, während der eigentliche Beitrag auf SO nur 11 Upvotes hat.
  • Auf Stack Overflow kann man erst ab 15 Punkten Upvotes vergeben. Wegen des Reputationssystems haben Leute oft auch wenig Lust, dort zu posten, und die 15-Punkte-Grenze scheint Upvotes zu bremsen.
• Reicht bloße Computation wirklich aus? Die berechenbaren reellen Zahlen sind nur eine Teilmenge aller reellen Zahlen.
  • Ich halte schon die Bezeichnung „reelle Zahlen“ für irreführend. Man kann reelle Zahlen als reale physische Verhältnisse interpretieren. Wenn man zum Beispiel 180,255 Pfund sagt, bedeutet das ein reales physisches Verhältnis zwischen dem tatsächlichen Gewicht von Jones und einem Standard-Pfund. Solche Verhältnisse existieren physisch tatsächlich. In diesem Sinn können reelle Zahlen als physische Verhältnisse verstanden werden. Heute dominiert dagegen die Sicht auf Zahlen als abstrakte, von der Realität getrennte Begriffe; das ist typisch platonistisch. Aber in der realen Welt ist es unmöglich, irgendetwas mit unendlicher Präzision zu messen oder darzustellen. Messungen mit mehr als 50 Stellen Genauigkeit sind zum Beispiel wegen quantenmechanischer Grenzen unmöglich. Wenn man die Bahnen von Himmelskörpern im Sonnensystem fehlerfrei messen wollte, müsste man bei mehr als 50 Stellen die Masseneffekte benachbarter Sterne berücksichtigen, bei über 100 Stellen die gesamte Galaxie modellieren und schließlich sogar physikalische Einflüsse einbeziehen, die sich gar nicht messen lassen. Deshalb ist in der Realität nur Mathematik mit endlicher Präzision möglich. Das heißt: Im Prinzip ist alles berechenbar, aber gegen unendlich hin wird schon das mathematische Modell selbst bedeutungslos.
  • Ist das wirklich so? Eigentlich beruht die Vorstellung, dass es „mehr“ Überabzählbares gibt, auf einem Missverständnis. Siehe meine Erklärung. Wenn man akzeptiert, dass es mehr Überabzählbares gibt, muss man zwangsläufig eine umstrittene Position dazu einnehmen, was „Existenz“ bedeutet. Siehe auch diese Diskussion. Und selbst wenn wir die logische Argumentation bis zum Ende treiben, lässt sich alles mit einem Computer darstellen. Selbst wenn man zu ZFC große Mengen hinzufügt, kann man von PA ausgehend letztlich jede beliebige Schlussfolgerung herleiten, daher halte ich PA praktisch für ausreichend. Falls mehr Überzeugungsarbeit nötig ist, empfehle ich das Buch Gödel, Escher, Bach.
  • Mein Ansatz ist etwas anders. Reelle Zahlen im Allgemeinen lassen sich weder berechnen noch symbolisieren noch in irgendeiner Form aufschreiben, aber Aussagen über reelle Zahlen kann man oft trotzdem nützlich ausdrücken und verarbeiten. Ich finde Versuche wie die von Harvey Friedman oder vom Autor dieses Beitrags, in einfachen Systemen überraschend komplexe Werte zu erzeugen, wirklich spannend. (Hinweis: Die audiomulch-Website ist nicht erreichbar.)
  • Ohne ein Ziel zu benennen, ist die Frage „reicht aus“ begrifflich unscharf. Entscheidend ist, wofür etwas ausreichen soll.
  • Ich denke, schon die Frage „Reicht Computation allein aus?“ ist falsch gestellt. Natürlich reicht sie nicht aus; wenn sie ausreichen würde, hätten einige Leute recht, die die Realität wie ein leicht zu glaubendes Uhrwerk betrachten. Die Wirklichkeit ist viel interessanter und komplexer.