Logica Matematica   Anno Accademico 2007/2008   Docente: Dr Damiano Macedonio   Dipartimento di Informatica   Università Ca' Foscari di Venezia

Contenuti

• Comunicazioni
• Informazioni generali
• Descrizione Generale
• Materiale didattico
• Programma svolto

Comunicazioni

• Eccovi i risultati dello scritto del 01 settembre 2008.
• Per qualsiasi questione mandatemi una mail con subject: [logica]...

Informazioni Generali

• Lezioni
• Periodo: Primo Semestre
• Orario: Lunedì 11:00-13:00; Giovedì 14:00-16:00
• Ricevimento: Lunedì 14:00-16:00.
• Ufficio: stanza n.7 (Assegnisti/Ospiti).

Descrizione Generale

• Obiettivi formativi
  Il corso si propone di introdurre la logica matematica e di chiarire come essa sia ausiliaria alle altre materie. Temi centrali sono la distinzione tra sintassi e semantica, la formalizzazione di proprietà nel linguaggio logico e il concetto di dimostrazione corretta, basata su regole generali prefissate. Verranno presentate tecniche per produrre prove e controesempi.
• Programma
  • Livelli di riferimento. Linguaggio e meta-linguaggio.
  • Logica proposizionale e predicativa (classica e intuizionista).
  • Introduzione del calcolo dei sequenti con le equazioni definitorie. Sistemi LJ e LK. Teorema di eliminazione dei tagli. Ricerca delle prove.
  • Interpretazione classica delle formule, sia proposizionale che predicativa. Teoremi di Correttezza, Completezza e Compattezza per il calcolo LK.
  • Problema della decisione per il calcolo predicativo.
  • Teoremi di incompletezza.

Testi e Materiale Didattico

• Testi Addottati
  • [Sambin07] Giovanni Sambin.
    Per Istruire un Robot, Prima Parte. Libreria Progetto, Padova 2007.
  • [AspCiab97] Andrea Asperti, Agata Ciabattoni.
    Logica a Informatica, McGraw-Hill 1997.
• Testi di Approfondimento
  • Giovanni Sambin.
    Per Istruire un Robot, Seconda e Terza Parte. Libreria Progetto, Padova 2007.
  • Martin Davis.
    Il calcolatore universale. Da Leibniz a Turing, Biblioteca Scientifica Adelphi 2003.
  • Achille Varzi, John Nolt, Dennis Rohatyn
    Logica 2/ed, McGraw-Hill 2006.
• Appunti
  Eccovi alcuni appunti che approfondiscono le cose viste a lezione e riportano alcuni esercizi.
  Non esitate a scrivermi se avete osservazioni, dubbi, domande e soprattutto se trovate errori:
  Fate attenzione perché... ciò che ho scritto contiene almeno un errore. [David Makinson, the Preface Paradox]
  • [D1] Calcolo dei sequenti: i sistemi LJ e LK [pdf]
  • [D2] Principio di induzione applicato alle derivazioni [pdf]
    (10 ottobre 07) Ho modificato la discussione del caso base nell'esercizio, spero sia più chiaro.
  • [D3] Un altro esercizio su induzione e derivazioni [pdf]
  • [D4] Come costruire una derivazione: il caso proposizionale [pdf]
    (11 ottobre 07) Ho aggiunto le parentesi al punto 7 dell'esercizio 1.
  • [D5] Calcolo dei Sequenti Predicativo: Note ed Esercizi [pdf]
  • [D6] Linguaggio Quotidiano: Esercizi di Formalizzazione [pdf]
  • [D7] Linguaggio Quotidiano: Due Esercizi Risolti [pdf]
  • [D8] Secondo Teorema di Incompletezza: la dimostrazione in dettaglio [pdf]

Programma Dettagliato

