Mathematik, so liest man es gelegentlich in populärwissenschaftlicher Literatur, sei ein Spiel mit Zeichen, die nach beliebig wählbaren Regeln (Axiomen) manipuliert werden können. Die Wahl der jeweils gültigen Axiomatik werde nicht von äußeren Gegebenheiten diktiert, sondern von den Mathematikern in einem quasi politischen Akt demokratisch entschieden.
Man sollte also meinen, dass die Wahl des “richtigen” Axiomensystems, gerade wenn es um die ganz allgemeinen für alle Mathematiker relevanten Grundlagen der Mengenlehre und Logik geht, von enormer Bedeutung und mathematikintern heiß umstritten sein müsste.
Tatsächlich haben solche Auseinandersetzungen über Axiomensysteme in der Vergangenheit aber kaum stattgefunden. Der einzige Grundlagenstreit, der tatsächlich eine gewisse Publizität erreichte, war der in den 20er Jahren zwischen Intuitionismus und Formalismus – und das wohl auch nur deshalb, weil er sich mit eigentlich politisch motivierten Auseinandersetzungen vor allem zwischen Brouwer und Hilbert überlagerte. Zwar gab es damals zahlreiche Diskussionen und auch Veröffentlichungen zum Thema, um die eigentlichen mathematischen Details der neuen Grundlegung ging es dabei aber kaum, zumal diese von Brouwer nur auf Holländisch publiziert und wohl von kaum jemandem verstanden worden waren. Die einzige praktische Konsequenz des Intuitionismus für die Mathematik war wohl, dass Brouwer an der Amsterdamer Universät niemals Vorlesungen über seine topologischen Resultate oder den Brouwerschen Fixpunktsatz hielt, weil sie mit seinen philosophischen Ansichten nicht mehr in Übereinstimmung zu bringen waren.[1]
Kurz: man konnte mit den neuen Axiomen weniger beweisen als mit den gebräuchlichen der Zermelo-Frenkel-Mengenlehre mit Auswahlaxiom (ZFC), auf denen heute eigentlich die gesamte Mathematik aufbaut.
Konkurrenz erwächst der Zermelo-Frenkel-Mengenlehre nun seit einigen Jahren durch die Homotopietypentheorie (HoTT), deren Grundidee es wohl ist, Typen von Objekten durch Homotopietypen topologischer Räume zu repräsentieren.
Die Protagonisten (am bekanntesten wohl Wladimir Wojewodski) argumentieren, dass dieser Zugang für die Erstellung computerüberprüfbarer Beweise besser geeignet sei – das wird aber wohl nicht von allen Experten so gesehen.
Jedenfalls, und das war jetzt der Anlaß dieses Artikels, scheint sich das Thema HoTT vs. ZFC zu einem veritablen Grundlagenstreit zu entwickeln. Auf Google+ findet sich aktuell ein polemischer Artikel zu Konflikten auf der “Foundations of Mathematics”-Mailingliste und auch im n-Category Café wird das Thema kontrovers diskutiert.
Bisher habe ich freilich noch von keinem relevanten mathematischen Lehrsatz gehört, der in dem einen Axiomensystem richtig wäre und bei dem anderen Zugang aber nicht. Und solange es dabei bleibt, muss man sich als Mathematiker über den neuen Grundlagenstreit wohl genauso wenige Gedanken machen wie über die früheren.
Kommentare (7)