PRESENTAZIONE

La teoria della dimostrazione è uno dei quattro pilastri della logica matematica ed è di fondamentale interesse per matematici, informatici, filosofi e linguisti. La teoria della dimostrazione ha radici storiche nei sillogismi di Aristotele e nel sogno di Leibniz di un calculus ratiocinator per la formalizzazione e l'automazione del ragionamento. Nel ventesimo secolo la teoria della dimostrazione è stata fortemente richiesta dal programma di Hilbert e con i contributi rivoluzionari di Gentzen e l'invenzione della deduzione naturale e del calcolo dei sequenti si è  sviluppata come campo di studio indipendente. La teoria della dimostrazione si occupa dello sviluppo di sistemi formali di deduzione, concepiti come oggetti formali definiti sintatticamente, dello studio delle loro proprietà e della loro applicabilità a problemi concreti al di là della disciplina.

OBIETTIVI E CONTENUTI

OBIETTIVI FORMATIVI

L'insegnamento introduce allo studio delle dimostrazioni come oggetti formali della matematica analizzandone la struttura e applicandolo a particolari sistemi logici, con attenzione all'automazione delle dimostrazioni.

OBIETTIVI FORMATIVI (DETTAGLIO) E RISULTATI DI APPRENDIMENTO

Lo scopo dell'insegnamento e' da una parte quello di presentare i risultati centrali della teoria della dimostrazione, dall'altra fornire gli strumenti perchè gli studenti possano definire ed utilizzare in modo autonomo calcoli deduttivi con buone proprietà ai fini dello studio meta-teorico dei sistemi logici, delle loro applicazioni, e dell'automazione delle dimostrazioni.

MODALITA' DIDATTICHE

Lezioni frontali

PROGRAMMA/CONTENUTO

0. Introduzione alla teoria della dimostrazione.

1.  Dalla deduzione naturale al calcolo dei sequenti

2. Un calcolo invertibile per la logica proposizionale classica

3. Il ragionamento costruttivo 

4. Calcolo dei sequenti intuizionistico 

5. Ammissibilità di contrazione e taglio

6. Conseguenze dell'eliminazione del taglio

7. Completezza

8. Quantificatori in deduzione naturale ed in calcolo dei sequenti

9. Completezza della logica predicativa classica

10. Varianti del calcolo dei sequenti

11. Analisi strutturale delle teorie assiomatiche, con esempi dall'algebra, dalla geometria, e dalla teoria dei reticoli.

12. Il contenuto costruttivo delle dimostrazioni classiche

13. Il calcolo etichettato per le logiche modali e non classiche.

TESTI/BIBLIOGRAFIA

Oltre ad articoli e note che saranno resi disponibili su AulaWeb, verranno utilizzati i seguenti libri ti testo:

S. Negri and J. von Plato, Structural Proof Theory, Cambridge University Press 2001.

S. Negri and J. von Plato, Proof Analysis, Cambridge University Press 2011.

A.S. Troelstra and H. Schwichtenberg, Basic Proof Theory, second edition. Cambridge University Press 2000. 

DOCENTI E COMMISSIONI

Commissione d'esame

SARA NEGRI (Presidente)

JACOPO EMMENEGGER

RICCARDO CAMERLO (Presidente Supplente)

LEZIONI

INIZIO LEZIONI

Dal 17 febbraio 2025 secondo l'orario riportato qui 

Orari delle lezioni

L'orario di questo insegnamento è consultabile all'indirizzo: Portale EasyAcademy

ESAMI

MODALITA' D'ESAME

Valutazione basata su esercizi svolti durante il corso ed una presentazione finale su una tematica da concordare con la docente.

MODALITA' DI ACCERTAMENTO

Valutazione basata su esercizi svolti durante il corso ed una presentazione finale su una tematica da concordare con la docente.

Si valutera' l'acquisizione della capacita' di utilizzare strumenti e metodi dimostrativi, di mettere in relazione la teoria e le sue applicazioni, e di esporre agli altri partecipanti  pubblicazioni recenti di teoria della dimostrazione sintetizzandole e connettendole agli argomenti svolti nel corso.

Calendario appelli