Logica matematica/Calcolo delle proposizioni/I tableaux semantici

Template:Logica matematica

I tableaux semantici sono stati introdotti da Jaakko Hintikka ed Evert Willem Beth alla fine degli anni '50, poi ripresi da Raymond Smullyan in First order logic e rielaborati successivamente da Melvin Fitting e Reiner Hähnle.

Sintassi e regole di inferenza

Formule segnate

Prima di esporre le regole del calcolo, è necessario a tal fine definire il concetto di formula segnata; una formula segnata è una proposizione a cui è assegnato un valore di verità, cioè viene assunta come vera o falsa. Per fare ciò, si utilizzano i simboli $T$ e $F$ : essi fungono da operatori, assegnando alle formule un valore booleano, rispettivamente vero e falso. Quest'operazione è detta valutazione booleana.

Diamo ora una definizione formale: Template:Definizione

Formule congiuntive e disgiuntive

Lo schema proposto da Smullyan, per la scomposizione delle formule del calcolo proposizionale, suddivide esse in due categorie. Secondo questo schema, una formula del calcolo proposizionale, che non sia un atomo, appartiene a una delle due seguenti categorie:

α-formula: formula proposizionale congiuntiva, la cui soddisfacibilità equivale alla soddisfacibilità di entrambe le sue componenti;
β-formula: formula proposizionale disgiuntiva, la cui soddisfacibilità equivale alla soddisfacibilità di almeno una tra le sue due componenti.

In altre parole, lo schema raggruppa in due categorie tutte le formule del calcolo proposizionale del tipo $(\neg A)$ e $(A \circ B)$ , con $\circ \in {\lor, \land, \to, \leftrightarrow}$ : quelle che agiscono congiuntivamente e quelle che agiscono disgiuntivamente.

Regole di espansione

La scomposizione di Smullyan è usata per definire le corrispondenti regole per i tableaux, o regole di espansione dei tableaux. Per ogni connettivo logico è definita la corrispondente $T$ -regola e $F$ -regola, cioè la regola che assegna i valori di verità agli operandi, in base al connettivo e al valore booleano della corrispondente formula; la sigla a destra della riga sta a indicare la rispettiva regola. La virgola va letta come un "and", mentre la barra verticale come un "or".

S è l'insieme di formule segnate precedentemente sviluppate, cioè la parte di formula congiuntiva da lasciare inalterata.

Template:Definizione

Validità delle regole

Dimostrare la validità delle regole per i tableaux è semplicissimo, perché esse fanno direttamente riferimento alle tavole di verità dei connettivi. Si prenda, ad esempio, la congiunzione: essa è vera se e solo se entrambi gli operandi sono veri; perciò, nella $T$ -regola dell'and, entrambi gli operandi vengono segnati veri in maniera congiunta; mentre, dato che essa è falsa se e solo se almeno uno degli operandi è falso, nella $F$ -regola entrambi gli operandi vengono segnati falsi in maniera disgiunta. Le regole per gli altri connettivi vengono dedotte nel medesimo modo.

Per una dimostrazione formale, si veda il lemma di conservazione dell'equivalenza.

Definizioni

Template:Definizione

Tabella riassuntiva

La seguente tabella riassume l'utilizzo dei tableaux come metodo di dimostrazione.


Per provare che $A$ è	Fare tableau per	Chiuso	Aperto
Teorema	$F A$	Sì	No
Soddisfacibile	$T A$	No	Sì
Contraddizione	$T A$	Sì	No

Metateoremi

Il sistema dei tableaux è corretto e completo. Prima di enunciare la correttezza e completezza, mostriamo la semantica che servirà a darne la dimostrazione.

Semantica dei simboli di valutazione

Template:Definizione

Soddisfacibilità

Template:Definizione

Lemma di chiusura

Se un insieme di formule segnate $Γ$ è chiuso, allora è insoddisfacibile.

Dimostrazione

Supponiamo per assurdo che $Γ$ sia chiuso ma soddisfacibile. Allora $ℳ_{𝒱} ⊨ Γ$ , per qualche modello $ℳ_{𝒱}$ . Siccome $Γ$ è chiuso, abbiamo che $T A, F A \in Γ$ per qualche formula $A$ , oppure $T ⊥ \in Γ$ , oppure $F ⊤ \in Γ$ . Se $T A, F A \in Γ$ , allora $ℳ_{𝒱} ⊨ A$ e $ℳ_{𝒱} ⊭ A$ , contraddizione; se $T ⊥ \in Γ$ , allora $ℳ_{𝒱} ⊨ ⊥$ , contraddizione con la definizione di modello; se $F ⊤ \in Γ$ , allora $ℳ_{𝒱} ⊭ ⊤$ , contraddizione con la definizione di modello.

