Topic outline
Programma e materiali del corso, Introduzione al 10.o problema di Hilbert. (5 marzo h.11-13, Aula 5A edif. H2bis)
- Lucidi introduttivi al 10.o problema di Hilbert File PDF document
Le lezioni delle date 2, 3 aprile e 9, 10 aprile verranno tenute in inglese dal prof. Ernst-Erich Doberkat, vedi
http://www.cs.tu-dortmund.de/nps/de/Home/Personen/D/Doberkat__Ernst-Erich.html
che tratterà i seguenti temi:
* Modal logics and Kripke models
* Expressivity
* Model morphisms
* Categories and Coalgebras
* Bisimulations
Di che si occupa la logica formale? Cos'e`---intesa matematicamente---una logica? (6 marzo h.14-16, Aula 5A edif. H2bis)
Approfondimento sulla semantica della logica proposizionale; riduzione dei suoi enunciati a forma 3CNF. Logiche booleane. (12 marzo h.11-13, Aula 5A, edif. H2bis)
Soddisfacibilita` proposizionale, per formule in 3CNF. Consistenza, logiche booleane e teorema di Lindenbaum (19 marzo, h.11-13, aula 5A edificio H2bis)
Vedi la terza pagina (recentemente aggiunta) della dispensa della lezione scorsa sulla riduzione a forma 3CNF
Per il resto, proseguire nella lettura dei lucidi "Cos'è una logica?" del 6 marzo scorso, della dispensa associata agli stessi e del Capitolo 1 delle `Lecture Notes in Logic' di Martin Davis, 1993.
Approfondimento suggerito: Documentarsi sul lemma di Zorn e ri-dimostrare per suo tramite il teorema di Lindenbaum, senza l'ipotesi semplificatrice impiegata nei lucidi e nella dispensa del corso.
Logiche booleane minimali e teorema di Post. Un linguaggio di programmazione 'a registri' Turing-completo. (20 marzo 2019, h.14-16, aula 5A)
Proseguire nella lettura dei lucidi "Cos'è una logica?" del 6 marzo scorso, della dispensa associata agli stessi e del Capitolo 1 delle `Lecture Notes in Logic' di Davis del 1993.
Gödelizzazione e diagonalizzazione (26 marzo 2019, h.11-13 aula 5A edificio H2bis)
Gödelizzazione e diagonalizzazione
- Dall'abbinamento alla codifica di sequenze File PDF document
Qui sopra si trova un esempio di Gödelizzazione, applicato alle equazioni diofantee; però in Dropbox trovate un'estesa trattazione su 'lucidi' del tema "Dall'abbinamento alla codifica di sequenze".
Completamento di qualche punto lasciati in sospeso nelle recenti lezioni (27 marzo 2019, h.14-16 aula 5A)
Completare la lettura dei lucidi "Cos'e` una logica?" esposti tra il materiale del 6 marzo
Modulo "Introduction to modal logics and their coalgebraic interpretation" svolto dal prof. E.-E. Doberkat nelle date 02/04, 3/04 e 09/04, 10/04 2019, usuale orario e luogo
AVVISO! La lezione del 3 aprile iniziera` alle 13:15 anzichè alle 14:15
La lezione del 10 aprile subirà la stessa anticipazione di orario.
I linguaggi interpretati che soggiacciono alla logica predicativa del prim'ordine (16 aprile 2019, h.11-13 & 17 aprile 2019, h.14-16. Aula 5A edificio H2bis)
- Qualche teoria assiomatica del prim'ordine File PDF document
Come motivazione di partenza, vengono presentate tre teorie assiomatiche:
- teoria elementare dei gruppi
- aritmetica di Dedekind-Peano
- teoria degli insiemi di Vaught
- equipollenza di sistemi di assiomi differenti (perfino nel linguaggio in cui vengono enunciati), indecidibilità
- assiomatizzabilità finita, indecidibilità essenziale
- indecidibilità essenziale in un contesto ridotto "all'osso", che verrà esteso in una teoria in grado di fungere da fondamento per l'intero corpus delle discipline matematiche
- Linguaggi predicativi del prim'ordine File PDF document
Come ulteriore esempio motivante, viene presentata---nella versione assiomatica del 1967---la geometria elementare di Tarski; poi vengono proposti lessico, sintassi, semantica di un generico linguaggio predicativo del prim'ordine. Per ora non viene proposto alcun apparato deduttivo: una volta aggiunto anche quello, saremo appieno dentro il calcolo predicativo del 1.o ordine, adatto a far da supporto a un'infinità di teorie, rilevanti sia per la matematica che per la programmazione dichiarativa.
Assiomi di una teoria degli insiemi (30 aprile 2019, h.11--13, aula 5A edif. H2bis)
Calcolo predicativo del prim'ordine (7 maggio, h.11-13, aula 5A edif. H2bis; 8 maggio, h.13-16, aula 5A edif. H2bis)
In precedenza abbiamo visto (e prima di guardare questi lucidi richiameremo) la definizione di sintassi e semantica della logica predicativa: fin qui avevamo definito, in tutto, un linguaggio interpretato. Ora forniremo una versione del calcolo, cioè introdurremo una nozione di derivabilità che riguarda gli enunciati del linguaggio in questione.
Gioca un ruolo importante, nella verifica che il linguaggio predicativo diventa, una volta che lo si sia munito anche dell nozione di derivabilità, una logica booleana: il teorema di deduzione.
La piena rispondenza fra calcolo e semantica si basa su due teoremi: correttezza (in inglese 'soundness') e completezza. Il primo ci garantisce che da un insieme E di enunciati non possiamo derivare altro che 'conseguenze logiche' (questa locuzione riguarda la semantica) di E: dunque il calcolo non largheggia indebitamente. Il secondo ci assicura che tutte le conseguenze logiche di E sono derivabili da E: dunque al calcolo non manca nulla.
Entrano in gioco, nel corso della dimostrazione, interpretazioni di Herbrand, il cui dominio è interamente costituito di termini. Importante anche un meccanismo definitorio dovuto a Skolem e perciò chiamato skolemizzazione.
Completezza del calcolo predicativo del 1.o ordine (14 maggio, h.11-13, aula 5A edif. H2bis; 15 maggio, h.13-15, aula 5A edif. H2bis)
Avviso sulla calendarizzazione delle ultime lezioni e sulle date d'esame.
Le ultime lezioni sono previste nelle seguenti date / orari:
Mercoledì 15 maggio, h.13:00/15:00
Venerdì 17 maggio, h.9:00/11:00
Martedì 21 maggio, h.11:00/13:00
Mercoledì 22 maggioLezione annullataMartedì 28 maggio, h.11:00/13:00
Mercoledì 29 maggio, h.13:00/16:00
Venerdì 31 maggio, h.9:00/11:00
Gli appelli estivi d'esame sono previsti nelle seguenti date / orari:
17 Giugno, h.10:00
4 Luglio, h.10:00
25 Luglio, h.10:00
Programmazione tramite clausole di Horn (17 maggio, h.9:00/11:00, aula 4C edif. H2bis; 21 maggio, h.11:00/13:00, aula 5A edif. H2bis)
- Clausole di Horn e computabilità. (Lucidi) File PDF document
Clausole di Horn, modello minimo, domande e risposte; Programmazione tramite clausole e tramite regole di produzione grammaticale in Prolog (28 maggio, h.11:00/13:00, aula 5A edif. H2bis; 29 maggio, h.13:00/15:00, aula 5A edif. H2bis)
- Esempietto di programma Prolog File Text file
Indecidibilità della logica predicativa: teorema di Church applicato alle basi di clausole di Horn (31 maggio, h.9:00/12:00, aula 4B edif. H2bis)