Acquisire buona conoscenza dei principi della logica classica del primo ordine e del calcolo dei sequenti per essa, nonch‚ dei principali risultati che la concernono.
scheda docente
materiale didattico
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.
https://sites.google.com/view/lm410/home
Fruizione: 20410451-1 LM410 -TEOREMI SULLA LOGICA 1 - MODULO A in Matematica LM-40 MAIELI ROBERTO
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, 2014https://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à 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.