Logica

Obiettivi Formativi

Gli ultimi decenni hanno evidenziato un ruolo sempre maggiore della logica in informatica. Potremmo dire con R.A.Shore che "la logica è per l'informatica quello che è la matematica per la fisica e viceversa" (SHORE R.A. (2001). The prospects for mathematical logic in the twenty-first century, Bulletin of Symbolic Logic 7, pp.169-196).

Il ruolo della logica in informatica è duplice:

• applicativo (ad esempio: strumenti per la verifica del software e dell'hardware; linguaggi di programmazione funzionali; sistemi di tipi per linguaggi funzionali, sistemi automatici di deduzione)
• teorico-fondazionale (ad esempio: teoria dei tipi, teoria della dimostrazione, sviluppo di nuove logiche per sisitemi computazionali)

Scopo del corso è quello di introdurre le nozioni di base della logica simbolica al fine di permettere studi successivi e più approfonditi.

Attività Formativa

Programma

1. Parte 1: logica proposizionale
   1. linguaggio proposizionale:
      connettivi e proposizioni
   2. semantica:
      le tavole di verità
      valutazioni
      conseguenza logica
   3. deduzione naturale:
      il concetto di "dimostrazione":
      regole di introduzione e di eliminazione dei connettivi
   4. correttezza e completezza
2. Parte 2: Logica Dei Predicati
   1. Strutture
   2. linguaggio del I ordine:
      quantificazione
      definizioni per ricorsione sulla sintassi
      sostituzione
   3. semantica:
      interpetazioni
      semantica di Tarski
      conseguenza logica
      identità
   4. un esempio notevole: l'aritmetica di Peano (PA)
   5. deduzione naturale per la logica dei predicati:
      regole per il quantificatore universale
      regole per la quantificazione esistenziale
   6. deduzione naturale e identità
   7. teoremi fondamentali della logica dei predicati:
      teorema di completezza
      teorema di compattezza
      teorema Lowenheim-Skolem