Lemma di conservazione dell'equivalenza

Sia $𝒯_{1}$ un tableau e $𝒯_{2}$ il tableau ottenuto da $𝒯_{1}$ tramite un passo di espansione. Allora, per ogni modello $ℳ_{𝒱}$ , $ℳ_{𝒱} ⊨ 𝒯_{1}$ sse $ℳ_{𝒱} ⊨ 𝒯_{2}$ .

Dimostrazione

Il lemma si dimostra per induzione strutturale sulle regole di espansione. Consideriamo solo il caso della $T$ -regola della disgiunzione. Sia $β$ una formula; se $𝒯_{1}$ è il tableau iniziale per $T β$ , $ℳ_{𝒱} ⊨ T β$ sse $ℳ_{𝒱} ⊨ β$ sse ( $ℳ_{𝒱} ⊨ β_{1}$ oppure $ℳ_{𝒱} ⊨ β_{2}$ ), per qualche modello $ℳ_{𝒱}$ . Se $𝒯_{2}$ è il tableau ottenuto espandendo $𝒯_{1}$ tramite l'applicazione della $T$ -regola della disgiunzione, $𝒯_{2}$ è $T β_{1} | T β_{2}$ , e $ℳ_{𝒱} ⊨ (T β_{1} | T β_{2})$ sse ( $ℳ_{𝒱} ⊨ T β_{1}$ oppure $ℳ_{𝒱} ⊨ T β_{2}$ ) sse ( $ℳ_{𝒱} ⊨ β_{1}$ oppure $ℳ_{𝒱} ⊨ β_{2}$ ); dunque $ℳ_{𝒱} ⊨ T β$ sse ( $ℳ_{𝒱} ⊨ T β_{1}$ oppure $ℳ_{𝒱} ⊨ T β_{2}$ ). Di conseguenza, $ℳ_{𝒱}$ soddisfa almeno un ramo di $𝒯_{2}$ , e quindi $ℳ_{𝒱} ⊨ 𝒯_{1}$ sse $ℳ_{𝒱} ⊨ 𝒯_{2}$ .

Teorema dei modelli

Dato un insieme $Γ$ di formule segnate, esso è soddisfacibile sse ogni suo tableau completo è aperto. Inoltre, se un tableau $𝒯$ per $Γ$ è completo, allora ad ogni suo nodo foglia aperto corrisponde almeno un modello per $Γ$ , cioè, se $Δ = {T A_{0}, . . ., T A_{n}, F B_{0}, . . ., F B_{m}}$ è una foglia aperta di $𝒯$ , allora l'insieme di simboli proposizionali $ℳ_{𝒱} = {A_{0}, . . ., A_{n}}$ , costituito dai simboli proposizionali di $Δ$ segnati veri, e ogni suo sovrainsieme $ℳ_{𝒱} \cup {C_{0}, . . ., C_{k}}$ , dove $C_{0}, . . ., C_{k}$ sono simboli proposizionali che non compaiono in $Δ$ , è un modello per $Γ$ , ovvero $ℳ_{𝒱} ⊨ Γ$ e $ℳ_{𝒱} \cup {C_{0}, . . ., C_{k}} ⊨ Γ$ .

Dimostrazione

Per la conservazione dell'equivalenza, per ogni modello $ℳ_{𝒱}$ esiste un nodo $Δ$ foglia di $𝒯$ tale che $ℳ_{𝒱} ⊨ Γ$ sse $ℳ_{𝒱} ⊨ Δ$ . $ℳ_{𝒱} ⊨ Δ$ sse $ℳ_{𝒱} ⊨ A_{0}, . . ., A_{n}$ e $ℳ_{𝒱} ⊭ B_{0}, . . ., B_{m}$ . Dato che $𝒯$ è completo, ogni nodo foglia $Δ$ aperto è costituito da soli simboli proposizionali segnati, dunque è possibile costruire i modelli che lo soddisfano a partire dalle sue formule segnate, e si può vedere facilmente che questi modelli sono esattamente $ℳ_{𝒱} = {A_{0}, . . ., A_{n}}$ (dato che, per ogni atomo $A$ , $ℳ_{𝒱} ⊨ A$ sse $A \in ℳ_{𝒱}$ ) e ogni suo sovrainsieme $ℳ_{𝒱} \cup {C_{0}, . . ., C_{k}}$ , dove $C_{0}, . . ., C_{k}$ sono simboli proposizionali che non compaiono segnati in $Δ$ (altrimenti potremmo avere che $ℳ_{𝒱} ⊨ B_{i}$ , per qualche $i = 0, . . ., m$ ). Dunque, $Γ$ è soddisfacibile sse ogni suo tableau completo ha almeno un modello, cioè se è aperto.

