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.

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.