Der Code der Mathematik: Beweis und Wahrheit

Motiviert durch aktuelle Entwicklungen in der abha?ngigen Typentheorie und bei Unendlichkategorien pra?sentiert dieses Buch die Ideengeschichte der Begriffe Wahrheit, Beweis, Gleichheit und A?quivalenz. Neben ausgewa?hlten Ideen von Platon, Aristoteles, Leibniz, Kant, Frege und anderen werden Resultate von Go?del und Tarski u?ber Unvollsta?ndigkeit, Unentscheidbarkeit und Wahrheit in deduktiven Systemen und ihren semantischen Modellen vorgestellt. Der Hauptgegenstand dieses Textes ist die abha?ngige Typentheorie und neuere Entwicklungen in der Homotopy Type Theory. Diese Theorien beinhalten Identita?tstypen, die neue Mo?glichkeiten fu?r Gleichheit, Symmetrie, A?quivalenz und Isomorphie auf konzeptuelle Weise ero?ffnen. Die Interaktion von Typentheorie und Unendlichkategorien ist ein neues Paradigma fu?r eine strukturelle Sichtweise auf die Mathematik. Sie fo?rdert auch den neuen Trend zur Formalisierung von Mathematik in Form von Beweisassistenten.