1. Dispense del docente (scaricabili online dalla pagina Moodle del corso).
2. A.S. Troelstra, H. Schwichtenberg, Basic proof theory, Cambridge University Press 1996.
3. S. Negri, J. von Plato, Structural proof theory, Cambridge University Press 2001.
4. J.R. Hindley, J. Seldin, Lambda-Calculus and Combinators, an Introduction, Cambridge University Press 2008.
Obiettivi Formativi
(i) Conoscenza e capacità di comprensione.
Conoscenza delle principali tematiche e metodologie della teoria della strutturale della dimostrazione, della logica combinatoria e del lambda-calcolo tipato e non tipato. Capacità di comprendere e collegare problemi in questi ambiti di ricerca.
(ii) Capacità di applicare conoscenza e comprensione. Applicazione delle conoscenze e capacità di comprensione acquisite nel corso alla trattazione di problemi specifici nell'ambito della logica e della filosofia della logica, attraverso esercizi proposti.
(iii) Autonomia di giudizio. Approfondimento critico delle conoscenze acquisite nel corso mediante la lettura e lo studio autonomo di contributi scientifici (articoli, monografie).
(iv) Abilità comunicative. Esporre problemi/soluzioni di problemi/teorie/argomenti/dimostrazioni in modo comunicativamente e scientificamente appropriato, con padronanza della terminologia tecnica.
Prerequisiti
Il corso propedeutico da 12 CFU di Logica (CdS triennale in Filosofia), o conoscenze equivalenti (in questo caso parlare con il docente prima dell'iscrizione al corso).
Metodi Didattici
Lezioni frontali integrate da esercitazioni guidate dal docente.
Altre Informazioni
I materiali per il corso (dispense, sintesi delle lezioni, esercizi, ecc.) saranno resi disponibili sulla piattaforma Moodle.
Si ricorda che è richiesta una frequenza obbligatoria per almeno i 2/3 delle lezioni.
Non sono previste modalità di esame da non frequentante se non per gli studenti con iscrizione part-time (che devono prendere contatto con il docente all'inizio del corso per concordare un programma specifico).
Modalità di verifica apprendimento
L’esame consiste in una prova orale (durata: 45 minuti circa), articolata in due domande sulla prima parte del programma (teoria della dimostrazione) e due domande sulla seconda parte del programma (teorie delle operazioni).
La prova mira a verificare:
(i) la conoscenza e la comprensione delle nozioni teoriche fondamentali delle due parti del programma;
(ii) l’acquisizione della capacità di applicare quanto appreso a esercizi/problemi che saranno proposti durante il colloquio, in analogia con quelli svolti nel corso delle esercitazioni.
Alla graduazione analitica della prestazione dello studente concorrerà anche la valutazione della capacità espositiva e in particolare della precisione nell’uso del linguaggio “tecnico” della disciplina.
Programma del corso
(i) Ricapitolazione delle principali nozioni richieste come prerequisiti (sintassi e semantica della logica proposizionale e predicativa classica);
(ii) calcoli delle sequenze (L-calcoli di Gentzen e calcoli di tipo G3) per la logica classica e intuizionistica elementare;
(iii) teorema di eliminazione delle cesure e principali applicazioni (fra cui: lemma di Maehara e teorema di interpolazione; teorema di Herbrand);
(iv) cenni alle logiche sottostrutturali (in particolare logica lineare affine e logica lineare);
(v) logica combinatoria e lambda-calcolo non tipato; teorema di Church-Rosser e sue applicazioni; teorema del punto fisso e sue applicazioni.
(vi) lambda calcolo tipato; normalizzazione; corrispondenza di Curry-Howard.