Edizione 2024-2025

Lezioni ogni Lunedì, Mercoledì e Venerdì, ore 16-19 aula L con inzio il 23 Settembre 2024.

Note:

LE LEZIONI DEL II SEMESTRE SI SVOLGONO TRA IL 23 SETTEMBRE 2024 E IL 11 GENNAIO 2025 

LE LEZIONI SI SOSPENDONO NELLE SETTIMANE 11-16 NOVEMBRE  2024 e 13-18 GENNAIO 2025  PER LO SVOLGIMENTO DEGLI ESONERI

GLI ESAMI DEL I SEMESTRE  SI SVOLGONO TRA IL 20 GENNAIO E IL 12 FEBBRAIO 2025

1. lunedì 23/9 (LTdF+RM): presentazione e avvio del corso; Discussione generale su dimostrazioni e refutazioni logiche. Esempi di dimostrazioni, ed in particolare di dimostrazioni matematiche.  

Modulo A (R. Maieli)

2. Mercoledì 25/9 : I concetti di Proposizione del Primo Ordine, Formula Logica del Primo Ordine (chiusa) e Proposizioni Puramente Logiche. I concetti di dimostrazione (logica) e refutazione (logica), falsificabilità e soddisfacibilità di una formula del primo ordine chiusa. Gli enunciati dei Teoremi di Corretta e Completezza per la Logica del Primo Ordine. Riferimenti: Capitolo 1 (Introduzione) del libro Logica. Vol. 1 Dimostrazioni e modelli al primo ordine, Springer, 2014.  Nozioni preliminari: ordini parziali ed ordini totali, relazioni ben fondate, buoni ordini. Esempi. Definizione di albero e prime proprietà degli alberi. Una semplice costruzione sugli alberi (prolungamento di alberi finiti) . Riferimenti: Capitolo 2, pagg. 36 - 41 del libro Logica. Vol. 1.

3. Venerdì 27/9: Definizioni induttive di un insieme. Dimostrazioni per induzione. Induzione sull’ordine lessicografico. Dimostrazione che l'ordine lessicogafico è un buon ordine. Assioma di scelta e sua applicazione per dimostrare il lemma di König. Dimostrazione del Lemma di König numerabile senza Assioma di Scelta. Una semlice costruzione su alberi finiti: estnzioni unarie e prolungamento di un albero finito  Capitolo 2, pagg. 41 - 48 del libro Logica. Vol. 1. Esercizio: dimostrare che le due formulazioni del principio di induzione di pagina 45 (sezione 2.3.2) del libro di Logica vol. 1 sono equivalenti (vedi traccia dello svolgimento dell'esercizio e le altre formulazioni del principi di induzione 

4. Lunedì 30/09: Linguaggio del primo ordine: alfabeto. Due formulazioni diverse di un alfabeto del primo ordine. Definizione induttiva di termine su di un linguaggio del primo ordine. Definizione induttiva di formula su di un linguaggio del primo ordine. Occorrenze libere e vincolate di variabili in una formula. 

5. Mercoledì 2/10: Sostituzione di un termine in una formula: il "problema della cattura di una variabile". Una relazione di equivalenza sulle formule del primo ordine. Riferimenti: Capitolo 3, pagg. 49 - 61 del libro Logica. Vol. 1. Sottoformule. Grado e altezza di una formula. Osservazioni sulla cardinalità del linguaggio. Strutture per un linguaggio del primo ordine. Termini e formule a parametri (chiusi) in una struttura. Valutazione di termini e formule in una struttura. Modelli e Contromodelli per formule chiuse del primo ordine. 

6. Venerdì 4/10: Esercitazione sul principio di induzione: l’induzione sui multinsiemi finiti di numeri naturali ed il taglio delle teste dell’Idra  (scarica i file EserciziLogicaCap2.pdf).

7. Lunedì 7/10: Teorie del primo ordine e sequenti del primo ordine. Riferimenti: Capitolo 3, pagg. 62 - 69 del libro Logica. Vol. 1. Esercitazione sulla nozione di soddisfacibilità, da parte di una struttura, di una formula chiusa del primo ordine Prima discussione sull’assiomatizzazione al primo ordine della nozione di insieme finito e della nozione di insieme infinito. Esercizi sulla soddisfacibilità al primo ordine. Scarica il testo degli EserciziLogicaCap3-1.pdf.

8. Mercoledì 9/10: Presentazione del calcolo dei sequenti LK di Gentzen per la logica del primo ordine: lista delle regole, commenti e discussione. Formulazioni moltiplicativa e additiva delle regole del calcolo dei sequenti Definizione di derivabilità di una formula (e di un sequente) e di derivabilità di una formula (e di un sequente) da un insieme di formule. Esempi. Riferimenti: Capitolo 3, pagg. 70 - 73 del libro Logica. Vol. 1. Esempi. Esercitazione: La nozione di reversibilità di una regola logica.  Elenco delle regole reversibili del calcolo dei sequenti. Dimostrazione della reversibilità delle regole. Esercitazione sulla derivabilità delle regole moltiplicative da quelle additive e vice-versa mediante l’uso delle regole strutturali (weakening e contraction).

