Programma

Parte 1: Alcune nozioni preliminari.
Relazioni d'ordine e alberi, definizioni induttive, dimostrazioni per induzione, assioma di scelta e lemma di Kőnig.

Parte 2: Dimostrabilità e soddisfacibilità
Linguaggio formale del primo ordine: alfabeto, termini , formule, sequenti. Strutture per un linguaggio del primo ordine: strutture, termini e formule a parametri in una struttura, valutazione di termini, formule e sequenti. Calcolo dei sequenti per la logica del primo ordine: il calcolo dei sequenti LK di Gentzen. Sequenti derivabili e derivazioni. Correttezza delle regole di LK. Analisi canonica e teorema fondamentale: costruzione dellanalisi canonica (con e senza tagli) e dimostrazione del teorema fondamentale dellanalisi canonica. Conseguenze del teorema fondamentale dell'analisi canocica: teoremi di completezza, eliminabilit del taglio, compattezza, L"owenheim-Skolem.

Parte 3: Verso la teoria della dimostrazione: il teorema di eliminazione del taglio.
La procedura di eliminazione del taglio. Definizione dei passi elementari di eliminazione del taglio. Prima strategia dimostrativa (riduzione a grandi passi). Seconda strategia dimostrativa (rovesciamento delle derivazioni). Cenni sulla complessit\`a della procedura di eliminazione del taglio. Qualche conseguenza immediata del teorema di eliminazione del taglio.

Testi Adottati

V. Michele Abrusci e Lorenzo Tortora de Falco, Logica. Vol. 1 Dimostrazioni e modelli al primo ordine, Springer, 2014
https://sites.google.com/view/lm410/home

Bibliografia Di Riferimento

V. Michele Abrusci e Lorenzo Tortora de Falco, Logica. Vol. 1 Dimostrazioni e modelli al primo ordine, Springer, 2014 https://sites.google.com/view/lm410/home

Modalità Erogazione

Il corso prevede Didattica frontale; Discussioni con gli studenti e dibattiti sugli argomenti trattati; Esercitazioni; La frequenza non è obbligatoria ma è vivamente raccomandata. Nel caso di un prolungamento dell’emergenza sanitaria da COVID-19 verranno valutate le modalità di svolgimento delle attività didattiche. Si cercherà di limitare l’inevitabile danno agli studenti dovuto ad un’eventuale necessità di tenere il corso a distanza preservando, per quanto possibile, l’interattività durante le lezioni. E' presvisto lo streaming sincrono delle lezioni senza registrazione delle lezioni svolte in aula.

Modalità Frequenza

non obbligatoria ma fortemente raccomandata

Modalità Valutazione

Esame scritto e/o orale, di durata variabile, in media tra 45 e 60 minuti. Nel caso di misure restrittive dovute alla emergenza sanitaria da COVID-19 verranno valutate le modalità di svolgimento degli esami. Si cercherà di limitare l’inevitabile danno agli studenti dovuto ad un’eventuale necessità di tenere gli esami a distanza.

Programma

Parte 1: Alcune nozioni preliminari.
Relazioni d'ordine e alberi, definizioni induttive, dimostrazioni per induzione, assioma di scelta e lemma di Kőnig.

Parte 2: Dimostrabilità e soddisfacibilità
Linguaggio formale del primo ordine: alfabeto, termini , formule, sequenti. Strutture per un linguaggio del primo ordine: strutture, termini e formule a parametri in una struttura, valutazione di termini, formule e sequenti. Calcolo dei sequenti per la logica del primo ordine: il calcolo dei sequenti LK di Gentzen. Sequenti derivabili e derivazioni. Correttezza delle regole di LK. Analisi canonica e teorema fondamentale: costruzione dellanalisi canonica (con e senza tagli) e dimostrazione del teorema fondamentale dellanalisi canonica. Conseguenze del teorema fondamentale dell'analisi canocica: teoremi di completezza, eliminabilit del taglio, compattezza, L"owenheim-Skolem.

Parte 3: Verso la teoria della dimostrazione: il teorema di eliminazione del taglio.
La procedura di eliminazione del taglio. Definizione dei passi elementari di eliminazione del taglio. Prima strategia dimostrativa (riduzione a grandi passi). Seconda strategia dimostrativa (rovesciamento delle derivazioni). Cenni sulla complessit\`a della procedura di eliminazione del taglio. Qualche conseguenza immediata del teorema di eliminazione del taglio.

Testi Adottati

V. Michele Abrusci e Lorenzo Tortora de Falco, Logica. Vol. 1 Dimostrazioni e modelli al primo ordine, Springer, 2014
https://sites.google.com/view/lm410/home

Bibliografia Di Riferimento

V. Michele Abrusci e Lorenzo Tortora de Falco, Logica. Vol. 1 Dimostrazioni e modelli al primo ordine, Springer, 2014 https://sites.google.com/view/lm410/home

Modalità Erogazione

Il corso prevede Didattica frontale; Discussioni con gli studenti e dibattiti sugli argomenti trattati; Esercitazioni; La frequenza non è obbligatoria ma è vivamente raccomandata. Nel caso di un prolungamento dell’emergenza sanitaria da COVID-19 verranno valutate le modalità di svolgimento delle attività didattiche. Si cercherà di limitare l’inevitabile danno agli studenti dovuto ad un’eventuale necessità di tenere il corso a distanza preservando, per quanto possibile, l’interattività durante le lezioni. E' presvisto lo streaming sincrono delle lezioni senza registrazione delle lezioni svolte in aula.

Modalità Frequenza

non obbligatoria ma fortemente raccomandata

Modalità Valutazione

Esame scritto e/o orale, di durata variabile, in media tra 45 e 60 minuti. Nel caso di misure restrittive dovute alla emergenza sanitaria da COVID-19 verranno valutate le modalità di svolgimento degli esami. Si cercherà di limitare l’inevitabile danno agli studenti dovuto ad un’eventuale necessità di tenere gli esami a distanza.