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;
(v) 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
Le lezioni sono a carattere frontale; prevedono esercitazioni e frequenza del seminario di 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 di 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 i calcoli logici di Gentzen e le loro proprietà fondamentali, applicandole a qualche semplice problema.
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 (formulazione G3). Il caso
proposizionale intuizionista (un calcolo con la proprietà di terminazione).
Prova dell’Hauptsatz a livello elementare e proprieà della sottoformula.
Interpolazione: il lemma di Maehara, il teorema di Craig e qualche
applicazione. Hauptsatz e contenuto computazionale. Preliminari formali.
Maggiorazione di derivazioni e intepretazioni asimmetriche. Il teorema di
Parsons-Mints-Takeuti e suoi raffinamenti. Hauptsatz e astrazione: il
paradosso di Russell e la teoria della dimostrazione. Un sistema classico
predicativo. Un sistema non classico impredicativo (calcolo logico di
Grishin). Introduzione al lambda calcolo tipato. Nozioni di base e
proprietà fondamentali. Normalizzazione forte e sue applicazioni.