LOGICA MATEMATICA
Anno accademico 2021/2022 - 1° anno - Curriculum APPLICATIVOCrediti: 6
Organizzazione didattica: 150 ore d'impegno totale, 103 di studio individuale, 35 di lezione frontale, 12 di esercitazione
Semestre: 1°
Obiettivi formativi
La logica matematica è la disciplina che si occupa della formalizzazione sistematica e della catalogazione di metodi formali validi per il ragionamento matematico.
Obiettivo del corso è lo studio dei principali strumenti formali per il ragionamento in ambito matematico. Gli studenti acquisiranno la capacità di tradurre affermazioni dal linguaggio naturale nel linguaggio formale, anche attraverso esempi e casi di studio concreti in ambito matematico. Essi inoltre svilupperanno una buona conoscenza degli aspetti sintattici e semantici della logica proposizionale e predicativa e una buona competenza nell’utilizzare i metodi formali più noti per la verifica o la refutazione di relazioni di conseguenza logica.
Obiettivi formativi generali dell'insegnamento in termini di risultati di apprendimento attesi.
Conoscenza e capacità di comprensione (knowledge and understanding): l'obiettivo del corso è quello di far acquisire conoscenze che consentano allo studente di comprendere gli aspetti sintattici e semantici della logica proposizionale e predicativa; in particolare lo studente acquisirà familiarità con i principali sistemi formali per il ragionamento quali tableau semantici, risoluzione, deduzione naturale e metodo di Davis-Putnam.
Capacità di applicare conoscenza e comprensione (applying knowledge and understanding): lo studente acquisirà le competenze necessarie per tradurre affermazioni dal linguaggio naturale nel linguaggio formale, per utilizzare i principali sistemi di dimostrazione formale al fine di verificare relazioni di consieguenza logica nell’ambito della logica proposizionale e di prim’ordine.
Autonomia di giudizio (making judgements): Attraverso lo studio e l’analisi di esempi concreti di formalizzazione e di deduzione logica, lo studente acquisirà la capacità di comprendere la correttezza delle soluzioni proposte e di utilizzare autonomamente soluzioni in grado di garantire una corretta rappresentazione formale e dimostrazione di casi di studio più complessi.
Abilità comunicative (communication skills): lo studente acquisirà le necessarie abilità comunicative e di appropriatezza espressiva nell'impiego del linguaggio formale della logica in vari ambiti matematici, sia teorici che applicativi.
Capacità di apprendimento (learning skills): il corso si propone, come obiettivo, di fornire allo studente gli strumenti pratici e le nozioni teoriche per poter affrontare e risolvere autonomamente nuove problematiche di formalizzazione e inferenza in svariati ambiti matematici.
Modalità di svolgimento dell'insegnamento
Lezioni frontali in cui, oltre alla spiegazione di nozioni e concetti base relativi alla formalizzazione e dimostrazione formale negli ambiti della logica proposizionale e del primo ordine, verranno presentati diversi esempi e casi di studio al fine di stimolare la discussione in classe e facilitare la comprensione degli argomenti.
Prerequisiti richiesti
Nessuno.
Frequenza lezioni
Al fine di poter comprendere pienamente gli argomenti del corso, la frequenza delle lezioni è fortemente consigliata.
Contenuti del corso
Il corso introduce la sintassi, la semantica e le principali caratteristiche della logica proposizionale e del primo ordine. Verranno considerate questioni riguardanti decidibilità, definibilità e strutture del primo ordine, verranno introdotti i principali metodi formali di dimostrazione, come i tableaux semantici, la risoluzione, la deduzione naturale e i sistemi assiomatici di Hilbert.
PROGRAMMA DETTAGLIATO
Introduzione al corso. Definizione di insiemi per induzione. Principio di induzione strutturale. Definizione di funzioni per ricorsione.
Logica proposizionale
Sintassi della logica proposizionale. Costruzione del linguaggio della logica proposizionale. Principio di induzione strutturale e di ricorsione strutturale. Nozione di sottoformula.
Semantica della logica proposizionale. Connettivi, valutazioni booleane. Tautologie, formule soddisfacibili e soddisfacibilità di insiemi di formule. Teorema di deduzione semantica. Nozione di dualità per i connettivi binari.
Teoremi di sostituzione. Forma normale negativa. Notazione uniforme di Smullyan. Congiunzioni e disgiunzioni generalizzate. Letterali, clausole, clausole duali, Forma Normale Congiuntiva, Forma Normale Disgiuntiva.
Teorema di Compattezza per la logica proposizionale. Decidibilità della logica proposizionale.
Il metodo dei tableaux semantici: regole di espansione e costruzione. Correttezza del sistema dei tableaux. Il metodo di risoluzione: regole di espansione e regola di risoluzione. Correttezza del sistema di risoluzione. Insiemi di Hintikka e lemma di Hintikka. Teorema di esistenza di un modello. Dimostrazione di completezza per il sistema dei tableaux e della risoluzione proposizionale. Albero semantico. Insiemi di clausole saturi. Insiemi di Robinson. Completezza del sistema di risoluzione.
Sistemi di Hilbert. Teorema di Deduzione di Tarski-Herbrand. Correttezza e completezza di un sistema di Hilbert.
Sistema di deduzione naturale. Correttezza e completezza forte del sistema.
Procedura di Davis Putnam. Correttezza della procedura.
Logica del primo ordine
Logica del primo ordine: linguaggi, sostituzioni, unificazione. Verità e modelli. Implicazione logica. Definibilità in una struttura.
Modelli di Herbrand. Notazione uniforme per il primo ordine. Principio di induzione e di ricorsione strutturale per la logica del primo ordine. Insiemi di Hintikka al primo ordine, Lemma di Hintikka, Teorema di esistenza di un modello al primo ordine, Teorema di compattezza per la logica del primo ordine. Teorema di Lowenheim-Skolem.
Sistema dei tableaux semantici, di risoluzione, di Hilbert e di deduzione naturale per la logica del primo ordine, loro correttezza e completezza.
Skolemizzazione. Teorema di Skolemizzazione. Forma skolemizzata e prenessa.
Teorema di Herbrande sua forma costruttiva.
Modelli finiti. Dimensione dei modelli. Teorie del primo ordine.
Testi di riferimento
Libri di testo consigliati:
1) Herbert B. Enderton. A Mathematical Introduction to Logic, 2nd edition. Academic Press, 2010. pp. VII-317.
2) Melvin Fitting. First-order logic and automated theorem proving, 2nd edition. Springer-Verlag New York, 1996, pp. XVII-326.
Programmazione del corso
| Argomenti | Riferimenti testi | |
|---|---|---|
| 1 | Induzione e ricorsione. | Sez. 1.4 di 1) |
| 2 | Sintassi della logica proposizionale. | Sez. 1.1. di 1), Sez. 2.2 di 2) |
| 3 | Semantica della logica proposizionale. | Sez. 1.2 di 1), Sez. 2.3, 2.4 di 2) |
| 4 | Teoremi di sostituzione. Forma normale negativa. Notazione uniforme di Smullyan e nuove formulazioni di principio di induzione strutturale e di ricorsione strutturale. Congiunzioni e disgiunzioni generalizzate. Letterali, clausole, clausole duali, Forma Normale Congiuntiva, Forma Normale Disgiuntiva. | Sezioni da 2.5 a 2.8 di 2) |
| 5 | Compattezza e decidibilità. | Sez. 1.7 di 1) |
| 6 | Il metodo dei tableaux semantici. Il metodo di risoluzione. Correttezza dei due sistemi. Insiemi di Hintikka e lemma di Hintikka. Teorema di esistenza di un modello. Dimostrazione di completezza per il sistema dei tableaux e della risoluzione proposizionale. Albero semantico.Insiemi di Robinson. Completezza del sistema di risoluzione. | Cap. 3 di 2) |
| 7 | Sistemi di Hilbert. Teorema di Deduzione di Tarski-Herbrand. Sistema di deduzione naturale. Procedura di Davis Putnam. Correttezza e completezza dei tre sistemi. | Cap. 4 di 2) |
| 8 | Logica del I ordine: linguaggi, sostituzioni, unificazione. | Sezioni 2.0 e 2.1 di 1) e Sezioni 5.1, 5.2 e 7.2 di 2) |
| 9 | Verità e modelli. Implicazione logica. Definibilità in una struttura. | Sez. 2.2 di 1) e Sez. 5.3 di 2) |
| 10 | Modelli di Herbrand. Notazione uniforme per il I ordine. Principio di induzione e di ricorsione strutturale. Insiemi di Hintikka al I ordine, Lemma di Hintikka, Teorema di esistenza di un modello al primo ordine, Teorema di compattezza per la logica del primo ordine. Teorema di Lowenheim-Skolem. | Sezioni da 5.4 a 5.9 di 2) |
| 11 | Sistema dei tableaux, di risoluzione, di Hilbert e di deduzione naturale per la logica del I ordine, loro correttezza e completezza. | Cap. 6 di 2) vedere anche Sezioni 2.4 e 2.5 di 1) |
| 12 | Skolemizzazione. Teorema di Skolemizzazione. Forma skolemizzata e prenessa. | Sezioni 8.1-8.4 di 2) |
| 13 | Teorema di Herbrand e sua versione costruttiva. | Sezioni 8.6 e 8.7 di 2) |
| 14 | Modelli finiti. Dimensione dei modelli. Teorie del primo ordine. | Sez. 2.6 di 1) |
Verifica dell'apprendimento
Modalità di verifica dell'apprendimento
L'esame consta di una prova scritta, in cui lo studente è invitato a risolvere alcuni esercizi, e una prova orale sugli argomenti spiegati a lezione.
La verifica dell’apprendimento potrà essere effettuata anche per via telematica, qualora le condizioni lo dovessero richiedere.
Esempi di domande e/o esercizi frequenti
1) Verificare se una formula della logica proposizionale è una tautologia. In caso contrario esibire un controesempio.
2) Dimostrare che una formula della logica del primo ordine è conseguenza logica di un insieme di formule della logica del primo ordine.
Nel caso degli esercizi 1 e 2 si può chiedere di utilizzare uno specifico metodo formale di dimostrazione (tableaux, risoluzione, deduzione naturale, ecc...)
3) Dimostrare il Teorema di Compattezza per la logica proposizionale.
4) Dimostrare il Teorema di Deduzione di Tarski-Herbrand.