A questo punto possiamo illustrare il teorema di correttezza e completezza debole, che riguarda solo le tautologie.

Teorema di correttezza e completezza debole

$A$ è una tautologia sse $A$ ha una tableau-dimostrazione, cioè

$⊨ A$ sse $⊢_{T} A$ .

Dimostrazione

Per la correttezza, dobbiamo mostrare che se $A$ ha una tableau-dimostrazione, allora $A$ è una tautologia. Ma, per definizione, una tableau-dimostrazione per $A$ è un tableau $𝒯$ completo e chiuso per ${F A}$ , quindi, per il teorema dei modelli, ${F A}$ è insoddisfacibile, dunque non esiste alcun modello $ℳ_{𝒱}$ tale che $ℳ_{𝒱} ⊭ A$ , perciò $A$ è una tautologia.
Per la completezza, dobbiamo mostrare che se $A$ è una tautologia, allora ha una tableau-dimostrazione. Ma se $A$ è una tautologia, allora non esiste alcun modello $ℳ_{𝒱}$ tale che $ℳ_{𝒱} ⊭ A$ , perciò ${F A}$ è insoddisfacibile, quindi, per il teorema dei modelli, esiste un tableau chiuso per ${F A}$ , e sapendo che un tableau chiuso per ${F A}$ coincide con una tableau-dimostrazione per $A$ , allora $A$ ha una tableau-dimostrazione, quindi $A$ è un teorema del sistema di calcolo dei tableaux.

Lemma della verità

Per ogni insieme di formule $Δ = {A_{0}, A_{1}, . . .}$ , poniamo $T (Δ) = {T A_{0}, T A_{1}, . . .}$ . Allora si ha che, per ogni modello $ℳ_{𝒱}$ , $ℳ_{𝒱} ⊨ Δ$ sse $ℳ_{𝒱} ⊨ T (Δ)$ .

Dimostrazione

Per definizione, per ogni modello $ℳ_{𝒱}$ , $ℳ_{𝒱} ⊨ Δ$ sse $ℳ_{𝒱} ⊨ A_{0}, A_{1}, . . .$ e $ℳ_{𝒱} ⊨ T (Δ)$ sse $ℳ_{𝒱} ⊨ A_{0}, ℳ_{𝒱} ⊨ A_{1}, . . .$ , dunque $ℳ_{𝒱} ⊨ Δ$ sse $ℳ_{𝒱} ⊨ T (Δ)$ .

Lemma della dimostrabilità

Sia $Γ_{0}$ un insieme finito di formule. Allora, $Γ_{0} ⊢_{T} A$ sse $Γ_{0} \cup {\neg A}$ è insoddisfacibile.

Dimostrazione

Per definizione, $Γ_{0} ⊢_{T} A$ sse esiste una tableau-deduzione $𝒯$ di $A$ da $Γ_{0}$ . $𝒯$ è un tableau chiuso. Per il teorema dei modelli, abbiamo che $𝒯$ è chiuso sse $T (Γ_{0} \cup {\neg A})$ è insoddisfacibile, dunque, per il lemma della verità, $T (Γ_{0} \cup {\neg A})$ è insoddisfacibile sse $Γ_{0} \cup {\neg A}$ è insoddisfacibile.

Teorema di compattezza della dimostrabilità

Per dimostrare la correttezza e completezza forte, ci serviremo del teorema di compattezza, cioè:

dati un insieme di formule $Γ$ e una formula $A$ , $Γ ⊢_{T} A$ sse esiste un insieme finito di formule $Γ_{0} \subseteq Γ$ tale che $Γ_{0} ⊢_{T} A$ .

Dimostrazione

Dato che $Γ_{0} \subseteq Γ$ , allora $Γ_{0} \cup {\neg A} \subseteq Γ \cup {\neg A}$ . Dal teorema di compattezza della soddisfacibilità, sapendo che $Γ_{0} \cup {\neg A} \subseteq Γ \cup {\neg A}$ , si deduce che $Γ_{0} \cup {\neg A}$ è insoddisfacibile sse $Γ \cup {\neg A}$ è insoddisfacibile e, per il lemma della verità, $Γ \cup {\neg A}$ è insoddisfacibile sse $T (Γ \cup {\neg A})$ è insoddisfacibile; quindi, per il teorema dei modelli, abbiamo che $T (Γ \cup {\neg A})$ è insoddisfacibile sse $T (Γ \cup {\neg A})$ ha un tableau chiuso sse $Γ ⊢_{T} A$ , quindi $Γ_{0} ⊢_{T} A$ sse $Γ ⊢_{T} A$ .

