Logica computazionale (2006/2007)

Corso a esaurimento

Codice insegnamento
4S01115
Docenti
Andrea Masini, Ruggero Ferro
Coordinatore
Andrea Masini
crediti
5
Settore disciplinare
MAT/01 - LOGICA MATEMATICA
Lingua di erogazione
Italiano
Periodo
3° Q dal 2-apr-2007 al 8-giu-2007.

Orario lezioni

Obiettivi formativi

Aritmetizzazione della sintassi; aritmetiche con assiomatizzazioni minime per ottenere sufficiente rappresentabilità. Indecibilità, incompletezza di teorie effettive sufficientemente ricche. Indimostrabilità della consistenza all'interno di una teoria assiomatizzabile sufficientemente ricca.
Il calcolo dei sequenti LK. Relazioni con i sistemi alla Hilbert. L'eliminazione del taglio.Proprietà della sottoformula e consistenza del calcolo puro dei predicati. Eliminazione del taglio per teorie matematiche del I ordine.
Intuizionismo, Interpretazione BHK. Il calcolo dei sequenti LJ. Relazioni tra logica classica e logica intuizionista. Intuizionismo e teoria dei tipi. La logica lineare (cenni)

Programma

Aritmetizzazione della sintassi; aritmetiche con assiomatizzazioni minime per ottenere sufficiente rappresentabilità. Indecibilità, incompletezza di teorie effettive sufficientemente ricche. Indimostrabilità della consistenza all'interno di una teoria assiomatizzabile sufficientemente ricca.
Il calcolo dei sequenti LK. Relazioni con i sistemi alla Hilbert. L'eliminazione del taglio.Proprietà della sottoformula e consistenza del calcolo puro dei predicati. Eliminazione del taglio per teorie matematiche del I ordine.
Intuizionismo, Interpretazione BHK. Il calcolo dei sequenti LJ. Relazioni tra logica classica e logica intuizionista. Intuizionismo e teoria dei tipi. La logica lineare (cenni)

Modalità d'esame

Prova scritta