Das 21. Jahrhundert habe nun neue Kritik an der Mengenlehre und einen neuen Kandidaten für ihre Rolle: „univalente Grundlagen“.
Das Programm der univalenten Grundlagen besteht darin, die Homotopietheorie zur Interpretation der Typentheorie von Martin-Löf zu verwenden und dann das sogenannte “Univalenzaxiom” hinzuzufügen, das grob gesagt isomorphe Strukturen identifiziert. Das Ergebnis wird als „unvereinbar mit konventionellen (vermutlich mengen- und kategorientheoretischen) Grundlagen“ (Awodey) und „eine völlig neue Grundlage“ der Mathematik (Voevodsky) bezeichnet.
Vladimir Voevodksy hat 2014 in einem sehr persönlichen Text (The Origins and Motivations of Univalent Foundations) erzählt, wie ihn zahlreiche Fehler in eigenen und von ihm verwendeten Arbeiten dazu geführt hätten, nach neuen Grundlagen für die Mathematik zu suchen.
Dies ist also das dringende neue Problem, mit dem mathematische Praktiker auf diesem Gebiet konfrontiert sind: Wie können wir sicher sein, dass unsere Beweise korrekt sind? Bisher waren verschiedene soziologische Kontrollen ausreichend gewesen – Beweise wurden sorgfältig von der Gemeinschaft geprüft; Mathematiker mit hohem Ansehen waren im Allgemeinen zuverlässig; und so weiter – aber diese Kontrollen waren anscheinend überholt.
Die Notwendigkeit, dieses Problem anzugehen, führt zu einem neuen Ziel – einer systematischen Methode der Beweisprüfung – und es erscheint vernünftig, auch dieses Ziel als „grundlegend“ einzustufen.
Die Grundlagen der Mengenlehre entstanden aus der Einbettung der Standardmathematik in die Mengenlehre. Dafür muß man, wie es Voevodsky ausdrückt, nur noch „lernen, wie man Aussagen über einige grundlegende mathematische Konzepte in Formulierungen der ZFC-Mengenlehre übersetzt, und dann anhand von Beispielen glauben, dass der Rest der Mathematik auf diese wenigen grundlegenden Konzepte reduziert werden kann“.
Für die univalenten Grundlagen hat man die Einbettung in formalen Begriffen ausgedrückt. Trotz seiner metamathematischen Tugenden ist dieses formale System kein System, in dem ein Mathematiker tatsächlich etwas beweisen möchte. Tatsächlich basiert unser Vertrauen in einen formellen Beweis normalerweise auf unserem Vertrauen in den informellen Beweis, kombiniert mit unserer informierten Überzeugung, dass alle informellen Beweise auf diese Weise formalisiert werden können. Dagegen sind die Anforderungen an die Beweisprüfung ganz andere: hier braucht man ein System, das formelle Beweise darstellen kann, ein Werkzeug, das in der täglichen mathematischen Arbeit eingesetzt werden kann.
Maddy diskutiert dann verschiedene Beweisprüfungsverfahren und welche Rolle univalente Grundlagen oder andere Grundlagen dort spielen können.
Zusammenfassend scheinen Risk Assessment, Meta-mathematical Corral, Generous Arena und Shared Standard weiterhin die Heimstatt der mengentheoretischen Grundlagen zu sein. Es bleibt Proof Checking, das neue Ziel, als Argument für univalente Grundlagen. Das Versprechen ist, dass gewöhnliches mathematisches Denken einfach und direkt in CIC ausgedrückt werden wird und die Gültigkeit von Beweisen dann automatisch in COQ überprüft, und dass die Homotopietypentheorie einen Rahmen für zuverlässiges Proof Checking bietet:
„Ich mache jetzt meine Mathematik mit einem Beweisassistenten. Ich habe viele Wünsche, wie dieser Beweisassistent besser funktionieren könnte, aber zumindest muss ich nicht nach Hause gehen und mir Sorgen machen, dass ich bei meiner Arbeit einen Fehler gemacht habe. Ich weiß, wenn ich etwas getan habe, habe ich es getan, und ich muss nicht später wieder darauf zurückkommen, noch muss ich mir Sorgen machen, ob meine Argumente zu kompliziert sind oder wie ich andere von ihrer Richtigkeit überzeugen kann, dass meine Argumente richtig sind. Ich kann dem Computer einfach vertrauen.“ (Voevodsky)
Ich denke, wir können uns alle einig sein, dass dies ein sehr attraktives Bild ist, selbst wenn es sich nur auf Bereiche der Mathematik anwenden ließe, die für diese Art der Konzeptualisierung geeignet sind.
Letzte Kommentare