Teorema di correttezza e completezza forte

$Γ ⊨ A$ sse $Γ ⊢_{T} A$ .

Dimostrazione

Per il teorema di compattezza, $Γ ⊢_{T} A$ sse esiste un insieme finito di formule $Γ_{0} \subseteq Γ$ tale che $Γ_{0} ⊢_{T} A$ . Per il lemma della dimostrabilità, $Γ_{0} ⊢_{T} A$ sse $Γ_{0} \cup {\neg A}$ è insoddisfacibile. Dal teorema di soddisfacibilità, $Γ_{0} \cup {\neg A}$ è insoddisfacibile sse $Γ_{0} ⊨ A$ e, dal corollario del teorema di compattezza della soddisfacibilità, abbiamo che $Γ_{0} ⊨ A$ sse $Γ ⊨ A$ .

Complessità computazionale

È semplice dimostrare come il tempo impiegato per costruire un tableau per una formula $A$ sia esponenziale sulla lunghezza di $A$ . Infatti, supponendo che $n$ sia la lunghezza di $A$ , l'altezza dell'albero sarà minore o uguale $n$ , e siccome ad ogni livello il numero dei nodi può al massimo raddoppiare rispetto al livello precedente, ciò significa che l'ultimo livello avrà al più $2^{n}$ nodi.

Esempi di dimostrazioni

Non contraddizione

${\underline{F \neg (A \land \neg A)}}_{F \neg}$

${\underline{T A \land \neg A}}_{T \land}$

${\underline{T A, T \neg A}}_{T \neg}$

$\overline{T A}, \overline{F A}$

Terzo escluso

${\underline{F A \lor \neg A}}_{F \lor}$

${\underline{F A, F \neg A}}_{F \neg}$

$\overline{F A}, \overline{T A}$

Doppia negazione

${\underline{F A \leftrightarrow \neg \neg A}}_{F \leftrightarrow}$

${\underline{T A, F \neg \neg A}}_{F \neg} | {\underline{F A, T \neg \neg A}}_{T \neg}$

${\underline{T A, T \neg A}}_{T \neg} | {\underline{F A, F \neg A}}_{F \neg}$

$\overline{T A}, \overline{F A} | \overline{F A}, \overline{T A}$

Modus ponens

${\underline{F (A \to B) \land A \to B}}_{F \to}$

${\underline{T (A \to B) \land A, F B}}_{T \land}$

${\underline{T A \to B, T A, F B}}_{T \to}$

$\overline{F A}, \overline{T A}, F B | \overline{T B}, T A, \overline{F B}$

Contrapposizione

${\underline{F (A \to B) \leftrightarrow (\neg B \to \neg A)}}_{F \leftrightarrow}$

${\underline{T A \to B, F \neg B \to \neg A}}_{F \to} | {\underline{F A \to B, T \neg B \to \neg A}}_{F \to}$

${\underline{T A \to B, T \neg B, F \neg A}}_{T \to} | {\underline{T A, F B, T \neg B \to \neg A}}_{T \to}$

${\underline{F A, T \neg B, F \neg A}}_{F \neg} | {\underline{T B, T \neg B, F \neg A}}_{T \neg} | {\underline{T A, F B, F \neg B}}_{F \neg} | {\underline{T A, F B, T \neg A}}_{T \neg}$

$\overline{F A}, T \neg B, \overline{T A} | \overline{T B}, \overline{F B}, F \neg A | T A, \overline{F B}, \overline{T B} | \overline{T A}, F B, \overline{F A}$

Teorema di De Morgan

${\underline{F \neg (A \land B) \leftrightarrow (\neg A \lor \neg B)}}_{F \leftrightarrow}$

${\underline{T \neg (A \land B), F \neg A \lor \neg B}}_{T \neg} | {\underline{F \neg (A \land B), T \neg A \lor \neg B}}_{F \neg}$

${\underline{F A \land B, F \neg A \lor \neg B}}_{F \lor} | {\underline{T A \land B, T \neg A \lor \neg B}}_{T \land}$