• 24 set 2007. Introduzione: Capitolo 1 di [Sambin07]. Sintassi e semantica, livelli di riferimento.
• 27 set 2007. Pricipio di riflessione: Capitolo 2, paragrafi 1-4 di [Sambin07]. Costruzione del calcolo dei sequenti. Equazioni definitorie per i connettivi and e or.
• 01 ott 2007. Pricipio di riflessione: Capitolo 2, paragrafi 5-6 di [Sambin07]. Equazioni definitorie per il connettivo implicazione. Regole strutturali. Calcoli LJ e LK.
• 04 ott 2007. Negazione: Capitolo 2, paragrafi 7-8 di [Sambin07] e Capitolo 2, paragrafi 2.1,2.5 di [AspCiab97]. Assiomi per le costanti top e bottom. Regole per il connettivo negazione. Principio di non contraddizione in LJ e LK. Principio di doppia negazione, principio del terzo escluso e riduzione ad assurdo in LK.
• 08 ott 2007. Induzione e derivazioni: Appunti [D2]. Teorema di eliminazione dei tagli in LK: Capitolo 2, paragrafo 2.5.1 di [AspCiab97]. Principio di induzione su naturali, derivazioni e formule. Teorema di eliminazione dei tagli, con idea della dimostrazione per mutua induzione.
• 11 ott 2007. Proprietà delle derivazioni. Ricerca delle prove, esercizi: Capitolo 2, paragrafi 2.5.2, 2.5.3 e 2.6 di [AspCiab97]; appunti [D3] e D[4]. Proprietà della sottoformula e non derivabilità del taglio. Come si sfrutta la proprietà della sottoformula nella ricerca delle prove, alcuni suggerimenti si trovano negli appunti.
• 15 ott 2007. Valutazione classica delle formule proposizionali: Capitolo 1, paragrafi 1.1, 1.2, 1.3 e 1.4 di [AspCiab97]. Interpretazione classica delle formule proposizionali nel reticolo {0,1}. Tavole di verità. Formule soddisfacibili e insoddisfacibili. Tautologie. Esempi.
• 22 ott 2007. Conseguenza semantica: Capitolo 1, paragrafo 1.4, Definizione 1.22, Teorema 1.23, Definizione 3.19 di [AspCiab97]. Formule come conseguenza semantica di insiemi di formule. Insiemi di formule come conseguenza semantica di insiemi di formule. Esempi. N.B. L'approccio descritto a lezione è diverso (ma equivalente!) a quello del libro.
• 25 ott 2007. Teorema di deduzione semantica. Teorema di correttezza. Teoremi 1.14 e 1.15; Teorema 3.20 di [AspCiab97]. Dal Teorema 3.20 (dato implicitamente su insiemi finiti) si deriva il teorema di correttezza visto a lezione [per ulteriori chiarimenti, invito gli studenti non-frequentanti al ricevimento del lunedì].
• 29 ott 2007. Insiemi consistenti e massimali: definizioni e proprietà. Definizioni 3.3 e 3.7; Lemmi 3.4, 3.6, 3.8 e 3.9 di [AspCiab97]. Si tratta delle basi per la prova del teorema di completezza. N.B. Nella versione vista a lezione, la derivabilità sintattica è data dal Calcolo dei Sequenti (LK) e non dalla Deduzione Naturale come fatto dal libro. Cercate quindi di seguire le prove del libro considerando il calcolo LK.
• 05 nov 2007. Consistenza e Soddisfacibilità. Teorema di Completezza. Teorema di Compattezza. Capitolo 3, Sezioni 3.1 e 3.3; Teorema 1.18 di [AspCiab97]. Dato un insieme di formule consistente abbiamo mostrato come definire una valutazione che lo soddisfi. Abbiamo quindi provato la proprietà fondamentale che lega semantica e sintassi: un insieme di formule ben formate è consistente se e solo se è soddisfacibile. Da essa abbiamo derivato i teoremi di Completezza e Compattezza.
• 08 nov 2007. Logica dei predicati: sintassi e intuizione semantica. Capitolo 4, Sezioni 4.1 e 4.2 e 3.3 di [AspCiab97] e appunti [D5]. Linguaggio predicativo, variabili libere e legate, sostituzione.
• 12 nov 2007. Calcolo del primo ordine. Appunti [D5]. Equazioni definitorie e regole per i quantificatori universale ed esistenziale. Calcoli LJ e LK al primo ordine. Esempi di derivazione.
• 15 nov 2007. Calcolo del primo ordine: esercizi e formalizzazioni. Appunti [D5] e Capitolo 4 Sezione 4.3.6 di [AspCiab97]. Derivazioni in LJ e LK. Paradosso del barbiere. Introduzione del predicato di uguaglianza nel linguaggio predicativo. Aritmetica di Peano.
• 19 nov 2007. Calcolo LK: forma normale prenessa e forma normale disgiuntiva. Teoremi del Capitolo 4 Sezione 4.3.3 di [AspCiab97]. Attenzione: Abbiamo definito l'equivalenza tra formule usando il concetto di derivabilità in LK, e non abbiamo considerato la semantica come fa il libro di testo. I teoremi della Sezione 4.3.3. sono stati dimostrati utilizzando il calcolo dei sequenti LK.
• 22 nov 2007. Logica dei predicati: semantica. Capitolo 4 Sezione 4.3, Lemma 4.29 di [AspCiab97]. Strutture e ambienti. Valutazione dei termini e delle formule. Lemma di non interferenza e Lemma di sostituzione.
• 26 nov 2007. Logica dei predicati: conseguenza semantica e correttezza. Sezione 4.3.1, Teorema 5.1 (nel caso del calcolo LK), Esercizio 4.7 (senza dimostrazione) di [AspCiab97] . Soddisfacibilità, validità e modelli. Lemma di traslazione (solo enunciato). Teorema di correttezza per il calcolo dei sequenti al primo ordine.
• 29 nov 2007. Insiemi di Henkin e soddisfacibilità. Sezione 5.1.1 di [AspCiab97]. Proprietà degli insiemi di Henkin. Interpretazione canonica. Ogni insieme di Henkin consistente massimale è soddisfacibile.
• 03 dic 2007. Teorema del modello e Teorema di completezza per il calcolo LK. Sezione 5.1.1 di [AspCiab97]. Estensione di insiemi di formule a insiemi di Henkin. Teorema di Lindembaum (solo enunciato per il caso non numerabile). Soddisfacibilità per insiemi consistenti. Completezza.
• 17 dic 2007. Teoremi di incompletezza: introduzione. Sezione 5.5 pag.172-174 di [AspCiab97]. Cenni storici. Programma logicista di Hilbert. Contributo di Gödel. Definizione di Teoria (Def. 5.36) e Teoria Completa (Def. 5.37). Nozione di teoria assiomatizzabile e numerali. Numero di Gödel.
• 20 dic 2007. Teoremi di incompletezza: enunciati e dimostrazioni. Sezioni 5.5, 5.5.1 e 5.5.2 di [AspCiab97]. Predicati di provabilità e Teorema di diagonalizzazione. Primo e secondo Teorema di incompletezza di Gödel.
• 07 gen 2008. Equivalenza semantica. Forma Normale Prenessa e Forma di Skolem. Definizione 4.28 e Sezione 4.3.5 di [AspCiab97] .
• 10 gen 2008. Poblema della decisione. Teoria di Herbrand. Sezione 5.4.1 di [AspCiab97]. Sezioni 6.1 e 6.1.1 di [AspCiab97] senza dimostrazioni. Teorema della chiusura esistenziale (Teorema 4.26). Teorema di Church sulla decidibilità della logica al primo ordine (Teorema 5.25, senza dimostrazione). Interpretazione di Herbrand. Espansione di Herbrand. Teorema di Herbrand. Algoritmo che semi-decide la non soddisfacibilità di una formula.