problema tradizionale della logica: determinare forme di ragionamento valide indipendentemente dalle interpretazioni

• obiettivo: costruzione di algoritmi deduttivi

il metodo dei tableau analitici permette di determinare algoritmicamente tutte le verità logiche predicative

• cos'è un tableau analitico?   un albero (tanto per cambiare ;)

i nodi sono etichettati da formule predicative

• proprietà semantica: se in un modello vale la formula alla radice, vi devono valere anche tutte le formule di almeno un ramo dell'albero (fino alla foglia)
• proprietà sintattica: complessità logica degli schemi decrescente (non strettamente) lungo il cammino dalla radice alla foglia

regole di costruzione: v. appresso (alcune espresse da alberi: regole tableau)

N.B. t, t_i indicano termini chiusi qualsiasi, mentre a è una costante individuale univocamente determinata dalla formula: testimone della formula, o costante di Henkin)

esiste qualcuno che se è C (con il cappello) allora tutti sono C

• ⊢ ∃x(Cx → ∀y Cy)

si dimostra per refutazione del contrario:

1. ¬∃x(Cx → ∀y Cy)
2. ¬(Ca → ∀y Cy)
3. Ca
4. ¬∀y Cy
5. ¬Cb
6. ¬(Cb → ∀y Cy)
7. Cb
8. ¬∀y Cy
9. ⊥

un Φ-tableau è chiuso se tutti i suoi rami terminano in foglie di etichetta ⊥

dalla teoria predicativa Φ si deduce la formula ψ con il metodo dei tableau se esiste un Φ∪{¬ψ}-tableau chiuso

• la deduzione Φ ⊢_T ψ è refutativa

correttezza: Φ ⊢_T ψ ⇒ Φ ⊨ ψ

• poiché ogni teoria che abbia un tableau chiuso è insoddisfacibile

tuttavia, un tableau predicativo può ben essere infinito ... è sempre possibile stabilire se si chiude o meno?

• no!    ⇒ la validità logica predicativa è indecidibile

ciò non toglie che esistano teorie predicative decidibili: ma non tutte lo sono!

• la validità logica proposizionale è decidibile: perché? (v. esercizio 2)

l'indecidibilità della validità logica predicativa non è delle peggiori... vale la sua semidecidibilità, per la completezza della deduzione col metodo dei tableau:

• Φ ⊨ ψ  ⇒  Φ ⊢_T ψ

schema essenziale della dimostrazione: si definiscono i seguenti concetti:

• insieme di Hintikka di dominio D (che include le costanti di Σ): un insieme di Σ(D)-formule predicative "chiuso rispetto alle regole tableau" e che non contiene alcuna formula assieme alla sua negata
• Φ-tableau sistematico: ottenuto dalla teoria Φ per applicazione esaustiva delle regole di costruzione

quindi si dimostra che:

• ogni insieme di Hintikka è soddisfacibile, cioè ha un modello
• Φ è tableau-consistente (i.e. non ha tableau chiusi)  ⇒  il suo tableau sistematico ha un ramo che include Φ ed è un insieme di Hintikka

per i dettagli si veda sez. 2.5 del testo (Manca, 2001)

una formula predicativa è in forma prenessa se consta di una sequenza di quantificazioni, il prefisso, seguita da una formula priva di quantificatori, la matrice

• ogni formula predicativa ne ha una logicamente equivalente in forma prenessa

l'equisoddisfacibilità di formule, come pure di teorie, è una relazione molto meno restrittiva dell'equivalenza logica: non richiede che la segnatura sia la stessa

• ciò è utile a definire trasformazioni in forme normali equisoddisfacibili

ogni enunciato predicativo ψ in forma prenessa può essere trasformato in uno equisoddisfacibile, Skolem(ψ), privo di quantificatori esistenziali: la Skolemizzazione rimpiazza le variabili esistenzialmente quantificate con

• simboli di costante (di Skolem), se il quantificatore non è preceduto da quantificatori universali nel prefisso
• termini f(x₁,...,x_k), se il quantificatore è preceduto da k quantificatori universali nel prefisso, dove f è detta funzione di Skolem e i suoi argomenti sono le precedenti k variabili universalmente quantificate

quantificazione universale implicita delle variabili in una forma di Skolem
+ rappresentazione in CNF della matrice  →  equivalente rappresentazione a clausole

Skolem(Φ) : l'insieme delle forme di Skolem delle forme prenesse ottenute da formule dell'insieme Φ

Σ^*_Φ : la segnatura di Skolem(Φ), estesa con un simbolo di costante qualora Skolem(Φ) sia privo di tali simboli

universo di Herbrand della teoria Φ:

• l'insieme dei termini chiusi di segnatura Σ^*_Φ

espansione di Herbrand della teoria Φ, Herbrand(Φ) :

• la teoria proposizionale ottenuta da Skolem(Φ) istanziandone in tutti i modi possibili le variabili con termini del suo universo di Herbrand

fatto notevole: Φ e Herbrand(Φ) sono equisoddisfacibili

1. La definizione di tableau chiuso data qui corregge una svista nel testo (Manca, 2001), dove secondo la Def. 2.9 " un tableau si dice chiuso se in esso tutte le foglie sono etichettate con ⊥" (che si tratti di una svista è testimoniato dalla dimostrazione della Prop. 2.10 nello stesso testo): spiegare perché, se tale ne fosse la definizione, si potrebbe arguire l'esistenza di tableau chiusi soddisfacibili (produrne uno di esempio a tal fine).
2. Dimostrare che un tableau relativo ad una formula proposizionale è sempre finito, e dunque si può sempre decidere se è chiuso o meno.
3. Dimostrare che la finitezza deduttiva della logica predicativa consegue dalla sua compattezza.