Daily Archives: March 10, 2019

#HoTT Homotopy type theory la nouvelle fondation des mathématiques du 21eme siècle

Autrement qu'être Mathesis uni∜ersalis Problema Universale Heidegger/Husserl être/conscience : plan vital-ontologique vs plan spirituel d'immanence CLAVIS UNIVERSALIS HENOSOPHIA PANSOPHIA ενοσοφια μαθεσις

Cet article trace le parallèle entre le livre « Homotopy type theory Univalent foundations »:

https://aperiodical.com/2013/06/homotopy-type-theory-a-new-foundation-for-21st-century-mathematics/

The HoTT Book

Et les « Principia mathematica » de Whitehead et Russell, qui fonde les mathématiques du siècle dernier, et qui est ici :

https://quod.lib.umich.edu/u/umhistmath/aat3201.0001.001/23?view=image&size=100

(En forme très aisée pour la lecture)

https://ncatlab.org/nlab/show/Principia+Mathematica

L’article rappelle qu’il a fallu aux PM 379 pages pour prouver que 1+1=2, tandis que les 250 premières pages du livre HoTT suffisent pour déduire les groupes d’homotopie des sphères à partir des bases de la théorie des types.

Cette page relie HoTT aux théorèmes d’incompletude De Godel, qui datent de 1931, vingt après les Principia mathematica qui sont de 1910:

https://cstheory.stackexchange.com/questions/22130/homotopy-type-theory-and-gödels-incompleteness-theorems

Le langage formel des Principia mathematica est identique à la théorie des types, inventée par Russell :

https://www.sciencedirect.com/topics/computer-science/principia-mathematica

http://www.nuprl.org/documents/Constable/PrincipiaArticle.pdf

https://philosophy.stackexchange.com/questions/5951/what-does-the-type-theory-in-the-principia-mathematica-and-that-of-contemporary

La notation, le langage formel, des Principia peut être étudié ici :

https://plato.stanford.edu/entries/pm-notation/

View original post