Logica Matematica

  Logica Matematica
  Anno Accademico 2010/2011
  Corso di Laurea Magistrale in Ingegneria e Scienze Informatiche
  Università di Verona

  Docente Dr. Damiano Macedonio

Contenuti (ultimo aggiornamento: 20 luglio 2011)

Comunicazioni
Programma del Corso
Materiale Didattico
Lezioni in Dettaglio
Prove di Esame

Comunicazioni

Modalità di esame:
- Il corso rappresenta un modulo dell’esame di Fondamenti (12 CFU), che è composto dagli insegnamenti di Logica (6 CFU) e Linguaggi (6 CFU). Il voto dell’esame di Fondamenti è unico e viene determinato dalla media dei voti ottenuti nei due moduli.
- L’esame consiste in due prove scritte: una per Logica e una per Linguaggi. A discrezione dei docenti, può essere richiesta una eventuale prova orale.
- I due scritti possono essere affrontati in maniera indipendente. L’esame di Fondamenti può essere verbalizzato quando si ottiene la sufficienza (18/30) in entrambi i moduli. Il voto finale viene determinato dalla media dei voti.
- In ogni caso i voti verranno conservati fino a fine settembre 2011, poi sarà necessario ripetere entrambe le prove, anche se una risulta sufficiente.
- Ogni appello prevede due date, tendenzialmente distanziate di sette giorni l’una dall’altra: una data per lo scritto di Logica e una per quello di Linguaggi.
- La data dello scritto di Linguaggi coincide con la data ufficiale dell’appello di Fondamenti pubblicata sul sito di Ateneo. Tale appello è anche verbalizzante.
- La data dello scritto di Logica viene comunicata su questo sito.
- Le date dello scritto di Logica per la sessione autunnale sono:
  - Martedì 13 settembre 2011, ore 10:00 in aula I.
  - Mercoledì 28 settembre 2011, ore 10:00 in aula I.
