Die Konsistenz von New Foundations – ein schwieriger mathematischer Beweis, verifiziert mit Lean

Here is a summary of the key points from the given article, organized using Markdown:

Konsistenzbeweis der Mengenlehre New Foundations

• Randall Holmes hat seit 2010 behauptet, die Widerspruchsfreiheit der 1937 von Quine vorgeschlagenen Mengenlehre "New Foundations (NF)" bewiesen zu haben
• Dieses Repository beweist nun, dass NF tatsächlich widerspruchsfrei ist, indem es die schwierigen Teile von Holmes' Beweis mit dem interaktiven Theorembeweiser Lean verifiziert
• Der Beweis ist nun abgeschlossen, und die Aussage des Theorems ist in ConNF/Model/Result.lean zu finden

Ziel

• Es ist bekannt, dass NF genau dann und nur dann widerspruchsfrei ist, wenn Tangled Type Theory (TTT) widerspruchsfrei ist
• Durch die formale Konstruktion eines Modells von TTT in Lean wird die Widerspruchsfreiheit von NF bewiesen
• Die Arbeit basiert auf mehreren Versionen von Holmes' Beweis, wurde jedoch mit vielen Änderungen und Ergänzungen versehen, damit sie mit Leans Typtheorie kompatibel ist
• Dieses Projekt hängt von mathlib ab, der Community-Mathematikbibliothek für Lean, sodass vertraute Resultate über Kardinalzahlen, Gruppen usw. verwendet werden können, ohne sie direkt beweisen zu müssen
• Obwohl alle Definitionen und Theoreme in mathlib und diesem Projekt durch Leans vertrauenswürdigen Kernel verifiziert wurden, kann Lean nicht prüfen, ob die Beschreibungen von Definitionen und Theoremen mit den beabsichtigten englischen Erläuterungen übereinstimmen; daher ist bei Schlussfolgerungen aus dem Code dieses Projekts Vorsicht bei der Übersetzung zwischen beidem geboten

Tangled Type Theory (TTT)

• TTT ist eine mehrsortige Mengenlehre mit der Gleichheitsrelation "=" und der Zugehörigkeitsrelation "∈"
• Die Sorten sind durch eine Limesordinalzahl λ indiziert; Elemente von λ heißen Typindizes
• Die Formel "x = y" ist wohlgeformt, wenn x und y denselben Typ haben, und die Formel "x ∈ y" ist wohlgeformt, wenn x einen beliebigen kleineren Typ als y hat
• Eines der Axiome von TTT ist Extensionalität: Eine Menge vom Typ α wird durch ihre Elemente jedes Typs β < α eindeutig bestimmt
• Wenn sich zum Beispiel zwei Mengen vom Typ α unterscheiden, dann besitzen sie für jedes β < α unterschiedliche Elemente vom Typ β, was die Konstruktion eines TTT-Modells erschwert

Strategie

• Der Modellaufbau folgt grob der folgenden Strategie:

  • Konstruktion des Basistyps

    • Setze λ als Limesordinalzahl, κ > λ als reguläre Ordinalzahl und μ > κ als starke Limeskardinalzahl mit Kofinalität mindestens κ
    • Mengen mit Größe kleiner als κ heißen klein
    • Auf Ebene -1 wird ein Hilfstyp namens Basistyp konstruiert, der letztlich unter allen Typen liegt, die Teil des Modells werden
    • Die Elemente dieses Typs heißen Atome (nicht Atome im Sinne von ZFU oder NFU), davon gibt es μ viele, aufgeteilt in Litter der Größe κ

  • Konstruktion jedes Typs

    • Auf jeder Typebene α wird eine Sammlung von Modellelementen für das beabsichtigte Modell von TTT erzeugt, manchmal t-Mengen genannt
    • Es wird eine Permutationsgruppe erzeugt, deren Elemente zulässige Permutationen genannt werden; diese wirken auf die t-Mengen
    • Die Zugehörigkeitsrelation bleibt unter der Wirkung der zulässigen Permutationen erhalten
    • Jede t-Menge muss unter der Wirkung zulässiger Permutationen einen Träger besitzen, also eine kleine Menge von Objekten, Adressen genannt, so dass die t-Menge immer dann fixiert bleibt, wenn eine zulässige Permutation alle Elemente des Trägers fixiert
    • Jeder t-Menge auf Ebene α wird für jeden Typ β < α eine bevorzugte Erweiterung zugeordnet, und aus den Elementen einer t-Menge kann rekonstruiert werden, welche Erweiterung bevorzugt wird
    • Erweiterungen dieser t-Mengen in andere Untertypen können aus der β-Erweiterung erschlossen werden, wodurch das Extensionalitätsaxiom von TTT erfüllt werden kann

  • Kontrolle der Größe jedes Typs

    • Jeder Typ α kann nur unter der Annahme konstruiert werden, dass alle Typen β < α die Größe genau μ haben, zusätzlich zu anderen Hypothesen
    • Es ist leicht zu zeigen, dass die Sammlung der t-Mengen auf Ebene α Kardinalität mindestens μ besitzt; daher muss gezeigt werden, dass die Elemente dieser Menge höchstens μ viele sind
    • Dies gelingt, indem gezeigt wird, dass es unter der Wirkung zulässiger Permutationen nicht so viele grundsätzlich verschiedene Beschreibungen des Verflochtenseins gibt
    • Dafür wird das Freiheits-der-Wirkung-Theorem benötigt, ein technisches Hilfsresultat, das die Konstruktion zulässiger Permutationen ermöglicht
    • Das Hauptergebnis dieses Abschnitts befindet sich hier

  • Abschluss der Induktion

    • Durch rekursive Ausführung des obigen Verfahrens lassen sich verflochtene Typen auf jeder Typebene α erzeugen
    • In der Mengenlehre ist dies ein einfacher Schritt, in der Typtheorie jedoch wegen der Verflechtung der verschiedenen benötigten Induktionshypothesen mit viel Arbeit verbunden
    • Anschließend wird geprüft, ob unsere Konstruktion tatsächlich ein Modell von TTT liefert, indem sie eine endliche Axiomatisierung der Theorie erfüllt
    • Wir haben uns dafür entschieden, Hailperins endliche Axiomatisierung des Komprehensionsschemas von NF in eine endliche Axiomatisierung von TTT zu überführen und sie in der Ergebnisdatei darzustellen
    • Diese Wahl ist jedoch willkürlich, und mit der bereits vorhandenen Infrastruktur lassen sich leicht auch andere endliche Axiomatisierungen beweisen

