Corso di Logica II

• Richiami sui sistemi deduttivi più utilizzati: calcolo dei sequenti, di deduzione naturale e calcoli alla Hilbert. Differenza della nozione di dimostrazione nei vari sistemi presentati, prove come successioni e prove come alberi. Esempi di dimostrazioni nei vari sistemi. Definizione del calcolo alla Hilbert per la logica classica del I ordine, assiomi e regole. Semantica per il calcolo predicativo, richiami sui concetti di interpretazione, soddisfacibilità, verità e modello e isomorfismo tra interpretazioni.
• Aritmetica di Peano (PA). Definizioni di modello standard e modello non standard per l'aritmetica. Proprietà generali di PA. Cenni sull'aritmetica del II ordine e sui risultati di Presburger.
• Sistema di Robinson (R), proprietà e differenze con PA.
• Funzioni e relazioni ricorsive. Funzioni iniziali e metodi di composizione, ricorsione e mu-operatore. Funzioni e relazioni ricorsive primitive. Esempi. Cenni sulla tesi di Church. Relazioni numeriche e mu-operatore limitato. Insiemi ricorsivamente enumerabili.
• Teorie ricorsivamente assiomatizzabili. Relazioni e funzioni rappresentabili in PA. Relazione tra funzioni ricorsive e funzioni rappresentabili in PA. Eliminazione della ricorsione primitiva; funzione beta di Goedel.
• Aritmetizzazione e codifica. Numeri di Goedel. Ricorsione per decorso sui valori. Definizione di teoria decidibile, indecidibile ed essenzialmente indecidibile.
• Teorie sufficientemente potenti. Predicati debolmente rappresentabili. Teorema di Church, enunciato e dimostrazione. Corollari. Indecidibilità del calcolo dei predicati puro.
• Primo teorema di incompletezza di Goedel, enunciato e dimostrazione mediante il teorema di Church. Cenni sul programma hilbertiano.
• Coerenza e omega-coerenza. Lemma di diagonalizzazione, enunciato e dimostrazione. Primo teorema di incompletezza di Goedel, enunciato e dimostrazione mediante il lemma di Diagonalizzazione. Cenni sul teorema di Goedel-Rosser. Insiemi aritmetici. Teoremi di Tarski, enunciati e dimostrazioni.
• Il predicato Teor() e condizioni di derivabilità di Loeb-Hilbert-Bernays (senza dimostrazione). Secondo teorema di Goedel, enunciato e cenni sulla prova mediante le condizioni di derivabilità.

Bibliografia

1. E.Mendelson, Introduzione alla logica matematica, Boringhieri
2. J.I.Girard, Proof theory and logical complexity, Bibliopolis
3. P.G. Odifreddi, Classical recursion theory, North Holland
4. F. Montagna, Teoria della ricorsività (disponibile su http://www.unicam.it/matinf/aila/scuola.htm)
5. C.Smorynski, Self reference and modal logic, Springer-Verlag
6. S.Artemov, L.Beklemishev, Provability Logic (disponibile su: http://www.phil.uu.nl/preprints/lgps/list.html)
7. A. Visser, An overview on Interpretability Logic (disponibile su: http://www.phil.uu.nl/preprints/lgps/list.html)
8. G.Boolos, R.Jeffrey, Computability and Logic, Cambridge University Press
9. G.Boolos, The Logic of Provability, Cambridge Univ. Press