Ricevimento nel secondo semestre: su appuntamento via e-mail. [ufficio 1.56, primo piano Ca' Vignal 2]
Orario lezioni:
- Primo Semestre.
- Mercoledì 10:30-13:30 aula I.
- Venerdì 10:30-12:30 aula I.
Contatti:
- Università di Verona: damiano.macedonio@univr.it
- Università Ca’ Foscari Venezia: mace@dsi.unive.it
Per qualsiasi questione basta una mail con subject: [logica]...

Programma del Corso

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 contro-esempi.
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.

Materiale Didattico

Top

Testo adottato.
- [AspCiab97] Andrea Asperti, Agata Ciabattoni.
  Logica a Informatica, McGraw-Hill 1997.
Testi di Approfondimento.
- [Sambin07] Giovanni Sambin.
  Per Istruire un Robot, Prima, Seconda e Terza Parte. Libreria Progetto, Padova 2007.
- [Davis03] Martin Davis.
  Il calcolatore universale. Da Leibniz a Turing, Biblioteca Scientifica Adelphi 2003.
- [VarNolRoh06] Achille Varzi, John Nolt, Dennis Rohatyn
  Logica 2/ed, McGraw-Hill 2006.
- Per in confronto tra Logica Classica e Logica Intuizionistica suggerisco l'articolo di Giovanni Sambin:
  Molteplicità delle Logiche e Necessità delle Traduzioni. Logica Intuizionistica e Logica Classica a Confronto. [pdf]
Eccovi alcuni appunti che approfondiscono i concetti visti a lezione e riportano alcuni esercizi. Non esitate a scrivermi se avete osservazioni, dubbi, domande e soprattutto se trovate errori. Fate attenzione... ciò che ho scritto contiene almeno un errore. [David Makinson, the Preface Paradox]
- [SamBatFag00] Giovanni Sambin, Giulia Battilotti, Claudia Faggian. Basic logic: Reflection, symmetry, visibility. The Journal of Symbolic Logic, 65:979-1013, 2000. [pdf]
- [A01] Calcolo dei Sequenti: i sistemi LJ e LK. [pdf]
- [A02] Calcolo dei Sequenti: Induzione e Regole di Inferenza. [pdf] Attenzione: ho riscritto il testo dell’esercizio proposto [17 nov 2010].
- [A03] Calcolo dei Sequenti Proposizionale: Note ed Esercizi. [pdf]
- [A04] Linguaggio Quotidiano e Logica Proposizionale: Formalizzazioni. [pdf]
- [A05] Semantica di Kripke per LJ [pdf]
- [A06] Calcolo dei Sequenti Predicativo: Note ed Esercizi. [pdf]
- [A07] Linguaggio Quotidiano: Formalizzazioni in Logica. [pdf] Due esercizi risolti.
- [A08] Linguaggio Quotidiano e Logica Predicativa: Formalizzazioni. [pdf]
- [A09] Esercitazione di preparazione all'esame. [testo] [soluzione]

Lezioni in Dettaglio

Top

20 ott 2010 [2h]. Introduzione, pagg. XV-XIX e Capitolo 1, paragrafo 1.1 di [AspCiab97].
Sintassi e semantica, livelli di riferimento.
Un buon approfondimento per capire i livelli di riferimento è il Capitolo 1 di [Sambin07].
22 ott 2010 [2h]. Pricipio di riflessione.
Costruzione del calcolo dei sequenti. Equazione definitoria per il connettivo and e sua risoluzione.
Nota. Il principio di riflessione e le equazioni definitorie sono state introdotte in [SamBatFag00]. I paragrafi 1 e 2 di tale articolo illustrano lo spirito delle equazioni definitorie e mostrano come si risolvono. Un altro buon approfondimento sulle equazioni definitorie è il Capitolo 2, paragrafi 1-4 di [Sambin07].
29 ott 2010 [2h]. Pricipio di riflessione.
Equazioni definitorie per i connettivi or e implica e loro risoluzione.
Nota. Dei buoni approfondimenti sono ancora [SamBatFag00] e il Capitolo 2, paragrafo 5 di [Sambin07].
05 nov 2010 [2h]. Calcoli LJ e LK: Logica Classica e Logica Intuizionistica. Appunti [A01] e Capitolo 2, paragrafi 2.1-2.5 di [AspCiab97].
Regole strutturali. Liberalizzazione dei contesti. Introduzione delle costanti top e bottom: assiomi ed equazioni definitorie.
Nota. Dei buoni approfondimenti sono ancora [SamBatFag00] e il Capitolo 2, paragrafi 6-7 di [Sambin07].
10 nov 2010 [3h]. Negazione: Capitolo 2, paragrafi 2.1,2.5 di [AspCiab97]. Principio di induzione e derivazioni: Appunti [A02].
Assioma, regola ed equazione definitoria per la costante 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. Consequentia Mirabilis in LK e sua traduzione in LJ. Esempi di dimostrazioni sfruttando la tecnica offerta dalla consequentia mirabilis. Definizione formale di formule ben formate, derivazioni (in LJ e LK) e sequenti derivabili. Applicazione del principio di induzione alle derivazioni: descrizione del principio ed esercizi.
Nota. Approfondimenti sulla negazione e i principi di LK ed LJ si trovano in Capitolo 2, paragrafi 7-8 di [Sambin07]. Una breve discussione sulla consequentia mirabilis si trova su wikipedia.
12 nov 2010 [2h]. Principio di induzione e derivazioni: appunti [A02]. Teorema di eliminazione dei tagli: paragrafo 2.5.1 di [AspCiab97].
Esercizi sulle derivazioni. Gentzen’s Houptsatz: idea della dimostrazione per mutua induzione su grado/livello del taglio. Conseguenze del teorema su LJ, in particolare non derivabilità del principio del terzo escluso.
17 nov 2010[3h]. Corollari al teorema di eliminazione dei tagli: paragrafi 2.5.1-2.5.3-2.5.4-2.6 di [AspCiab97]. Ricerca delle derivazioni: appunti [A03]. Linguaggio quotidiano: appunti [A04].
Conseguenze del teorema di eliminazione dei tagli su LJ: non derivabilità dei principi di doppia negazione e di riduzione ad assurdo, non derivabilità della consequentia mirabilis. Proprietà della sottoformula. Non derivabilità della regola del taglio. Non derivabilità del bottom. Esercizi sulla ricerca delle prove e sulla formalizzazione del linguaggio quotidiano in linguaggio proposizionale.
19 nov 2010 [2h]. Valutazione classica delle formule proposizionali: Capitolo 1, paragrafi 1.1-1.2-1.3-1.4 (pag. 8-14) di [AspCiab97]. Interpretazione classica delle formule proposizionali nel reticolo {0,1}. Funzione di valutazione. Tavole di verità. Esempi: Lemma 1.6 e Teorema 1.23, con Definizione 1.22, di [AspCiab97].
24 nov 2010 [3h]. Soddisfacibilità, insoddisfacibilità e conseguenza semantica: Capitolo 1, paragrafo 1.4 (pag. 8-14), Definizione 3.19 di [AspCiab97]. Formule soddisfacibili e insoddisfacibili. Tautologie e contraddizioni. Formule come conseguenza semantica di insiemi di formule. Insiemi di formule come conseguenza semantica di insiemi di formule. Esempi. Teorema di deduzione semantica. Validità semantica della regola di riflessione implicita per l’implicazione. N.B. L’approccio descritto a lezione è diverso (ma equivalente!) a quello del libro.
01 dic 2010 [3h]. Validità semantica delle regole dei sistem LK ed LK-II, teorema di Validità e teorema di Completezza Finita: Capitolo 3, paragrafo 3.3 di [AspCiab97]. Concetto di validità di un sequente. Conservzione della validità nel sistema LK: per ogni regola (logica, strutturale o di taglio) di LK, se le premesse sono valide semanticamente allora anche la conclusione è valida semanticamente. Conservzione della validità nel sistema LK-II: per ogni regola logica di LK-II, le premesse sono valide se e solo se anche la conclusione è valida. Teorema di Validità (o Correttezza) per LK. Teorema di Completezza Finita per LK: la dimostrazione sfrutta l’invertibilità semantica delle regole di LK-II e fornisce una procedura di ricerca della derivazione di un sequente valido.
03 dic 2010 [4h]. Applicazioni del teorema di Validità e Completezza Finita: Capitolo 1, paragrafi 1.4.4-1.4.5-1.4.6 (pag. 20-27), Esempio 1.6, Esercizio 1.4 di [AspCiab97]. Cut-elimination semantica: un sequente derivabile in LK è semanticamente valido ed implicitamente contiene un numero finito di formule; possiamo quindi sfruttare la procedura mostrata nella dimostrazione del teorema di Completezza per ottenere una derivazione in LK-II e concludere che il sequente è derivabile anche in LK grazie al fatto che le regole di LK-II sono derivabili in LK senza usare tagli. Contromodello di un sequente: se una sequente non è valido sotto una certa valutazone allora esso non può essere derivato in LK. Equivalenza logica ed equivalenza semantica. Formule classicamente equivalenti. Forme normali: congiuntiva e disgiuntiva. Esistenza delle forme normali ed esempi. Costante falso e insoddisfacibilità. Esempi.
10 dic 2010 [2h]. Verso una prova costruttiva del teorema di Compattezza: Capitolo 3, paragrafo 3.1, Definizioni 3.3 e 3.7; Lemmi 3.4, 3.6, 3.8 e 3.9 di [AspCiab97]. Insiemi consistenti e loro principali proprietà. In particolare, la loro connessione con il teorema di compattezza: un insieme di formule ben formate è consistente se e solo se ogni suo sottoinsieme finito è soddisfacibile. Insiemi consistenti massimali: chiusura per derivabilità e loro comportamento rispetto ai connettivi logici. Si tratta delle basi per la prova costruttiva del teorema di compattezza che ci permette di estendere il teorema completezza a insiemi infiniti di formule ben formate. 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.
15 dic 2010 [3h]. Consistenza e soddisfacibilità, teoremi di Compattezza e di Completezza: Capitolo 3, Sezioni 3.1 e 3.3; Teorema 1.18 di [AspCiab97]. Ogni insieme consistente massimale è soddisfacibile e sappiamo come costruire la valutazione che lo soddisfa. Ogni insieme consistente è contenuto in un insieme consistente massimale, e sappiamo come costruire la sua estensione massimale. Quindi 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 Compattezza e Completezza. N.B. La dimostrazione del teorema di Compattezza vista a lezione differisce da quella che si trova nel libro. Potete trovare qui una dispensa che segue l’idea della dimostrazione del teorema di Compattezza nella forma vista a lezione. Interessante anche la biografia di John Wilder Tukey (1915-2000), ovviamente per cultura personale e non ai fini dell’esame.
17 dic 2010 [2h]. Modello di Kripke per la logica intuizionista (calcolo LJ): appunti [A05]. Modello ad albero e suo rapporto col modello della logica classica. Monotonia di Kripke. Valutazione delle formule ben formate: definizione. Vadità di formule ben formate, di insiemi di formule e di sequenti.
21 dic 2010 [2h]. Modello di Kripke per la logica intuizionista (calcolo LJ): appunti [A05]. Proprietà della valutazione dei sequenti. Dimostrazione che le regole per l'implicazione preservano la validità. Teorema di Validità (con traccia di dimostrazione). Teorema di Completezza (solo enunciato). Esempi ed esercizi.
12 gen 2011 [3h]. Logica dei predicati: sintassi e intuizione semantica. Capitolo 4, Sezioni 4.1-4.2-4.2.3-4.2.4 di [AspCiab97] e appunti [A06]. Linguaggio predicativo, variabili libere e legate, sostituzione. Intuizioni sulla semantica: formalizzazioni dal linguaggio quotidiano.
14 gen 2011 [3h]. Calcolo del primo ordine: appunti [A06]. Equazioni definitorie e regole per i quantificatori universale ed esistenziale. Calcoli LJ e LK al primo ordine. Esempi di derivazione e formalizzazioni dal linguaggio quotidiano.
17 gen 2011 [3h]. Ricerca delle prove: Capitolo 4 Sezione 4.3.6 (Uguaglianza), Capitolo 5 Sezioni 5.3-5.3.1-5.3.2-5.3.4-5.4.1 di [AspCiab97] e appunti [A06]. Introduzione del predicato di uguaglianza nel calcolo ed esempi. Consiglio di guardare anche gli appunti [A07]. Esempi di derivazione del calcolo dei sequenti al primo ordine: paradosso del barbiere (Esempio 4.9 del libro), esempi con quantificatori e contrazione (tratti dagli appunti [A06]). Invertivibilità delle regole di LK. Calcolo LK-II e algoritmo di ricerca della derivazione di un sequente. Cenni sulla semi-decidibilità della derivabilità di un sequente. Teorema di Church (enunciato).
19 gen 2011 [3h]. 07 gen 2008. Equivalenza semantica. Forma Normale Prenessa. Definizione 4.28, Teoremi della Sezione 4.3.3, Sezione 4.3.4 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.
21 gen 2011 [3h]. Logica dei predicati: semantica. Capitolo 4 Sezioni 4.3-4.3.1-4.3.5-5.4.1, Lemma 4.29 (senza dimostrazione) Teoremi 5.1-5.14 (senza dimostrazione, nel caso del calcolo LK), Esercizio 4.7 (senza dimostrazione) di [AspCiab97]. Strutture e ambienti. Valutazione dei termini e delle formule. Lemma di non interferenza, Lemma di sostituzione, Lemma di traslazione (solo enunciati). Soddisfacibilità, validità e modelli. Chiusura universale ed esistenziale. Conseguenza semantica. Teorema di validità e correttezza (solo enunciato). Forma di Skolem (idea, senza dimostrazioni) e in-decidibilità della soddisfacibilità di una formula predicativa. Cenni all'interpretazione di Herbrand e all'algoritmo che semi-decide la non soddisfacibilità di una formula (per chi fosse interessato, la trattazione completa si trova alla Sezione 6.1 di [AspCiab97]).

Prove di Esame

Top

mace@dsi.unive.it