Salta al contenuto principale della pagina

TEORIA DELLA DIMOSTRAZIONE

CODICE 107014
ANNO ACCADEMICO 2021/2022
CFU
  • 5 cfu al 2° anno di 9011 MATEMATICA(LM-40) - GENOVA
  • SETTORE SCIENTIFICO DISCIPLINARE MAT/01
    SEDE
  • GENOVA
  • PERIODO 2° Semestre
    MATERIALE DIDATTICO AULAWEB

    PRESENTAZIONE

    La teoria della dimostrazione e' la branca della logica matematica rivolta allo studio delle dimostrazioni intese a loro volta come oggetti matematici,  solitamente rappresentate come strutture ad albero induttivamente generate. 

    La teoria della dimostrazione,  oltre ad essere uno dei pilastri dei fondamenti della matematica, assieme alla teoria dei modelli, alla teoria assiomatica degli insiemi, alla teoria della calcolabilità, e alla teoria delle categorie, gioca un ruolo primario nella teoria dei linguaggi di programmazione.

    OBIETTIVI E CONTENUTI

    OBIETTIVI FORMATIVI

    In questo insegnamento verranno studiati i sistemi deduttivi per la logica classica ed intuizionista e le loro estensioni per teorie matematiche. 

    In particolare si studierà il rapporto tra sistemi assiomatici, di deduzione naturale e di calcolo dei sequenti, con particolare enfasi al loro utilizzo per la ricerca 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.

    PREREQUISITI

    Un corso introduttivo di logica

    MODALITA' DIDATTICHE

    Lezioni sincrone

    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

    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)

    RICCARDO CAMERLO

    GIUSEPPE ROSOLINI (Presidente Supplente)

    LEZIONI

    Orari delle lezioni

    L'orario di tutti gli insegnamenti è consultabile su 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.