Teoria della Dimostrazione
Corso di Laurea Specialistica in Informatica
Anno Accademico 2006/07
Obiettivi e contenuti
Il corso ha lo scopo di fornire le nozioni di base della teoria della dimostrazione e le principali
connessioni tra questa e l'informatica. In particolare, le basi logiche per lo studio dei linguaggi
di programmazione e della teoria dei tipi.
Dopo un richiamo delle principali nozioni di logica di base, si studieranno le relazioni tra i sistemi
alla Hilbert del primo ordine, la deduzione naturale e il calcolo dei sequenti e le principali proprietà
di questi sistemi.
Si passerà poi allo studio della logica intuizionistica e della sua interpretazione
Brouwer-Heyting-Kolmogorov.
Prima di passare allo studio dei sistemi del secondo ordine (sistema F),
si dimostreranno i teoremi di incompletezza di Gödel (preceduti da un
un richiamo delle nozioni base di calcolabità).
Si mostrerà quindi il teorema di normalizzazione forte per il sistema F e la
rappresentabilità di funzioni e tipi di dato in F. Infine, si vedrà
la rappresentabilità dell'aritmetica al secondo ordine (aritmetica di Heyting)
per mezzo della corrispondenza con il sistema F.
Il corso si concluderà con una parte seminariale composta da brevi presentazioni
(una o due ore) tenute dagli studenti su argomenti proposti dal docente.
Programma di massima
- Calcolo dei predicati
- Richiami su linguaggi e teorie del prim'ordine, validità logica e modelli
- Sistemi deduttivi:
- Sistemi assiomatici alla Hilbert
- Deduzione naturale
- Calcolo dei sequenti
- Corrispondenze tra i sistemi deduttivi
- Corretteza e completezza.
- Riduzioni ed eliminazione del taglio
- Riduzione di dimostrazioni in deduzione naturale
- Teorema di eliminazione del taglio
- Richiami di teoria della calcolabilità
- Aritmetica di Peano e teoremi di incompletezza di Gödel
- Logica Intuizionistica
- Differenze e relazioni con la logica classica
- Interpretazione Brouwer-Heyting-Kolmogorov e isomorfismo Curry-Howard
- Modelli della logica intuizionistica
- Sistemi di ordine superiore
- Polimorfismo e sistema F
- Teorema di forte normalizzazione
- Funzioni e tipi di dato rappresentabili nel sistema F
- Aritmetica di Heyting
- Parte seminariale su temi di approfondimento proposti dal docente e scelti dagli studenti
Esercizi
- Logica Combinatoria: Trovare la corrispondenza tra Logica Combinatoria e un sistema assiomatico alla Hilbert per l'implicazione.
- Logica Intuizionista: Dimostrare se alcune fomule sono derivabili o meno in NJ, per via sintattica (ragionando sulle regole di NJ) e per via semantica (usando la semantica di Kripke).
--
StefanoGuerrini - 22 Sep 2006