Die Konsistenz von New Foundations – mit Lean verifizierter Beweis schwieriger Mathematik

 (leanprover-community.github.io)
1 Punkte von GN⁺ 2024-04-24 | 1 Kommentare | Auf WhatsApp teilen
  • Der schwierige Teil des Konsistenzbeweises für die 1937 von Quine vorgeschlagene Mengenlehre New Foundations wurde mit Lean verifiziert; das zentrale Theorem ist in ConNF/Model/Result.lean festgehalten
  • Der Ansatz nutzt das Resultat, dass die Konsistenz von New Foundations und Tangled Type Theory (TTT) äquivalent ist, und konstruiert in Lean formal ein TTT-Modell
  • Die Konstruktion des TTT-Modells ist wegen der Extensionalität schwierig: Mengen müssen durch Elemente niedrigerer Typen eindeutig bestimmt sein
  • Für die Modellkonstruktion werden Basistypen, t-sets, zulässige Permutationen, kleine Supports und Preferred Extensions verwendet; um die Typgrößen durch μ zu kontrollieren, ist das Freedom-of-Action-Theorem nötig
  • Der Lean-Kernel prüft die formalisierte Beweisführung, garantiert aber nicht, dass formale Aussagen der beabsichtigten englischen Bedeutung entsprechen; die Interpretation der Ergebnisse erfordert daher eine Prüfung der Übersetzung

Mit Lean abgeschlossene Konsistenzverifikation von New Foundations

  • 1937 schlug Quine die Mengenlehre New Foundations vor, und Randall Holmes behauptet seit 2010, einen Konsistenzbeweis dafür zu besitzen
  • Dieses Projekt konzentriert sich darauf, den schwierigen Teil von Holmes’ Beweis mit dem interaktiven Theorem Prover Lean zu verifizieren und damit die Konsistenz von New Foundations zu zeigen
  • Der Beweis ist abgeschlossen; die Theorem-Aussage ist in ConNF/Model/Result.lean zu finden
  • Zugehörige Materialien werden ebenfalls bereitgestellt

Code lokal ausführen

  • Für die lokale Ausführung installiert man elan, klont das Repository und führt anschließend im Repository-Root den folgenden Befehl aus
lake exe cache get
  • Danach kann der Code in einem Editor wie Visual Studio Code angesehen werden; über die Kommandozeile lässt er sich mit lake build direkt kompilieren

Die Verbindung zwischen New Foundations und TTT

  • New Foundations ist genau dann konsistent, wenn Tangled Type Theory (TTT) konsistent ist
  • Das Projekt hat in Lean formal ein TTT-Modell konstruiert und erhält dadurch als Schlussfolgerung auf Papier die Konsistenz von New Foundations, also Con(NF)
  • Die Arbeit basiert auf mehreren Beweisdokumenten von Holmes, erforderte aber viele Änderungen und Ergänzungen, um sie an Leans Typentheorie anzupassen

Grundlage der Lean-Verifikation und Hinweise zur Interpretation

  • Das Projekt hängt von der in Lean geschriebenen Community-Mathematikbibliothek mathlib ab
  • Dank mathlib können vertraute Resultate etwa zu Kardinalzahlen und Gruppen im Projekt genutzt werden, ohne sie erneut beweisen zu müssen
  • Die Definitionen und Theoreme von mathlib und diesem Projekt werden von Leans vertrauenswürdigem Kernel geprüft
    • Der Lean-Kernel verifiziert rechnerisch, dass der konstruierte Beweis tatsächlich korrekt ist
  • Allerdings kann Lean nicht prüfen, ob eine formale Aussage ihrem beabsichtigten englischen Äquivalent entspricht
    • Wenn aus dem Code Schlussfolgerungen gezogen werden, muss die Übersetzung zwischen englischer Beschreibung und formaler Aussage sorgfältig betrachtet werden