9. Venerdì 11/10:Teorema di correttezza per la logica del primo ordine (Vedi Errata-Corrige Volume 1). Esercizi: mostrare che la regola del Vero moltiplicativo (1) è derivabile dal LK senza (1) e che la regola del Vero additivo (T) è derivabile da LK senza (T).

10. Lunedì 14/10: Esercitazione sull’induzione e la derivabilità. Elementi neutri ed elementi assorbenti della congiunzione e della disgiunzione. Distributivi della congiunzione sulla disgiunzione. Il Teorema dell’Ubriaco e la necessità della regola di Contrazione per la nozione di derivabilità nel calcolo dei predicati del primo ordine. Esercizi sulla nozione di derivabilità in LK senza Quantificatori (calcolo proposizionale) ed in presenza di Quantificatori. (Esercizi 3.8.1, 3.9.1 e 3.10 del file EserciziLogicaCap3-2.pdf). Esercizi Definizione di Analisi di un sequente da un insieme di formule come generalizzazione della nozione di derivazione di un sequente da un insieme di formule. Esempi. Riferimenti:

11. Mercoledì 16/10: Ordine Ciclico. Costruzione dell’Analisi Canonica Senza Tagli di una formula del primo ordine. Proprietà dell'A.C.S.T di una formula chiusa del primo ordine. Esempi e discussione. Riferimenti: Capitolo 3, pagg. 80 -  88 del libro Logica. Vol. 1.

12. Venerdì 18/10: Costruzione dell’Analisi Canonica Con Tagli di una formula chiusa A da una Teoria T del primo ordine. Proprietà dell'A.C.C.T. Esempi e discussione. Prime Proprietà dei rami scorretti dell'Analisi Canonica con e senza tagli: Lemmi 0,1 e 2. Riferimenti: Capitolo 3, pagg. 88 - 97 del libro Logica. Vol. 1.

13. Lunedì 21/10:  Esercitazione: sulla nozione di derivabilità in LK in presenza di quantificatori + analisi canonica con e senza tagli (Riferimenti:   file EserciziLogicaCap3-2.pdf). 

14. Mercoledì 23/10: Proprietà dei rami scorretti dell'Analisi Canonica con e senza tagli: Lemmi 3,4 e 5 e 6. Teorema fondamentale dell’Analisi Canonica con la dimostrazione completa. Commenti ed esempi. Riferimenti: Capitolo 3, pagg. 97 - 108 del libro Logica. Vol. 1.

15. Venerdì 25/10: Conseguenze del teorema fondamentale dell'Analisi Canonica: teorema di completezza, teorema di eliminabilità del taglio. Corollario della non-contraddittorietà di LK. Ulteriori conseguenze del teorema fondamentale dell’analisi canonica: teorema di compattezza, teorema di Löwenheim-Skolem. Osservazioni conclusive sul teorema fondamentale dell’analisi canonica e sulle estensioni delle sue conseguenze al caso dei linguaggi più che numerabili (verso la Teoria dei Modelli).   Esercitazione: su soddisfacibilità, dimostrabilità, analisi canonica.

16. Lunedì 28/10: La questione dell’eliminazione del taglio di Gentzen. Enunciato del teorema di eliminazione del taglio e suo raffinamento. Strategia generale della dimostrazione. Le trasformazioni elementari definite da Gentzen (i casi-chiave). I casi dell’indebolimento e della contrazione. Le trasformazioni elementari definite da Gentzen: il caso dei quantificatori e le difficoltà ad esso connesse. Riferimenti: Capitolo 4, pagg. 109 - 125 del libro Logica. Vol. 1.

17. Mercoledì 30/10: Prima dimostrazione del teorema di eliminazione del taglio applicando la procedura T_glob ottenuta componendo opportunamente tra loro i passi elementari di riduzione T e distinguendo i passi logici (L) da i passi strutturali (S). Discussione ed esempi. Riferimenti: Capitolo 4, pagg. 125 - 133 del libro Logica. Vol. 1. 

18. Lunedì 4/11: Lemma di reversibilità. Seconda dimostrazione del teorema di eliminazione del taglio applicando la procedura T_rev, ottenuta sfruttando il lemma di reversibilità. Discussione ed esempi. Riferimenti: Capitolo 4, pagg. 125 - 133 del libro Logica. Vol. 1.

19. Esercizi sulla dimostrabilità di formule con quantificatori chiuse del primo ordine. Esercizi sulla eliminazione dei tagli da dimostrazioni con quantificatori.

Primo Esonero sul Modulo A: Martedì 12 Novembre 2024 ore 10 - 13 aula L

Lezioni Modulo B (Lorenzo Tortora de Falco)

Lezione extra sul Modulo A (Roberto Maieli), Mercoledì 18 Dicembre 2024, ore 16-19 aula L: Weak-Normalization vs Strong Normalization