Advanced course in foundations of mathematics (2016/2017)

Codice insegnamento
4S001104
Docenti
Peter Michael Schuster, Iosif Petrakis
Coordinatore
Peter Michael Schuster
crediti
6
Settore disciplinare
MAT/01 - LOGICA MATEMATICA
Lingua di erogazione
Inglese
Periodo
II sem. dal 1-mar-2017 al 9-giu-2017.

Orario lezioni

II sem.
Giorno Ora Tipo Luogo Note
mercoledì 14.30 - 17.30 lezione Aula M dal 1-mar-2017  al 30-apr-2017
giovedì 11.30 - 14.30 lezione Aula B dal 16-mar-2017  al 9-giu-2017

Obiettivi formativi

Introdurre gli studenti all'Homotopy Type Theory, un nuovo approccio ai fondamenti della matematica che fornisce un punto d'incontro fra logica, computer science e matematica.

Al termine dell'insegnamento lo studente dovrà essere in grado di produrre argomentazioni e dimostrazioni rigorose e di leggere articoli e testi (anche avanzati) relativi alla Homotopy Type Theory.

Programma

Homotopy Type Theory (HoTT) costituisce un nuovo approccio ai fondamenti della matematica, che ha mostrato sorprendenti connessioni fra la Teoria dei Tipi Intensionale (ITT) di Martin-Löf e la teoria classica dell'omotopia.

Innanzitutto daremo un'introduzione ad ITT e un'analisi dettagliata dell'assioma di path-induction di Martin-Löf (l'assioma di eliminazione dell'uguaglianza) che si era mostrato di difficile comprensione prima dell'interpretazione omotopica di Voevodsky dei tipi come spazi, o meglio, come infinity groupoids. Attraverso questa interpretazione, ITT soddisfa un certo principio di naturalezza che rende il suo sviluppo inaspettatamente elegante. Questa naturalezza è preservata dall'estensione di ITT tramite il cosiddetto axiom of univalence di Voevodsky, un principio di particolare forza e generalità, le cui conseguenze verranno studiate dettagliatamente. Nell'ultima parte del corso presenteremo importanti teoremi sui path spaces di higher inductive types, quali ad esempio high circle e higher spheres.

Non è richiesta alcuna conoscenza preliminare di teoria dell'omotopia, teoria delle categorie o logica matematica, ma soltanto abilità operative di base in algebra e topologia.

Parole chiave: Martin-Löf Type Theory, Univalence Axiom, Higher Inductive Types, Synthetic Homotopy Theory

Al di fuori del monte ore dell'insegnamento, che comprende sia lezioni frontali che esercitazioni in aula, sono assegnati esercizi da svolgere a casa che vengono raccolti e corretti dal docente oppure discussi durante le ore di esercitazione.

Testi di riferimento
Autore Titolo Casa editrice Anno ISBN Note
The Univalent Foundations Program Homotopy Type Theory: Univalent Foundations for Mathematics. Institute for Advanced Study 2013 Available on-line: https://homotopytypetheory.org/book/

Modalità d'esame

L'esame consiste in una sola prova orale a quesiti aperti e voti in trentesimi. Le modalità d’esame non sono differenziate fra frequentanti e non frequentanti.

L'esame ha lo scopo di verificare la piena maturità circa le tecniche dimostrative e la capacità di leggere e comprendere argomenti avanzati della Homotopy Type Theory.

Opinione studenti frequentanti - 2015/2016


Statistiche per i requisiti di trasparenza (Attuazione Art. 2 del D.M. 31/10/2007, n. 544)

I dati relativi all'AA 2016/2017 non sono ancora disponibili