Struktur und Schwierigkeiten der Tangled Type Theory

  • TTT ist eine mehrsortige Mengenlehre mit Gleichheit = und Zugehörigkeitsrelation ∈
  • Sorten werden durch eine Limesordinalzahl λ indiziert; die Elemente von λ heißen Typindizes
  • Die Wohlgeformtheit von Ausdrücken wird durch Typen eingeschränkt
    • x = y ist wohlgeformt, wenn x und y denselben Typ haben
    • x ∈ y ist wohlgeformt, wenn der Typ von x niedriger ist als der Typ von y
  • Die zentrale Schwierigkeit entsteht aus dem Extensionalitätsaxiom von TTT
    • Eine Menge vom Typ α muss durch Elemente eines beliebigen Typs β < α eindeutig bestimmt sein
    • Wenn sich zum Beispiel zwei Mengen vom Typ α unterscheiden, müssen sie für jedes β < α unterschiedliche Elemente vom Typ β enthalten
  • Diese Anforderung macht die Konstruktion eines TTT-Modells schwieriger als eine einfache Konstruktion eines mengen-theoretischen Modells

Wichtige Schritte der Modellkonstruktion

  • Konstruktion der Basistypen

    • Sei λ eine Limesordinalzahl, κ > λ eine reguläre Ordinalzahl und μ > κ eine starke Limeskardinalzahl mit Kofinalität mindestens κ
    • Mengen mit Größe kleiner als κ werden small genannt
    • Zunächst wird ein base type auf Level -1 konstruiert, ein Hilfstyp unterhalb aller Modelltypen
    • Die Elemente dieses Typs heißen atoms, sind aber keine Atome im Sinne von ZFU oder NFU
    • Es gibt μ viele atoms, die in litters der Größe κ partitioniert werden

  • t-sets und zulässige Permutationen

    • Auf jedem Typ-Level α wird eine Kollektion erzeugt, die zu den Elementen des TTT-Modells werden soll; sie wird t-set genannt
    • Gleichzeitig wird eine Permutationsgruppe konstruiert, die auf t-sets wirkt: die allowable permutations
    • Die Zugehörigkeitsrelation bleibt unter der Wirkung der allowable permutations erhalten
    • Jedes t-set wird so festgelegt, dass es einen support für die Wirkung der allowable permutations besitzt
    • Ein support ist eine kleine Menge von Objekten, die addresses genannt werden
    • Wenn eine allowable permutation alle Elemente des support fixiert, fixiert sie auch dieses t-set

  • Extensionalität über Preferred Extensions herstellen

    • Jedes t-set auf Level α besitzt eine preferred extension eines bestimmten Typs β < α
    • Aus den Elementen eines t-set lässt sich rekonstruieren, welche Extension bevorzugt wird; Extensions anderer niedrigerer Typen werden aus dieser β-Extension abgeleitet
    • Diese Struktur wird genutzt, um das Extensionalitätsaxiom von TTT zu erfüllen

  • Kontrolle der Typgrößen

    • Jeder Typ α lässt sich nur unter Annahmen konstruieren, etwa dass die Größe aller Typen β < α exakt μ ist
    • Es ist leicht zu zeigen, dass die Kollektion der t-sets auf Level α mindestens Größe μ hat; daher muss gezeigt werden, dass es höchstens μ viele sind
    • Dazu wird gezeigt, dass es unter der Wirkung der allowable permutations nicht viele grundsätzlich verschiedene Beschreibungen von tangles gibt
    • Für diesen Schritt ist das Freedom-of-Action-Theorem nötig, ein technisches Hilfslemma, das die Konstruktion von allowable permutations ermöglicht
    • Das wichtigste Resultat dieses Abschnitts findet sich in ConNF.mk_tSet

  • Abschluss der Induktion und Prüfung der Axiome

    • Das obige Verfahren wird rekursiv ausgeführt, um auf jedem Typ-Level α den Typ der tangles zu erzeugen
    • In der Mengenlehre ist dies ein einfacher Schritt, doch in der Typentheorie erfordert er viel Arbeit, weil mehrere notwendige Induktionsannahmen miteinander verwoben sind
    • Anschließend wird geprüft, ob das konstruierte Objekt eine endliche Axiomatisierung der Theorie erfüllt, um sicherzustellen, dass es ein Modell von TTT ist
    • Das Projekt verwendet Hailperins endliche Axiomatisierung des NF-Comprehension-Schemas und wandelt sie in eine endliche Axiomatisierung von TTT um
    • Die Ergebnisdatei befindet sich in der results file
    • Diese Wahl ist willkürlich; mit der bereits aufgebauten Infrastruktur ließen sich auch andere endliche Axiomatisierungen leicht beweisen

