Mathematik für die Woche – Lösung

[1unitedpower]

nein, das $$\equiv$$ steht nicht für identisch, sondern für äquivalent

das ist dann aber sehr irreführend.

Gleichheit wird in der Mathematik sowieso sehr oft übergangen und nur informell behandelt. Im Detail beschäftigen sich eigentlich nur die mathematischen Grundlagen-Disziplinen damit, wie die Mengenlehre, Typ-Theorie und Kategorien-Theorie. Bei nLab gibt es einen kurzen Artikel über verschiedenen Perspektiven zu dem Thema.

Man könnte meinen über Gleichheit sei längst alles gesagt, aber es ist noch gar nicht so lange her da erfasste ein Raunen die moderne mathematische Gesellschaft, weil jemand folgenden Satz gesagt hat:

In other words, identity is equivalent to equivalence. In particular, one may say that “equivalent types are identical”. However, this phrase is somewhat misleading, since it may sound like a sort of “skeletality” condition which collapses the notion of equivalence to coincide with identity, whereas in fact univalence is about expanding the notion of identity so as to coincide with the (unchanged) notion of equivalence.

Das ist eine Idee einer neuen mathematischen Grundlagen-Disziplin, die sich "Univalent Foundations" schimpft. Manche Mathematiker glauben sogar, dass sie das Potenzial hat die Mengenlehre als defakto Fundament der Mathematik abzulösen. Auf jeden Fall scheint das gerade ein heißes Eisen zu sein.

Das obige Zitat ist ein Auszug aus dem Homotopy Type Theory Buch, das ist gewissermaßen die Einführungsliteratur für alle, die sich mit dem Thema befassen. Ich bilde mir ein etwas Ahnung von Typ-Theorie zu haben, und kann wissenschaftliche Veröffentlichungen in dem Bereich recht gut lesen, aber das Buch liegt jetzt schon seit mehr als einem Jahr auf meinem Nachttisch und beschäftigt mich. Es ist keine leichte Kost, aber spannender als jeder Stephen King Roman (zumindest für manche Mathe-Nerds).

Für Informatiker ist das übrigens auch interessant, weil die nächste Generation von Beweis-Assistenten und funktionalen Programmiersprachen auf diesen Grundlagen aufbauen wird. Prototypen gibt es sogar schon. Agda scheint da gerade führend zu sein.