Die Bourbaki-Gruppe, die in der Mitte des vorherigen Jahrhunderts mit einer Reihe von Lehrbüchern die reine Mathematik auf eine gemeinsame Grundlage stellen wollte, ging nicht davon aus, dass Mathematik komplett formalisiert werden könne. Dementsprechend machte sie sich auch keine Gedanken darüber, ob ein Ansatz mit Blick auf Formalisierbarkeit effizienter sein könnte als ein anderer. Sie selbst erwähnten in ihrem Buch, dass eine Formalisierung ihrer Definition der 1 hunderte, wenn nicht tausende Symbole benötigen würde.

Berühmt wurde das durch einen Text des Logikers A.R.D.Mathias aus den 80er Jahren (veröffentlicht 1992 in “The Mathematical Intelligencer”). Der hatte seinen Kollegen Robert Solovay die genaue Anzahl der benötigten Symbole ausrechnen lassen, sie betrug 4523659424929.
Ihm ging es dabei aber nicht um die Unmöglichkeit einer völligen Formalisierung, sondern darum aufzuzeigen, dass Bourbaki durch einen ungeschickt gewählten Ansatz eine für die Formalisierung wenig geeignete Definition gewählt hätte. Überhaupt war der Text eher eine Abrechnung mit Bourbaki, in der es vor allem um die von ihm Bourbaki zugeschriebene Vernachlässigung der mathematischen Logik durch die meisten Mathematiker ging. (Sanford Segal sprach in der Zentralblatt-Besprechung von einem “mit leidenschaftlicher Rhetorik verfaßten wütenden Text”.)
Bourbaki hatten in ihrem in den 50er Jahren verfaßten Band zur Mengenlehre diese zur Grundlegung der gesamten Mathematik entwickelt. Dabei verwandten sie einen von Hilbert vorgeschlagenen Ansatz für die Logik erster Ordnung, der als vergleichsweise kompliziert gilt. (Diese Komplikationen und einige weitere Entwicklungen wie schlecht geschriebene Lehrbücher sollen dann angeblich dazu geführt haben, dass die formale Logik in den französischen Prüfungen für angehende Sekundarschullehrer nicht mehr vorkam, so jedenfalls Mathias.) Mathias zeigte, dass sich die Komplikationen von Bourbakis Ansatz so kumulieren, dass bereits die Definition der Kardinalzahl 1 in ihrem Formalismus die Länge 4523659424929 hätte. Die Berechnung von 1+1=2 hätte die Länge 19,516,572,617,436,743,593. (In einer späteren Ausgabe der Mengenlehre (1970) hatte Bourbaki einen anderen Zugang über “Kuratowski-Paare” gewählt, mit dem die formale Realisierung allerdings noch viel aufwändiger wurde: die Definition der 1 benötigte nun 2409875496393137472149767527877436912979508338752092897 Symbole.)
In einem Folgeartikel, eigentlich einer Replik auf die Zentralblatt-Besprechung, stellte Mathias damals die verschiedenen mathematischen Ansätze noch in einen ideologischen Zusammenhang: “Platonismus=Katholizismus, Intuitionismus=Protestantismus, Formalismus=Atheismus, Kategorientheorie=dialektischer Materialismus”. Diese Zuordnung ist freilich nicht einmal kompatibel mit seinen Ausfûhrungen unmittelbar davor im selben Artikel, wo er einige Mühe darauf verwendet, die (ja wohl am ehesten dem Formalismus und teils natürlich auch der Kategorientheorie nahestehende) Bourbaki-Gruppe als von Juden und Protestanten dominiert darzustellen. (Der Folgeartikel ist hier und er ist auch sonst eine recht seltsame Replik auf die Zentralblatt-Besprechung, die deren einzelne Punkte zu widerlegen versucht. Zum Beispiel hatte der Rezensent “the author’s cavalier attitude towards history” daran festgemacht, dass dieser Klein und Poincaré implizit in unterschiedliche Generationen, Klein jedoch in dieselbe Generation mit Noether und Weyl, aber nach Minkowski eingeordnet habe. Das widerlegt Mathias dann in seiner Replik, indem er eine Generationseinteilung nach Sterbe(!)jahren mit der Bruchstelle in 1920 vornimmt. Es sei ja schließlich beliebig, ob man das Geburts- oder Sterbejahr zur Einteilung heranziehe und eigentlich gäbe es sowieso keine Generationen.)

Der Vollständigkeit halber sei hier erwähnt, dass die (effiziente) Formalisierung der Mathematik inzwischen rasante Fortschritte macht, einen guten Überblick dazu gibt Thomas Hales’ Bourbaki-Vortrag von 2014.

Aktuell wieder in die Diskussion gekommen ist die Geschichte jetzt durch eine Frage von John Baez auf mathoverflow. Als eine der Antworten wurde die Zahl dort noch einmal von Alex Nelson mit einem Haskell-Programm überprüft. (“ For what it’s worth, computing the size of 1 was nearly instantaneous, whereas computing the size of “1+1=2” took about 7 minutes and 30 seconds.”)

Brilliant! Hopefully we make as much fun soonish of what is now the standard categorical definition of a symmetric monoidal category, which is still stuffed with the same kinds of absurdity…

kommentierte Bob Coecke Baez’ Beitrag auf Twitter.

Kommentare (4)

  1. #1 Karl Mistelberger
    mistelberger.net
    5. Mai 2020

    > “ For what it’s worth, computing the size of 1 was nearly instantaneous, whereas computing the size of “1+1=2” took about 7 minutes and 30 seconds.”

    The relation “1+1=2” can be computed, and found to have a length of 22,411,322,875,029,037,193,545,441,224,646,148,573,589,725,893,763,139,344,694,162,029,240,084,343,041

    or approximately 2.24113228750290371×10^76

  2. #2 Automatic Mouse and Keyboard Crack
    https://crackedpedia.com/automatic-mouse-and-keyboard-crack/
    10. Mai 2020

    good and very suitable application that allows you to go the mouse pointer over the road you designate, and also reveal where in fact the click will be produced, which can only help to handle a number of very diverse jobs.https://crackedpedia.com/automatic-mouse-and-keyboard-crack/

  3. #3 Microsoft Word Crack
    22. Juni 2020

    Microsoft never released a complete version of the free office, not even a very old and outdated version. In the absence of hacking software, the best practice are to download a free trial version. https://procracksoft.com/microsoft-word-v15-27-0-crack-download/

  4. #4 Range rover workshop dubai
    https://munichmotorworks.ae/
    27. Dezember 2022

    John Auto Spare Parts Co. LLC. was established in 1998 as an independent automotive spare parts company. Specializing in new Mercedes and BMW Original Equipment(OE), Original Equipment Manufacturer (OEM) and Aftermarket parts we can offer the full range of parts for any Mercedes and BMW passenger car.