Programma dettagliato di
Logica Matematica
Anno Accademico 2001/2002
Prof. Domenico Cantone
PARTE I: LOGICA PROPOSIZIONALE
- Alfabeto della logica proposizionale
- lettere proposizionali
- costanti proposizionali
- connettivi proposizionali
- simboli ausiliari
- Formule ben formate proposizionali (fbf)
- minimo insieme P tale che ...
- dimostrazione che un'espressione è una fbf
- dimostrazione che un'espressione non è una fbf
- alberi di derivazione
- alberi sintattici
- sottoformule
- principio di induzione strutturale, esempi
- principio di ricorsione strutturale (solo enunciato), esempi
- Semantica della logica proposizionale classica
- assegnamenti e valutazioni booleane
- semantica dei connettivi e delle costanti proposizionali
- Lemma: se due valutazioni booleane v e v' coincidono sulle lettere
proposizionali di una fbf X, allora v(X) = v'(X).
- formule soddisfacibili (modelli), insoddisfacibili, tautologie
- proprietà della relazione di soddisfacibilità (es. v sodd. X or Y se e
solo se v sodd. X oppure v sodd. Y)
- metodo delle tavole di verità per il problema della soddisfacibilità
- conseguenza semantica (X è conseguenza semantica di un insieme di
fbf G se e solo se ogni valutazione booleana che soddisfa tutte le
fbf di G soddisfa anche X)
- Lemma: X è conseguenza semantica di un insieme di fbf G se e solo se
G U {not X} è insoddisfacibile
- Teorema (deduzione semantica)
Y è conseguenza semantica di {X1, ..., Xn} se e solo se
Xn implies Y è conseguenza semantica di {X1, ...,
Xn-1}
- teorema di compattezza proposizionale
- esempio di formalizzazione
- equivalenza semantica (X e Y sono semanticamente equivalenti se
v(X) = v(Y), per ogni valutazione booleana v
- definizione di sostituzione (di una formula al posto di una lettera
proposizionale) mediante ricorsione strutturale
- teorema della sostituzione
- forme normali disgiuntive e congiuntive
- algoritmo per la trasformazione di una fbf in forma normale (mediante
manipolazione dell'albero sintattico)
- definizione di letterale
- Sistemi deduttivi
- proprietà desiderabili in un sistema deduttivo:
- chiusura per istanziazioni e per composizione (regola del taglio)
- regole di introduzione e di eliminazione dei connettivi and, or,
implies
- regole di introduzione e eliminazione di not (con brevi cenni sulla
logica intuizionistica
- correttezza
- completezza
- sistema dei tableaux proposizionali
- suddivisione delle regole in alfa- e beta-regole
- definizione di ramo chiuso e di tableau chiuso
- definizione di teorema nel sistema dei tableau
- correttezza del sistema dei tableau
- ipotesi di strettezza
- lemma di König
- saturazione di un tableau in ipotesi di strettezza (terminazione)
- completezza del sistema dei tableau
- uso dei tableau per la costruzione di controesempi
- conseguenza logica nel sistema dei tableaux
- correttezza e completezza forte del sistema dei tableaux (solo
enunciato)
- sistema della risoluzione proposizionale
- regola di risoluzione binaria, risolvente
- deduzione mediante risoluzione
- refutazione per risoluzione
- correttezza e completezza forte del sistema della risoluzione (solo
enunciato)
- sistemi assiomatici di Hilbert
- assiomi, regole di inferenza
- dimostrazione e derivazione
- teorema e conseguenza logica
- schemi di assiomi per la logica proposizionale, esempi di
dimostrazioni
- teorema della deduzione (solo enunciato), esempi
- correttezza e completezza forte del sistema di Hilbert (solo
enunciato)
PARTE II: LOGICA DEL PRIMO ORDINE
- Introduzione alla logica del I ordine
- problemi di formalizzazione con la logica proposizionale
- oggetti, relazioni, quantificatori
- universo del discorso
- relazione tra quantificatore universale e congiunzione
- relazione tra quantificatore esistenziale e disgiunzione
- relazione tra quantificatore universale ed esistenziale
- funzioni
- Sintassi della logica del I ordine
- Linguaggio della logica del I ordine
- costanti e variabili individuali
- simboli funzionali
- simboli relazionali
- Esempi di linguaggi del I ordine
- linguaggio della teoria dei numeri
- linguaggio della teoria degli ordinamenti parziali
- linguaggio della teoria dei gruppi
- costanti e variabili individuali, simboli funzionali e relazionali
- termini, sottotermini e alberi sintattici
- formule ben formate, sottoformule e alberi sintattici
- quantificatori, variabili libere e variabili legate
- formule chiuse
- notazione per la sostituzione di termini a variabili in una fbf
- termine libero per una variabile in una fbf
- notazione uniforme per la logica del I ordine
- Semantica della logica del I ordine
- Modelli: domini e interpretazioni
- Assegnamenti in un modello
- Interpretazione dei termini in un modello
- Assegnamenti x-varianti
- Interpretazione delle fbf in un modello
- Fbf vere in un modello
- Fbf valide
- Fbf soddisfacibili in un modello
- Fbf soddisfacibili e insoddisfacibili
- Alcune proprietˆ delle interpretazioni
- Chiusura universale e chiusura esistenziale di un fbf aperta; proprietˆ
- Conseguenza semantica nella logica del I ordine
- Relazione tra validitˆ e insoddisfacibilitˆ
- Equivalenza semantica
- Leggi notevoli di trasformazione di fbf con quantificatori
- Forma normale prenessa; esempi
- Forma normale di Skolem
- Algoritmo di skolemizzazione; esempi
- Sistemi deduttivi per la logica del I ordine
- Sistema dei tableaux
- Sistema dei tableaux per la logica del I ordine con formule chiuse;
esempi; correttezza e completezza forte
- Problema dell'istanziazione della gamma-regola
- Sostituzioni; composizione di sostituzioni; sostituzione libera per
una formula
- Sistema dei tableaux con variabili libere; regola di sostituzione
- Correttezza e completezza forte
- Unificazione; coppie di disaccordo; algoritmo di unificazione; esempi
- Sistema della risoluzione
- Regola di risoluzione binaria
- Regola di fattorizzazione
- Correttezza e completezza forte
- Sistema assiomatico di Hilbert
- Assioma di istanziazione universale
- Reogla di generalizzazione universale
- Correttezza e completezza forte
- Teorema della deduzione; esempi