1) Appunti del docente, accessibili online, con relativa bibliografia;
2) per approfondimenti, si possono consultare:
(i) J.Y.Girard, Proof Theory and Logical Complexity, Bibliopolis Napoli
1987;
(ii) A.S.Troelstra, H.Schwichtenberg, Basic Proof Theory, Cambridge
University Press, Cambridge 2000 (2nd ed.);
(iii) S.Negri and J. von Plato, Structural Proof Theory, Cambridge 2001;
(iv) M.H.Sorensen, P.Urczyn, Lectures on the Curry-Howard Isomorphism,
Amsterdam-New York 2006;
(iii) H.Schwichtenberg, S.S.Wainer, Proofs and Computations, Cambridge
2012.
Obiettivi Formativi
Approfondire i fondamentali risultati sul concetto di 'dimostrazione',
emersi a partire dagli anni Trenta, e incentrati in particolare sulle tecniche dell' 'eliminazione delle cesure' e della 'normalizzazione'.
Prerequisiti
Logica 1 (12 CFU), a livello di laurea triennale in Filosofia
Metodi Didattici
Lezioni frontali ed eventuali esercitazioni; partecipazione al seminario ricerche in corso
Altre Informazioni
Lo studente deve frequentare almeno 2/3 delle lezioni. Lo studente part-time (o che abbia articolari esigenze) deve contattare direttamente il docente. Consultare la pagina web del docente sul sito UNIFI o scrivere al docente
andrea.c a n t i n i @ u n i f i . i t .
Inoltre per cambiamenti orario e ricevimento dell'ultimo minuto, v.
avvisi sul sito DILEF.
Modalità di verifica apprendimento
Esame orale, teso a verificare: (i) la padronanza delle principali nozioni teoriche e del lessico disciplinare adeguato; (ii) la capacità di applicare le tecniche corrispondenti nell'esecuzione di esercizi.
L'esame dura circa 45 minuti; il colloquio consta di tre argomenti, uno scelto dal discente. Il voto risulta dalla media dei voti riportati nella trattazione dei singoli argomenti. L'esame orale deve verificare che il discente padroneggi le nozioni fondamentali del corso e qualche dimostrazione di risultati fondamentali.
Programma del corso
1) Complementi di logica proposizionale e predicativa (per es. forme
normali, completezza funzionale, teoremi di Skolem e Herbrand; logica
monadica).
2) Introduzione alla teoria della dimostrazione: l'approccio analitico alla
logica mediante i calcoli logici di Gentzen. Prova dell’Hauptsatz a livello elementare e proprieà della sottoformula.
Interpolazione: il lemma di Maehara, il teorema di Craig e sue conseguenze.
3) Hauptsatz e astrazione: il paradosso di Russell e la teoria della dimostrazione; il calcolo logico di Grishin.
4) Introduzione al lambda calcolo tipato. Nozioni di base e proprietà fondamentali. Normalizzazione forte e sue applicazioni.