Il corso è incentrato sulla relazione tra la possibilità di definire un oggetto/problema in un certo linguaggio logico e la complessità computazionale (o algoritmica) dell'oggetto/problema stesso. Questo tema è illustrato attraverso risultati e tecniche classiche e sviluppi recenti. Logica del Primo Ordine: sintassi e semantica. Eliminazione dei quantificatori, teorie decidibili. Definibilità di una query in una logica. Tecniche per dimostrare la non-esprimibilità (Duplicator/Spoiler games, località). Descrizioni logiche di computazioni. Risultati di indecidibilità algoritmica. Il Calcolo dei Predicati. Completezza e Compattezza. Ultrafiltri e ultraprodotti. Applicazioni alla definibilità di queries. Teoremi di Incompletezza di Gödel. Logica della dimostrabilità, logica modale, cenni di logica temporale. Semantica di Kripke. Computazione con oracoli e Gerarchia Aritmetica. Gradi di insolubilità algoritmica. Analisi del contenuto algoritmico di teoremi. Calcolo dei sequenti e cut-elimination.

Dispense fornite dal docente.