Logic and Formal Language Theory

Modulo Advanced Topics in Mathematical Logic for Computer Science

Il corso riguarda alcuni argomenti avanzati e rilevanti per la logica matematica, disciplina che si occupa della formalizzazione sistematica e della catalogazione di metodi formali validi per il ragionamento in ambito matematico e informatico.

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 teoria dei numeri del primo ordine e della logica del secondo ordine; in particolare lo studente acquisirà conoscenze riguardanti risultati di rilievo quali, ad esempio, i teoremi di incompletezza di Goedel e i confini della definibilità diofantea.

Capacità di applicare conoscenza e comprensione (applying knowledge and understanding): lo studente acquisirà le competenze necessarie per applicare procedure come l’eliminazione dei quantificatori per dimostrare la decidibilità di teorie logiche, come la Skolemizzazione e l’espansione di Hebrand per lo sviluppo di dimostrazioni formali e automatizzate e per comprendere in modo concreto caratteristiche della logica del primo ordine quali la semidecidibilità. Inoltre, lo studente sarà in grado di identificare la strategia logico-strutturale alla base di sistemi complessi di equazioni polinomiali.

Autonomia di giudizio (making judgements): Attraverso lo studio e l’analisi di esempi concreti di formalizzazione e di deduzione logica, lo studente consoliderà la propria capacità di valutare la correttezza di soluzioni logico-matematiche avanzate. Saprà inoltre interpretare con occhio critico il fondamentale trade-off tra il potere espressivo di una logica (es. la categoricità del secondo ordine) e la perdita delle sue proprietà metateoriche fondamentali (completezza, compattezza).

Abilità comunicative (communication skills): lo studente consoliderà e migliorerà le proprie abilità comunicative nell'impiego del linguaggio formale della logica anche rispetto a tematiche avanzate. Sarà in grado di descrivere rigorosamente concetti sintattici complessi sia a livello di aritmetizzazione della sintassi (numeri di Gödel), sia nell'esposizione critica di risultati profondi di indecidibilità o nell'analisi di semantiche non standard (strutture generali di Henkin).

Capacità di apprendimento (learning skills): Il corso fornisce strumenti pratici e nozioni teoriche per poter affrontare e risolvere autonomamente problematiche di formalizzazione e inferenza avanzate, anche complesse, in contesti di ricerca teorica o applicata sia in matematica che in informatica.

Lezioni frontali in cui, oltre alla spiegazione di nozioni e concetti base relativi alle tematiche trattate, 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.

IL MATERIALE DEL CORSO ED EVENTUALI COMUNICAZIONI SARANNO PUBBLICATI SUL CANALE TEAMS DAL CODICE: yjvdb8j

NOTA BENE: 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 o al Presidente del Corso di Studi.  

Il corso è strutturato in tre blocchi:

·       Primo blocco: Introduzione della teoria dei numeri naturali del primo ordine e discussione della sua rilevanza, anche in vista dei teoremi di incompletezza di Gödel. Viene presentata la teoria dei numeri naturali con successore, dimostrandone la completezza e la decidibilità tramite l'eliminazione dei quantificatori; tale procedura concreta verrà applicata per provare la decidibilità di diverse teorie logiche, quali la teoria dei naturali con solo successore, la teoria con successore e relazione di minore, e l'aritmetica di Presburger. Si analizzerà inoltre una sottoteoria della teoria dei numeri finitamente assiomatizzabile, mostrandone l'incompletezza e l'indecidibilità come conseguenza del Teorema di Gödel, per poi definire e dimostrare il secondo Teorema di incompletezza di Gödel.

·       Secondo blocco: Tema della rappresentabilità diofantea in relazione al Decimo Problema di Hilbert. Viene offerta un'analisi sia culturale sia strutturale del problema stesso e del fondamentale Teorema DPRM (Davis-Putnam-Robinson-Matiyasevich). Durante le lezioni verranno esaminate le equazioni di Pell e i relativi lemmi step-down, utilizzati come strumenti aritmetici avanzati per controllare la crescita esponenziale. Saranno inoltre presentate le tecniche di combinazione e compattazione delle relazioni diofantee mediante l'impiego di polinomi e del trucco di Putnam. Il modulo si conclude con un'analisi critica della specifica dell'esponenziazione a 13 incognite.

·       Terzo blocco: Logica del secondo ordine, studio della sua espressività in ambito matematico e informatico. Ci si concentrerà sull'analisi della categoricità dei modelli e sul fallimento sistematico di proprietà metateoriche chiave come i teoremi di Compattezza e Löwenheim-Skolem. Vengono quindi introdotte le funzioni di Skolem, la Skolemizzazione applicata al secondo ordine e lo studio della logica many-sorted. Per superare i limiti espressivi della semantica standard, si introducono le strutture generali e la semantica di Henkin al fine di ripristinare il teorema di completezza. Infine, la trattazione si estende ai metodi di dimostrazione automatica mediante lo studio delle tecniche di espansione, del Teorema di Herbrand e delle ottimizzazioni della delta-regola per i tableaux semantici.

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. 

L'esame consta di 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.

Criteri per l'attribuzione del voto. Si terrà conto: della chiarezza espositiva, della completezza delle conoscenze, della capacità di collegare diversi argomenti. Lo studente deve dimostrare di aver acquisito una conoscenza suffciente dei principali argomenti trattati durante il corso.

Per l'attribuzione del voto si seguiranno di norma i seguenti criteri: 

non approvato: lo studente non ha acquisito i concetti di base e non è in grado di svolgere gli esercizi. 

18-23: lo studente dimostra una padronanza minima dei concetti di base, le sue capacità di esposizione e di collegamento dei contenuti sono modeste. 

24-27: lo studente dimostra una buona padronanza dei contenuti del corso, le sue capacità di esposizione e di collegamento dei contenuti sono buone. 

28-30 e lode: lo studente ha acquisito tutti i contenuti del corso ed è in grado di esporli compiutamente e di collegarli con spirito critico. 

1) Definire la teoria dei numeri naturali con successore e dimostrare la sua decidibilità.

2) Dimostrare il secondo Teorema di incompletezza di Goedel. 

3) Definire il problema della rappresentabilità diofantea. 

4) Enunciare e discutere il Teorema DPRM. 

5) Definire la nozione di Skolemizzazione al secondo ordine e dimostrare i relativi teoremi. 

6) Definire e dimostrare il Teorema di Herbrand in versione costruttiva. 

Si precisa che tali domande hanno carattere puramente indicativo: le domande effettivamente proposte in sede d’esame potranno divergere, anche in modo significativo, da quelle riportate in questa lista.