Cos’è una dimostrazione? È la nozione qualificante del pensiero matematico, ma essa stessa non è stata oggetto di uno studio matematico se non a partire dal secolo scorso. Nacque in un contesto geometrico ma è solamente quanto si giunse all’aritmetizzazione della logica, a partire da Hilbert e Gödel, che venne finalmente trattata rigorosamente, introducendo tra l’altro i concetti fondamentali su cui si appoggerà la futura rivoluzione informatica. Una dimostrazione oggi è concepita come l’altra faccia di un algoritmo; e ogni principio di induzione corrisponde ad un meccanismo di ricorsione. Intendiamo discutere vari esempi di dimostrazioni e degli algoritmi soggiacenti, ma anche alcune conseguenze pratiche della loro mancanza. Parleremo infine del sistema che ha permesso al matematico russo Vladimir Voevodsky, medaglia Fields nel 2002 di porre su basi rigorose alcuni dei suoi risultati. Questo sistema, chiamato Teoria Omotopica dei Tipi, offre una nuova possibile risposta alla questione dei Fondamenti della Matematica. Il matematico Hales, che ha risolto nel 1998 il problema di Keplero, così si è espresso sulla Teoria di Voevodsky: “If you want to ask how profound his work is, that’s how profound it is. It changes the very meaning of what the equals sign means in mathematics.”
#palazzofranchetti
12 авг 2024