${\underline{F A \land B, F \neg A, F \neg B}}_{F \neg} | {\underline{T A, T B, T \neg A \lor \neg B}}_{T \lor}$

${\underline{F A \land B, T A, T B}}_{F \land} | {\underline{T A, T B, T \neg A}}_{T \neg} | {\underline{T A, T B, T \neg B}}_{T \neg}$

$\overline{F A}, \overline{T A}, T B | \overline{F B}, T A, \overline{T B} | \overline{T A}, T B, \overline{F A} | T A, \overline{T B}, \overline{F B}$

Proprietà distributiva

${\underline{F A \lor (B \land C) \leftrightarrow (A \lor B) \land (A \lor C)}}_{F \leftrightarrow}$

${\underline{T A \lor (B \land C), F (A \lor B) \land (A \lor C)}}_{T \lor} | {\underline{F A \lor (B \land C), T (A \lor B) \land (A \lor C)}}_{F \lor}$

${\underline{T A, F (A \lor B) \land (A \lor C)}}_{F \land} | {\underline{T B \land C, F (A \lor B) \land (A \lor C)}}_{T \land} | {\underline{F A, F B \land C, T (A \lor B) \land (A \lor C)}}_{T \land}$

${\underline{T A, F A \lor B}}_{F \lor} | {\underline{T A, F A \lor C}}_{F \lor} | {\underline{T B, T C, F (A \lor B) \land (A \lor C)}}_{F \land} | {\underline{F A, F B \land C, T A \lor B, T A \lor C}}_{T \lor}$

$\overline{T A}, \overline{F A}, F B | \overline{T A}, \overline{F A}, F C | T B, T C, F A \lor B | T B, T C, F A \lor C | \overline{F A}, F B \land C, \overline{T A}, T A \lor C | F A, F B \land C, T B, T A \lor C$

${\underline{T B, T C, F A \lor B}}_{F \lor} | {\underline{T B, T C, F A \lor C}}_{F \lor} | {\underline{F A, F B \land C, T B, T A \lor C}}_{T \lor}$

$\overline{T B}, T C, F A, \overline{F B} | T B, \overline{T C}, F A, \overline{F C} | \overline{F A}, F B \land C, T B, \overline{T A} | F A, F B \land C, T B, T C$

${\underline{F A, F B \land C, T B, T C}}_{F \land}$

$F A, \overline{F B}, \overline{T B}, T C | F A, \overline{F C}, T B, \overline{T C}$

Collegamenti esterni

Template:En Una pagina interattiva sui tableaux.

Template:Avanzamento

Logica matematica/Calcolo delle proposizioni/I tableaux semantici

Indice

Sintassi e regole di inferenza

Formule segnate

Formule congiuntive e disgiuntive

Regole di espansione

Validità delle regole

Definizioni

Tabella riassuntiva

Metateoremi

Semantica dei simboli di valutazione

Soddisfacibilità

Lemma di chiusura

Dimostrazione

Lemma di conservazione dell'equivalenza

Dimostrazione

Teorema dei modelli

Dimostrazione

Teorema di correttezza e completezza debole

Dimostrazione

Lemma della verità

Dimostrazione

Lemma della dimostrabilità

Dimostrazione

Teorema di compattezza della dimostrabilità

Dimostrazione

Teorema di correttezza e completezza forte

Dimostrazione

Complessità computazionale

Esempi di dimostrazioni

Non contraddizione

Terzo escluso

Doppia negazione

Modus ponens

Contrapposizione

Teorema di De Morgan

Proprietà distributiva

Collegamenti esterni

Menu di navigazione

Logica matematica/Calcolo delle proposizioni/I tableaux semantici

Sintassi e regole di inferenza

Formule segnate

Formule congiuntive e disgiuntive

Regole di espansione

Validità delle regole

Definizioni

Tabella riassuntiva

Metateoremi

Semantica dei simboli di valutazione

Soddisfacibilità

Lemma di chiusura

Dimostrazione

Lemma di conservazione dell'equivalenza

Dimostrazione

Teorema dei modelli

Dimostrazione

Teorema di correttezza e completezza debole

Dimostrazione

Lemma della verità

Dimostrazione

Lemma della dimostrabilità

Dimostrazione

Teorema di compattezza della dimostrabilità

Dimostrazione

Teorema di correttezza e completezza forte

Dimostrazione

Complessità computazionale

Esempi di dimostrazioni

Non contraddizione

Terzo escluso

Doppia negazione

Modus ponens

Contrapposizione

Teorema di De Morgan

Proprietà distributiva

Collegamenti esterni

Menu di navigazione

Ricerca