Zwei Diskussionen bei Mathoverflow (Are categories special, foundationally? und Category theory and set theory: just a different language, or different foundation of mathematics?) werfen wieder einmal die Frage nach den „richtigen“ Grundlagen für die Mathematik auf: sollte die Axiomatik der Mathematik auf der Mengenlehre oder auf der Kategorientheorie aufbauen?
Es gibt dort eine Reihe interessanter Diskussionsbeiträge, zum Beispiel diesen Auszug aus einem Beitrag von Timothy Chow:
Befürworter anderer Grundlagen als der Mengenlehre betonen oft, was Maddy “wesentliche Führung” nennt. Das Argument ist, dass die Kategorientheorie genauer widerspiegelt, wie Mathematiker tatsächlich denken, wie sie tatsächlich Mathematik betreiben oder welche mathematischen Strukturen wesentlich sind. Das mag richtig sein (obwohl die Mengenlehre in dieser Richtung mehr Ressourcen hat, als ihre Gegner manchmal anerkennen), aber diese alternativen Grundlagen übertreffen die Mengenlehre nicht immer, wenn es um andere Rollen geht, die Grundlagen zukommen sollen. Zum Beispiel gibt es eine “Risikobewertung” – welche Axiome braucht man wirklich, um die Theoreme abzuleiten, und sind diese Axiome “sicher”? Oder “großzügige Arena” – vielleicht sind die vorgeschlagenen alternativen Grundlagen gut für die Homotopietheorie, aber nicht so geeignet für die numerische Lösung partieller Differentialgleichungen oder die Berechnung kleiner Ramsey-Zahlen.
Die Mengenlehre hat im 19. und 20. Jahrhundert bemerkenswerte Arbeit geleistet, indem sie die Mathematik vereinheitlicht, alles auf eine gemeinsame Grundlage gestellt und einen Rahmen für die Analyse von Fragen der Konsistenz und Beweisbarkeit geschaffen hat. Heutzutage ist es einfach, diese Leistung als selbstverständlich zu betrachten und anzunehmen, dass die gesamte Mathematik “sicher” ist und dass wir immer einen Weg finden werden, wenn wir Methoden aus einem Zweig der Mathematik in einem anderen verwenden wollen. Wenn man diese Haltung einnimmt, wird “Risikobewertung” irrelevant und “großzügige Arena” und “gemeinsamer Standard” verlieren an Bedeutung – ich kann mich einfach darum kümmern, Grundlagen für die Art von Mathematik zu finden, die mir wichtig ist, und wenn meine Grundlagen für die Mathematik meines Kollegen zu umständlich sind, dann ist das sein Problem und nicht meins.
In beiden Diskussionen wird auf einen Artikel von Penelope Maddy (What do we want a foundation to do? Comparing set-theoretic, category-theoretic and univalent approaches) verwiesen, der versucht, diese Frage für den „arbeitenden Mathematiker“ systematisch anzugehen, also zunächst zu fragen, was man von „Grundlagen der Mathematik“ erwarten könnte und dann unter diesen möglichen Aspekten die Ansätze zu vergleichen. (Der Artikel ist im November 2019 veröffentlicht worden, obwohl er von der äußeren Form Jahrzehnte älter aussieht.)
Maddy geht dort zunächst sehr ausführlich auf die Geschichte der mathematischen Grundlagen bis zum Aufkommen der mengentheoretischen Axiomatisierung ein und definiert dort angekommen erst einmal, was man von „Grundlagen“ eigentlich erwarten sollte:
Mein Vorschlag ist also, dass wir die Behauptung, dass die Mengenlehre eine (oder ‘die’) Grundlage für die Mathematik ist, durch eine Handvoll genauerer Beobachtungen ersetzen: Die Mengenlehre bietet ein Risk Assessment für mathematische Theorien, eine Generous Arena, wo die Zweige der Mathematik in einem vereinheitlichten Setting mit einem Shared Standard für Beweise verfolgt werden können, und einen Meta-mathematical Corral, so dass formale Techniken auf die gesamte Mathematik gleichzeitig angewendet werden können. Ich habe kein Argument dafür angeführt, dass diese Errungenschaften als „grundlegend“ verstanden werden müssen, aber dies scheint mir im Einklang mit der gewöhnlichen Verwendung des Begriffs zu sein. Ich nehme als gegeben, dass diese Dinge von offensichtlichem Wert für die Mathematik sind.
Nach der Historie der Entwicklung der Mathematik aus der Mengenlehre geht sie dann ausführlich auf die von Saunders Mac Lane propagierte kategorientheoretische Grundlegung der Mathematik ein:
Was war also falsch an mengentheoretischen Grundlagen? Der erste Einwand ist, dass sich die Kategorientheorie mit unbegrenzten Kategorien befasst, wie der Kategorie aller Gruppen oder der Kategorie aller Kategorien oder der Kategorie aller mathematischen X, aber nichts dergleichen kann im Universum der Mengen gefunden werden. Grothendieck hat dieses Problem überwunden, indem er eine immer größere Folge von ‘lokalen Universen’ postuliert und feststellt, dass jede kategorientheoretische Aktivität in einem ausreichend großen dieser Universen ausgeführt werden kann. In mengentheoretischen Begriffen bedeutet dies, unerreichbare Kardinalzahlen hinzuzufügen, die kleinsten der großen Kardinalzahlen jenseits der ZFC-Mengenlehre. Mit anderen Worten, das Risiko von Grothendiecks Kategorientheorie ist nicht größer als das von ZFC + unerreichbaren Kardinalzahlen. Wenn Risk Assessment das grundlegende Ziel ist, ist die Mengenlehre immer noch in Ordnung. Surrogate für die Kategorien sind auch in der Generous Arena der Mengenlehre verfügbar, so dass Shared Standard und Metamathematic Corral ebenfalls in Ordnung zu sein scheinen.
Neben diesem den arbeitenden Mathematiker kaum tangierenden Vorbehalt gab es aber noch ein praktischeres zweites Argument gegen Mengen und für Kategorien:
Die Hoffnung bestand darin, eine Grundlage zu finden, welche die Mathematiker zu den wichtigen Strukturen führt und diese strikt unter Bezugnahme auf ihre mathematisch wesentlichen Merkmale charakterisiert. Eine solche Grundlage wäre tatsächlich nützlich für Mainstream-Mathematiker in ihrer täglichen Arbeit. Sie wäre nicht für diese weitgehend irrelevant wie die Mengenlehre; sie würde Essential Guidance liefern. Ihre Befürworter argumentierten, dass die Kategorientheorie genau dies für die algebraische Geometrie und die algebraische Topologie geleistet habe.
Maddy argumentiert dagegen, dass ja auch kaum jemand behauptet habe, die Mathematik wäre besser dran, wenn alle Mathematiker wie Mengentheoretiker denken würden. Natürlich sollten algebraische Geometer oder algebraische Topologen nicht in mengentheoretischen statt kategorientheoretischen Begriffen denken. Andererseits wäre es jedoch unvernünftig zu behaupten, dass Analytiker oder Mengentheoretiker besser in kategorietheoretischen Begriffen denken sollten. Das habe durchaus auch Mac Lane so gesehen. Beide Ansätze hätten ganz unterschiedliche Ziele. Die Mengenlehre biete Risk Assessment, Generous Arena, Common Standard und Meta-mathematical Corral und erledige diese Aufgaben auch im Kontext kategorietheoretischer Grundlagen, die Kategorientheorie biete Essential Guidance, aber nur für die Zweige der Mathematik mit einigermaßen algebraischem Charakter.
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