Cari studenti,

purtroppo l'esonero del 12/6/02 è andato meno bene del primo, come si vede dai risultati (specialmente se si tiene conto che tutti i voti sono stati scalati rispetto a quello più alto, perché ci fosse almeno un 15).

A vostro beneficio, questa volta nella pagina dedicata alla correzione delle prove di esame riporterò le soluzioni complete a tutte le domande (compreso quelle riguardanti definizioni ed enunciati), perché possiate avere un esempio del livello di precisione necessario ad un esame di Logica Matematica.

Ritengo che il risultato non molto positivo di questo esonero sia in parte dovuto ad un equivoco sulla valenza dei lucidi da me pubblicati. Dovete tenere conto che essi, specialmente quelli che sono stati scritti direttamente durante le lezioni, non possono sostituire un libro di testo oppure appunti completi delle lezioni, in quanto mancano del tutto i raccordi tra lucido e lucido e le integrazioni a voce (nonostante sui lucidi sia riportato molto più di quanto solitamente si scriva alla lavagna). Inoltre, a causa delle sue dimensioni limitate e per evitare di spezzare la presentazione di un concetto su più lucidi (a meno che ciò non sia strettamente necessario), la presentazione su lucidi risulta molto succinta e necessariamente incompleta. Pertanto i lucidi vanno considerati come una traccia, anche se molto capillare e particolareggiata, del programma e non come libro di testo ufficiale del corso da mandare giù a memoria.

Al di là dei problemi riconducibili ad un uso non corretto dei lucidi, ho riscontrato che i seguenti punti non sono stati ben compresi o applicati:

- nel caso di tableaux con variabili libere

• la delta-regola deve sempre introdurre simboli nuovi di Skolem dipendenti da tutte le variabili libere presenti sul ramo cui essa viene applicata
• le sostituzioni debbono essere applicate contemporaneamente a tutti i rami
• non è possibile unificare letterali del tipo R(x) e not R(f(x)), in quanto ogni sostituzione {t/x} dà luogo ai due letterali R(t) e not R(f(t)) (che certamente non sono complementari). Ciò è dovuto alla contemporanea presenza della variabile x sia in R(x) che in not R(f(x)). In questi casi occorre creare almeno una nuova occorrenza di uno dei due letterali in questione che utilizzi un’altra variabile. Come? Riutilizzando opportunamente la gamma-regola sulla stessa gamma formula per cui era stata introdotta la variabile libera x (si veda la correzione della prova di esonero A per un esempio concreto di questo punto)

- nel caso di tableaux con o senza variabili libere, conviene applicare le regole di espansione/sostituzione secondo il seguente ordine:

• alfa-regola
• beta-regola
• delta-regola
• gamma-regola
• regola di sostituzione

- nel corso della costruzione di un tableau, non è consentita alcuna semplificazione al di fuori dell’applicazione delle regole di espansione o di una sostituzione

- se si intende dimostrare che una formula F del I ordine è valida nel sistema della risoluzione, si può procedere nella seguente maniera:

• sia G = not F
• supponiamo che dopo semplici manipolazioni proposizionali la formula G raggiunga la forma G₁ and G₂ and … and G_k . In questo caso, anziché trasformare G prima in forma normale prenessa e poi in forma normale di Skolem, sarà sufficiente trasformare ciascuna G_i in forma normale prenessa e poi in forma normale di Skolem H_i per poi procedere a mettere insieme tutte le clausole generate da ciascuna H_i, per i=1,2,…,k. Ciò avrà l’effetto di semplificare non solo la procedura in sé, ma anche le clausole risultanti. Infatti, quando è possibile, conviene sempre evitare inutili dipendenze di quantificatori esistenziali da quantificatori universali. (Anche questo punto sarà opportunamente illustrato nella correzione della prova di esonero A.)

- quando si intende dimostrare una formula mediante un sistema refutazionale (quale quello dei tableaux o quello della risoluzione) come primo passo si deve negare la formula.

A questo punto non mi resta che augurarvi che, mettendo a frutto le raccomandazioni appena fatte, possiate affrontare con maggiore sicurezza le prossime prove di esame.

Domenico Cantone