Meinung von GN⁺

• Dieser Beweis ist ein sehr bedeutendes Resultat, weil er die Widerspruchsfreiheit der NF-Mengenlehre formal nachweist, die bislang nur auf sehr abstrakter Ebene bekannt war. Das ist nicht nur für die reine Mathematik wichtig, sondern zeigt auch einen praktischen Fortschritt bei Beweisassistenten und automatisierter Theorembeweisung
• Die Formalisierung mit Lean garantiert die Genauigkeit und Vollständigkeit des Beweises, kann aber zugleich schwer verständlich sein, weil sie in einer Sprache geschrieben ist, die vielen Mathematikern nicht vertraut ist. Eine klare Erklärung der Kernideen des Beweises in natürlicher Sprache sollte parallel dazu erfolgen
• Es fehlt zudem etwas an einer intuitiven Erklärung der Hintergrundtheorie, etwa warum das ungewöhnliche Extensionalitätsaxiom von TTT nötig ist und wie sich TTT zu anderen Mengenlehren verhält. Neben dem formalen Beweis wären ergänzende Diskussionen zum philosophischen und historischen Kontext hilfreich, um das Verständnis der NF-Theorie weiter zu vertiefen
• Interessant erscheinen auch weitere Forschungsthemen, etwa in welcher Beziehung das konstruierte Modell zu Modellen der Standard-Mengenlehre ZFC steht und wie die Widerspruchsfreiheit von NF mit der Widerspruchsfreiheit anderer Axiomensysteme zusammenhängt
• Ein so komplexes Beispiel der Formalisierung mit Lean kann auch für die Automatisierung von Beweisen in anderen mathematischen Bereichen vorbildhaft sein. Wenn ähnliche Arbeiten auf Theoreme angewandt würden, deren Beweisweg bisher nicht gut bekannt ist, könnte das große Auswirkungen auf die Mathematik haben

[GN⁺]

Hacker-News-Kommentare

• Das Risiko, dass ein mit Lean geführter Beweis falsch ist, ist sehr gering. Unabhängig von Bugs in Lean gilt jedoch: Man muss die Schlussfolgerung sorgfältig lesen und prüfen, ob tatsächlich das bewiesen wurde, was behauptet wird — ein bekanntes Problem in Softwareverifikation und Mathematik.
• Dies scheint der erste Fall zu sein, in dem ein Beweisassistent eingesetzt wurde, um den Status eines schwierigen Beweises zu klären. Zuvor gab es Projekte, die bestehende Beweise überprüften, die große Rechenanteile enthielten und mit nicht vertrauenswürdiger Software verarbeitet worden waren; in diesem Fall war jedoch erstmals der erkenntnistheoretische Status des Ergebnisses in der mathematischen Gemeinschaft unklar.
• Es wird die Frage aufgeworfen, worin die grundlegenden Unterschiede zwischen Coq und Lean bestehen und ob sie auf derselben Art von Logik basieren. In der zugehörigen Diskussion werden schwer verständliche Inhalte erwähnt.
• Anhänger von Lean neigen dazu, den Punkt, dass Lean eine überlegene Beweismethode sei, zu stark auszuspielen. Lean ist lediglich eine alternative Beweismethode und hat als Programmiersprache und System eigene Bugs; außerdem hängt es stark von verschiedenen Bibliotheks-Stacks ab, die andere geschrieben haben.
• Genauer und ehrlicher wäre die Formulierung, dass der geschriebene Beweis von menschlichen Mathematikern geprüft wurde und anschließend in Lean übertragen wurde, wo er ebenfalls verifiziert wurde, statt zu sagen, Lean habe bestätigt, dass der Beweis gut sei. Die Darstellung, Lean liefere die einzig maßgebliche und goldene Verifikation, ist nicht zutreffend, oder zumindest hat man keine solche Darstellung gesehen.
• Es wird um eine grobe Erklärung gebeten, was an der Formalisierung der Mengenlehre „New Foundations“ im Vergleich zu anderen Formalisierungen besonders oder neu ist, und zwar in einer Form, die Mathematikstudierende im Grundstudium oder Fachleute aus dem Ingenieurwesen lesen können.
• Es wird gefragt, ob dieser Ansatz letztlich zu kollaborativen Beweisen und „Bugfixes“ führen und die Mathematik zu einem Prozess machen wird, der dem von Code auf GitHub ähnelt.
• Nach Gödels Satz kann kein hinreichend starkes System seine eigene Konsistenz beweisen; dazu wird eine Frage gestellt.
• Man würde das mathlib-Projekt gern weiterverfolgen, hat dafür aber keine Zeit. Es wird gefragt, ob es eine Möglichkeit gibt, sich auf sehr passive Weise zu beteiligen.