LOGICA MATEMATICA

Anno accademico 2022/2023 - Docente: MARIANNA NICOLOSI ASMUNDO

Risultati di apprendimento attesi

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 delle caratteristiche sintattiche e semantiche della logica proposizionale e predicativa, attraverso lo studio delle nozioni di base della teoria dei modelli e della teoria della dimostrazione. 

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 le principali caratteristiche della logica proposizionale e predicativa; in particolare lo studente acquisirà familiarità con diverse teorie del primo ordine e sistemi formali di rappresentazione e dimostrazione quali sistemi assiomatici di Hilbert e tableau semantici.

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 conseguenza logica nell’ambito della logica proposizionale e di teorie matematiche del 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.

Qualora l'insegnamento venisse impartito in modalità mista o a distanza potranno essere introdotte le necessarie variazioni rispetto a quanto dichiarato in precedenza, al fine di rispettare il programma previsto e riportato nel syllabus.

Informazioni per studenti con disabilità e/o DSA

A garanzia di pari opportunità e nel rispetto delle leggi vigenti, gli studenti interessati possono chiedere un colloquio personale in modo da programmare eventuali misure compensative e/o dispensative, in base agli obiettivi didattici ed alle specifiche esigenze. E' possibile rivolgersi anche al docente referente CInAP (Centro per l’integrazione Attiva e Partecipata - Servizi per le Disabilità e/o i DSA) del nostro Dipartimento, prof. Filippo Stanco. 

Prerequisiti richiesti

Nessun prerequisito. 

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.

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.  Teorema di Compattezza per la logica proposizionale. 

Teoremi di sostituzione. Forma normale negativa. Notazione uniforme di Smullyan. Congiunzioni e disgiunzioni generalizzate. Letterali, clausole, clausole duali, Forma Normale Congiuntiva, Forma Normale Disgiuntiva.

 Decidibilità della logica proposizionale.

Logica del primo ordine: linguaggi, sostituzioni. Verità e modelli. Implicazione logica. Definibilità in una struttura.

Definibillità in una classe di strutture.

Omomorfismi e Teorema dell'omomorfismo. 

Un calcolo deduttivo assiomatico. Teoremi di correttezza e completezza del calcolo deduttivo. 

Modelli finiti. Dimensione dei modelli. Modelli di Herbrand. Teorema di Herbrand. 

Teorie del primo ordine. Esempi. Cenni di analisi non standard. Teoria dei numeri. Eliminazione dei quantificatori.

Sistema dei tableaux semantici, di risoluzione, di Hilbert e di deduzione naturale per la logica del primo ordine, loro correttezza e completezza.    


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

 ArgomentiRiferimenti testi
1Induzione e ricorsione. Sez. 1.4 di 1).
2Sintassi della logica proposizionale. Sez. 1.1. di 1), Sez. 2.2 di 2).
3Semantica della logica proposizionale. Sez. 1.2 di 1), Sez. 2.3, 2.4 di 2).
4Teoremi di sostituzione. Forme normali.Sezioni da 2.5 a 2.8 di 2).
5Compattezza e decidibilità.Sez. 1.7 di 1).
6Logica del I ordine: linguaggi, sostituzioni. Sezioni 2.0 e 2.1 di 1) e Sezioni 5.1, 5.2 e 7.2 di 2).
7Verità e modelli. Implicazione logica. Definibilità in una struttura. Definibilità in una classe di strutture. Omomorfismi e Teorema dell'omomorfismo. Sez. 2.2 di 1) e Sez. 5.3 di 2).
8Un calcolo deduttivo assiomatico. Sez. 2.3 di 1).
9Correttezza e completezza del calcolo. Sez. 2.4 di 1).
10Modelli finiti. Dimensione dei modelli. Teorie del primo ordine.Sez. 2.6 di 1).
11Teorema di Herbrand e sua versione costruttiva. Sezioni 8.6 e 8.7 di 2).
12Cenni di analisi non standard.Sez. 2.8 di 1)
13Teoria dei numeri. Eliminazione dei quantificatori. Sezioni 3.0 e 3.1 di 1). 
14Sistemi formali: tableaux semantici, risoluzione, sistemi assiomatici di Hilbert, deduzione naturale. Loro correttezza e completezza. Capitoli 3, 4 e 6 di 2). 

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) Dimostrare che una formula della logica del primo ordine è conseguenza logica di un insieme di formule della logica del primo ordine (si può chiedere di utilizzare uno specifico metodo formale di dimostrazione: tableaux, deduzione naturale, ecc...).

2) Dimostrare che un enunciato è finitamente valido. 

3) Dimostrare il Teorema di Compattezza per la logica proposizionale. 

4) Dimostrare il Teorema dell'omomorfismo.