Verwandte Beiträge

1 Kommentare

 
GN⁺ 2024-04-24
Hacker-News-Meinungen

  • Ich halte das Risiko, dass ein in Lean geführter Beweis falsch ist, für sehr gering.
    Unabhängig von Lean-Bugs gibt es jedoch ein sowohl aus der Softwareverifikation als auch aus der Mathematik gut bekanntes Risiko: Man muss die Schlussfolgerung genau lesen und prüfen, ob tatsächlich die benötigte Aussage bewiesen wurde.
    Ich habe Wilshaws abschließende Schlussfolgerung sorgfältig gelesen und bin der Meinung, dass tatsächlich das bewiesen wurde, was bewiesen werden musste.

    • Das Paper sagt etwas Ähnliches: Alle Definitionen und Theoreme in mathlib und in diesem Projekt wurden vom Trusted Kernel von Lean geprüft, und der von uns konstruierte Beweis wurde rechnerisch als tatsächlich korrekt verifiziert.
      Lean kann jedoch nicht überprüfen, ob die Aussagen der Definitionen und Theoreme mit der beabsichtigten englischen Formulierung übereinstimmen; daher muss man beim Ableiten der Schlussfolgerung aus dem Code dieses Projekts vorsichtig mit der Übersetzung ins Englische sein.

    • Das von mir angesprochene Problem hängt mit Bedenken rund um Bibliotheken zusammen: Wenn man ein definiertes Konzept verwendet, muss man sicher sein, dass diese Definition korrekt ist, also dass wirklich das bewiesen wurde, was man braucht.
      Wilshaws Formalisierung verwendet zwar Bibliotheken, ist aber für diesen Einwand nicht anfällig. Bewiesen wurde, dass ein bestimmtes definiertes Konzept ein bestimmtes Bündel prädikatenlogischer Formeln erster Stufe erfüllt; und wenn es ein Prädikat gibt, das solche Formeln erfüllt, dann ist NF konsistent.

    • Ein weiteres Risiko sind Bugs in Lean selbst. Das wäre bei Theorem-Provern nicht beispiellos 1.
      Zufällig darauf zu stoßen mag schwierig sein, aber groß angelegte Kollaborationen, bei denen beliebige Personen Schritte ergänzen, werden immer größer, wie in 3. Es könnte zu einer berechtigten Sorge werden, dass jemand einen entdeckten Bug ausnutzt, um einen Schritt einzufügen und das Ganze zu sabotieren.

    • Aus grundlagentheoretischer Sicht ist außerdem wichtig, dass dieser Beweis ein Beweis der Gleichkonsistenz zwischen NF und dem Lean-Kernel ist. Der Lean-Kernel selbst wird von Menschen überprüft.
      Mechanisierte Theorem-Prover bewahren das Maß an Korrektheit, das ihnen durch Menschen oder andere externe Systeme eingespeist wurde.

  • Wenn ich mich nicht täusche, scheint dies der erste Fall zu sein, in dem der Status eines schwierigen Beweises, der jahrelang in einem unklaren Zustand geblieben war, mit einem Beweisassistenten geklärt wurde.
    Es gab Projekte, die bereits existierende Beweise verifiziert haben, bei denen nicht vertrauenswürdige Software einen großen rechnerischen Anteil übernommen hatte, etwa der Vier-Farben-Satz in Coq. Aber dies scheint der erste Fall zu sein, in dem der epistemische Status des Resultats selbst in der breiteren mathematischen Community ungewiss war.

  • Kann jemand grob erklären, was an der Formalisierung der Mengenlehre „New Foundations“ im Vergleich zu anderen Formalisierungen besonders oder neu ist?
    Alternativ wäre auch ein Erklärlink geeignet, den Mathematik-Studierende im Grundstudium oder Fachleute aus dem Engineering lesen können.

    • Ich habe gerade den Wikipedia-Artikel bearbeitet; er sollte jetzt etwas lesbarer sein: https://en.wikipedia.org/wiki/New_Foundations
      Der Kern ist aus meiner Sicht die Existenz einer universellen Menge. In meinem Anwendungsfall, Typsystemen für Programmiersprachen, ist eine solche universelle Menge sehr nützlich.
      Die verschiedenen Workarounds bestehender Systeme, etwa kumulative Universen oder type-in-type, sind nicht zufriedenstellend. Stattdessen kann man einfach prüfen, ob eine Typsignatur stratifiziert ist, und anschließend vergessen, dass Typen numerische Stufen haben.
    • Was mir an NF ästhetisch wirklich gefällt, ist die Art, wie das Aussonderungsaxiom angepasst wird, damit die „Menge aller Mengen“ nicht zu Russells Paradoxon führt.
      Im Grunde wird verlangt, dass das Prädikat, mit dem man Teilmengen auswählt, ein sehr leichtgewichtiges Typsystem einhält. „x ist kein Element seiner selbst“ ist in einem vernünftigen Typsystem keine wohlangetypte Frage und erfüllt insbesondere auch nicht die Anforderung der „Stratifizierbarkeit“ in NF; daher kann man die Menge aus Russells Paradoxon, also die Menge aller Mengen, die sich nicht selbst enthalten, nicht bilden.
    • Ein „guter“ Punkt an NF ist, dass es nur zwei Axiome/Axiomenschemata gibt: 1) Mengen mit denselben Elementen sind gleich, 2) jeder beliebigen stratifizierbaren Eigenschaft entspricht die Menge aller Dinge, die diese Eigenschaft haben.
      Auch die Definition von „stratifizierbar“ ist nicht besonders kompliziert. ZF hat dagegen acht Axiome/Axiomenschemata, die ziemlich ad hoc wirken.

  • Weil ich wissen wollte, was der grundlegende Unterschied zwischen Coq und Lean ist und ob sie auf derselben Art von Logik arbeiten, habe ich diesen Beitrag gefunden 1.
    Die Diskussion habe ich kaum verstanden, und ich benutze auch keines von beiden praktisch. Falls es dazu mehr Erklärungen oder Vergleiche mit anderen Beweisassistenten gibt, würde ich sie gern hören.

    1 https://proofassistants.stackexchange.com/questions/153/what...

  • Lean-Befürworter scheinen die Formulierungen etwas zu überziehen. Lean ist nicht die überlegene Beweismethode, wie oft angedeutet wird, sondern eine alternative Art des Beweisens.
    Wenn man versucht, Lean zu lernen, merkt man schnell: Es ist eine Programmiersprache und ein System mit eigenen Bugs und hängt stark von mehreren Library-Stacks ab, die von anderen Menschen geschrieben wurden. In diesen Libraries stecken Entscheidungen, und es kann Lücken oder Bugs geben.
    Deshalb habe ich Einwände gegen Formulierungen wie „Lean hat gesagt, dass dieser Beweis gut ist“. Präziser und ehrlicher wäre meiner Ansicht nach: Der geschriebene Beweis wurde von menschlichen Mathematikern geprüft, und Menschen haben diesen Beweis nach Lean übersetzt, wo er ebenfalls geprüft wurde. Die Vorstellung, Lean liefere die einzige goldene Verifikation, ist nicht unbedingt korrekt, oder zumindest habe ich keine Erklärung gesehen, die das belegt. Der Untertitel „Digitalisierung von Randall Holmes’ Beweis“ scheint mir die treffendste Formulierung zu sein.

    • Bei einem starken System wie Lean halte ich einen maschinengeprüften Beweis für einem nur von Menschen geprüften Beweis weit überlegen. Menschen sind erstaunlich, aber sie langweilen sich und übersehen Details.
      Das ist nicht nur eine theoretische Behauptung. Menschen haben Euklids Elemente mehr als 2.000 Jahre lang gelesen, bevor ihnen ein fehlendes Axiom auffiel. Das ist die Art grundlegender Fehler, die ein korrekt funktionierendes maschinelles Beweisprüfsystem sofort offengelegt hätte.
      Auch veröffentlichte mathematische Beweise stellen sich später oft als falsch heraus. Je ausgefeilter die Mathematik wird, desto schwieriger wird es für Menschen, jeden Schritt korrekt zu überprüfen. Maschinen sind bei der Erzeugung von Beweisen noch nicht so gut wie Menschen, aber bei der Verifikation sind sie konkurrenzlos.
      Es gibt auch Systeme, die mit Lean „konkurrieren“, daher würde ich nicht sagen, Lean sei „der einzig wahre Weg“. Metamath zum Beispiel mag ich ebenfalls. Allerdings braucht diese „Konkurrenz“ zwischen den Systemen Anführungszeichen. Jedes hat eigene Vor- und Nachteile, und viele Menschen mögen mehrere Systeme, nutzen sie oder tragen zu ihnen bei. Alle können Theoreme mit einer Strenge prüfen, die für Menschen unrealistisch ist.

    • Bugs kann es geben, aber nach meinem Verständnis muss man nur dem Kernel vertrauen.
      Wenn mit „mehreren Library-Stacks, die von anderen Menschen geschrieben wurden“ mathlib gemeint ist, scheint mir das nicht zu stimmen. Denn auch mathlib-Code wird letztlich zu Code kompiliert, den der Kernel verarbeitet.
      Der Paper-Entwurf 0 auf der Website unterstreicht diesen Punkt ebenfalls: Lean ist ein großes Projekt, aber um sicherzustellen, dass akzeptierte Beweise korrekt sind, muss man nur dem Kernel vertrauen. Selbst wenn eine Taktik einen falschen Beweisterm ausgibt, hat der Kernel die Möglichkeit, diesen Fehler zu erkennen, bevor er den Beweis akzeptiert.

    • Der Unterschied ist: In Lean muss man nur dem Kernel vertrauen. Alles andere ist darauf aufgebaut. Wenn der Kernel sound ist, ist auch alles andere sound.
      Das unterscheidet sich stark von normalen Programmiersprachen. In normalen Sprachen können jederzeit Bugs hineingeraten. Und es unterscheidet sich auch stark von Mathematik, in der jedes Lemma einen Fehler enthalten kann.

    • Das Großartige an Theorem-Provern ist: Unter der Annahme, dass der Kernel korrekt ist, kompiliert ein falscher Beweis nicht einmal.
      Bei Beweisen gibt es keine Bugs, die wie in traditioneller Software erst zur Laufzeit auftreten. Es gibt nämlich gar keine Laufzeit.
      Man kann Lean auch als „normale“ Programmiersprache verwenden, und dann besteht das Risiko von Laufzeit-Bugs, aber darum geht es hier nicht.

    • Du verstehst Theorem-Prover falsch. Das ist keine Sache auf dem Niveau von „alle Abstraktionen lecken“. Man muss Libraries nicht vertrauen, nur dem Kernel.
      Dem Kernel zu vertrauen ist zwar nicht trivial, aber gegenüber informellen Beweisen ein großer Sprung. Bei informellen Beweisen muss man tatsächlich den „Libraries“ vertrauen, also der Kultur und dem Wissen anderer Menschen, weil es keine praktische Möglichkeit gibt, alles wirklich bis auf die Axiome herunterzukochen.

  • Ist ZFC tot und lang lebe NF?
    Als Amateurmathematiker, der Mengen hauptsächlich als gemeinsame Sprache benutzt, um andere Dinge zu beschreiben, ist mir nicht ganz klar, welche Implikationen das für die breitere Mathematik hat. Vor allem dann, wenn NF in seiner Nützlichkeit dem bestehenden ZFC und seinen Varianten ähnelt.
    Wird erwartet, dass NF in maschinellen Beweisen genauso populär wird wie ZFC? Die Existenz einer universellen Menge fühlt sich intuitiver an, daher hat zumindest dieser Beweis mein persönliches Interesse an Formalisierung wiederbelebt.

    • Aus naiver Amateurperspektive scheint das relative Konsistenzergebnis, dass jedes ZFC-Modell zu einem NF-Modell erweitert werden kann, NF mindestens so nützlich zu machen wie ZFC.
      Allerdings dürfte NF wohl nicht wesentlich nützlicher werden, außer eines der folgenden Dinge passiert:

      1. Man beweist, dass NF widersprüchlich ist. Dann ist auch ZFC widersprüchlich. Die Sterne am Nachthimmel beginnen einer nach dem anderen zu erlöschen ;)

      2. Man beweist, dass ZFC widersprüchlich ist. Dann bleibt noch die Möglichkeit, dass NF konsistent ist. Da sollte man auf Glück hoffen.

      Natürlich kann es gut sein, dass ich praktischere „Quality-of-Life“-Vorteile von NF übersehe, etwa dass man über echte Klassen sprechen kann oder dass man Russells Paradox durch stratifizierte Formeln vermeidet.

    • Es gibt überhaupt keine Absicht, NF als unabhängiges Grundlagen­system zu pushen. NF ist ein ziemlich ungewöhnliches System.
      Wenn jemand das trotzdem vorantreiben möchte, sagt dieses Konsistenzergebnis immerhin, dass es zumindest nicht riskanter ist, als in ZFC auf einen Widerspruch zu stoßen.

  • Das gefällt mir wirklich.
    Ich frage mich, ob das am Ende zu kollaborativen Beweisen und „Bugfixes“ führt, sodass Mathematik zu einem ähnlichen Prozess wird wie Code auf GitHub.

  • Ich wünschte, ich hätte genug freie Zeit, um das mathlib-Projekt zu verfolgen. Wirklich großartig.
    Gibt es eine Möglichkeit, sich auch nur ganz locker zu beteiligen?

  • Ich bin nicht aus diesem Fachgebiet, aber gab es da nicht den Satz von Gödel, wonach jedes hinreichend starke System seine eigene Konsistenz nicht zeigen kann?

    • Gemeint ist vermutlich Gödels Unvollständigkeitssatz: https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...
      Allerdings kann System X zwar seine eigene Konsistenz nicht beweisen, ein stärkeres System Y kann aber die Konsistenz von X beweisen. Und ein anderes, noch stärkeres System kann wiederum die Konsistenz von Y beweisen. So entsteht eine Kette, in der jedes System die Konsistenz eines schwächeren Systems beweist.
      Das beweist nicht, dass dieses System absolut konsistent ist. Denn wenn Y widersprüchlich ist, kann es sowohl beweisen, dass X konsistent ist, als auch, dass X widersprüchlich ist. Trotzdem hat das einen Wert. Schließlich ist einer der Gründe, warum wir Y verwenden, dass wir darin keinen Widerspruch kennen. Formale Systeme können oft auf subtile Weise widersprüchlich sein; daher ist „konsistent unter der Annahme, dass ein anderes System konsistent ist“ viel besser als „gar kein Konsistenzbeweis“.
    • Hier beweist das System nicht seine eigene Konsistenz. Die Konsistenz wird in einem anderen, stärkeren System bewiesen.
    • Interessant ist, dass man selbst dann nichts allein daraus weiß, wenn ein starkes System seine eigene Konsistenz beweisen könnte.
      Auch ein widersprüchliches System kann seine eigene Konsistenz beweisen. Selbst wenn ein System also einen Beweis dafür enthält, dass es selbst konsistent ist, weiß man weiterhin nicht, ob es tatsächlich konsistent ist.
    • Diesen Beweis kann man als „Wenn Lean 4 konsistent ist, dann ist auch New Foundations konsistent“ verstehen. Das widerspricht Gödels Unvollständigkeitssatz nicht.
    • Das System hier scheint nicht zu versuchen, seine eigenen Grundannahmen zu beweisen, sondern auf einer Menge bestehender Annahmen aufzubauen. Der Satz, an den du denkst, dürfte wohl nicht anwendbar sein.

  • Auch die Reddit-Diskussion, an der einer der Ersteller beteiligt ist, ist lesenswert 0

    https://old.reddit.com/r/math/comments/1ca6bj8/new_foundatio...