Logica matematica/Calcolo delle proposizioni/I tableaux semantici

Indice del libro


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

modifica

Formule segnate

modifica

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   e  : essi fungono da operatori, assegnando alle formule un valore booleano, rispettivamente vero e falso. Quest'operazione è detta valutazione booleana.

Diamo ora una definizione formale:   Definizione

  •   e   sono detti simboli di valutazione;
  • se   è una formula proposizionale, allora   e   sono formule segnate.

Formule congiuntive e disgiuntive

modifica

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   e  , con  : quelle che agiscono congiuntivamente e quelle che agiscono disgiuntivamente.

Regole di espansione

modifica

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  -regola e  -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.

  Definizione

Negazione

 

 

Congiunzione

 

 

Disgiunzione

 

 

Implicazione

 

 

Doppia implicazione

 

 

Validità delle regole

modifica

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  -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  -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

modifica

  Definizione

Supponiamo che   sia un insieme finito di formule segnate.

Tableau

Un tableau è un albero binario in cui ogni nodo è etichettato da un insieme di formule segnate.

Dato  , l'albero binario costituito dal solo nodo radice etichettato da   stesso è detto tableau iniziale per   e denotato  .

Passo di espansione

Dato  , se   è un tableau per  , e   è un nodo foglia di  , possiamo costruire un tableau   per   attraverso un passo di espansione.

  si ottiene applicando le regole di espansione dei tableaux ad una delle formule segnate del nodo foglia  , in particolare:

  1. nel caso la regola sia congiuntiva, si aggiunge come figlio di   un nodo contenente l'espansione che si ottiene applicando la suddetta regola;
  2. nel caso la regola sia disgiuntiva, si aggiungono come figli di   due nodi contenenti le rispettive espansioni disgiunte.

Il tableau   si dice ottenuto da   con un passo di espansione.

Tableau ben costruito

Dati due tableaux   e   per  ,   è un'espansione coerente di   sse   è stato ottenuto da   attraverso un numero finito di passi di espansione.

Un tableau   per   si dice ben costruito sse è stato ottenuto per espansioni coerenti dal tableau radice e nessun nodo è stato oggetto di più di un'espansione coerente.

Tableau completo

Un tableau   per   è completo sse è ben costruito e non può più essere oggetto di espansioni coerenti.

Il nodo di un tableau può essere visto come la congiunzione delle formule che appaiono in esso (negando le formule segnate con  ) e l'intero tableau come una disgiunzione di congiunzioni.

Chiusura

Un ramo di un tableau si dice chiuso sse, per qualche formula  , sia   che   occorrono nella congiunzione che etichetta il nodo del ramo, oppure se in essa occorre   o  . Altrimenti, il ramo è detto aperto. La coppia   e   si chiama coppia complementare.

Un tableau è chiuso sse tutti i suoi rami sono chiusi, altrimenti è aperto.

Tableau-refutazione

Una tableau-refutazione di una formula   è un tableau chiuso, la cui radice è etichettata da  .

Una tableau-refutazione di una formula   da  , insieme finito di formule, è un tableau chiuso, la cui radice è etichettata da  .

Tableau-dimostrazione

Una tableau-dimostrazione di una formula   è un tableau chiuso, la cui radice è etichettata da  .   è un teorema del sistema di calcolo dei tableaux sse   ha una tableau-dimostrazione. In questo caso scriviamo

 

Tableau-deduzione

Una tableau-deduzione di una formula   da  , insieme finito di formule, è un tableau chiuso, la cui radice è etichettata da  . In questo caso scriviamo

 

Tabella riassuntiva

modifica

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

Per provare che   è Fare tableau per Chiuso Aperto
Teorema   No
Soddisfacibile   No
Contraddizione   No

Metateoremi

modifica

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

modifica

  Definizione

Dato un modello   e un insieme di formule segnate  , diciamo che   soddisfa  , e scriviamo  , sse:

  • per ogni formula  , con  ,  ;
  • per ogni formula  , con  ,  .

Soddisfacibilità

modifica

  Definizione

Un insieme di formule segnate   è soddisfacibile sse esiste un modello   tale che  . Un tableau è soddisfacibile sse almeno uno dei suoi nodi è soddisfacibile.

Lemma di chiusura

modifica

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

Dimostrazione

modifica

Supponiamo per assurdo che   sia chiuso ma soddisfacibile. Allora  , per qualche modello  . Siccome   è chiuso, abbiamo che   per qualche formula  , oppure  , oppure  . Se  , allora   e  , contraddizione; se  , allora  , contraddizione con la definizione di modello; se  , allora  , contraddizione con la definizione di modello.

Lemma di conservazione dell'equivalenza

modifica

Sia   un tableau e   il tableau ottenuto da   tramite un passo di espansione. Allora, per ogni modello  ,   sse  .

Dimostrazione

modifica

Il lemma si dimostra per induzione strutturale sulle regole di espansione. Consideriamo solo il caso della  -regola della disgiunzione. Sia   una formula; se  è il tableau iniziale per  ,   sse   sse (  oppure  ), per qualche modello  . Se   è il tableau ottenuto espandendo   tramite l'applicazione della  -regola della disgiunzione,   è  , e   sse (  oppure  ) sse (  oppure  ); dunque   sse (  oppure  ). Di conseguenza,   soddisfa almeno un ramo di  , e quindi   sse  .

Teorema dei modelli

modifica

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   è una foglia aperta di  , allora l'insieme di simboli proposizionali  , costituito dai simboli proposizionali di   segnati veri, e ogni suo sovrainsieme  , dove   sono simboli proposizionali che non compaiono in  , è un modello per  , ovvero   e  .

Dimostrazione

modifica

Per la conservazione dell'equivalenza, per ogni modello   esiste un nodo   foglia di   tale che   sse  .   sse   e  . 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   (dato che, per ogni atomo  ,   sse  ) e ogni suo sovrainsieme  , dove   sono simboli proposizionali che non compaiono segnati in   (altrimenti potremmo avere che  , per qualche  ). 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

modifica

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

  sse  .

Dimostrazione

modifica
  • Per la correttezza, dobbiamo mostrare che se   ha una tableau-dimostrazione, allora   è una tautologia. Ma, per definizione, una tableau-dimostrazione per   è un tableau   completo e chiuso per  , quindi, per il teorema dei modelli,   è insoddisfacibile, dunque non esiste alcun modello   tale che  , perciò   è una tautologia.
  • Per la completezza, dobbiamo mostrare che se   è una tautologia, allora ha una tableau-dimostrazione. Ma se   è una tautologia, allora non esiste alcun modello   tale che  , perciò   è insoddisfacibile, quindi, per il teorema dei modelli, esiste un tableau chiuso per  , e sapendo che un tableau chiuso per   coincide con una tableau-dimostrazione per  , allora   ha una tableau-dimostrazione, quindi   è un teorema del sistema di calcolo dei tableaux.

Lemma della verità

modifica

Per ogni insieme di formule  , poniamo  . Allora si ha che, per ogni modello  ,   sse  .

Dimostrazione

modifica

Per definizione, per ogni modello  ,   sse   e   sse  , dunque   sse  .

Lemma della dimostrabilità

modifica

Sia   un insieme finito di formule. Allora,   sse   è insoddisfacibile.

Dimostrazione

modifica

Per definizione,   sse esiste una tableau-deduzione   di   da  .   è un tableau chiuso. Per il teorema dei modelli, abbiamo che   è chiuso sse   è insoddisfacibile, dunque, per il lemma della verità,   è insoddisfacibile sse   è insoddisfacibile.

Teorema di compattezza della dimostrabilità

modifica

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

dati un insieme di formule   e una formula  ,   sse esiste un insieme finito di formule   tale che  .

Dimostrazione

modifica

Dato che  , allora  . Dal teorema di compattezza della soddisfacibilità, sapendo che  , si deduce che   è insoddisfacibile sse   è insoddisfacibile e, per il lemma della verità,   è insoddisfacibile sse   è insoddisfacibile; quindi, per il teorema dei modelli, abbiamo che   è insoddisfacibile sse   ha un tableau chiuso sse  , quindi   sse  .

Teorema di correttezza e completezza forte

modifica

  sse  .

Dimostrazione

modifica

Per il teorema di compattezza,   sse esiste un insieme finito di formule   tale che  . Per il lemma della dimostrabilità,   sse   è insoddisfacibile. Dal teorema di soddisfacibilità,   è insoddisfacibile sse   e, dal corollario del teorema di compattezza della soddisfacibilità, abbiamo che   sse  .

Complessità computazionale

modifica

È semplice dimostrare come il tempo impiegato per costruire un tableau per una formula   sia esponenziale sulla lunghezza di  . Infatti, supponendo che   sia la lunghezza di  , l'altezza dell'albero sarà minore o uguale  , 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ù   nodi.

Esempi di dimostrazioni

modifica

Non contraddizione

modifica

 

 

 

 

Terzo escluso

modifica

 

 

 

Doppia negazione

modifica

 

 

 

 

Modus ponens

modifica

 

 

 

 

Contrapposizione

modifica

 

 

 

 

 

Teorema di De Morgan

modifica

 

 

 

 

 

 

Proprietà distributiva

modifica

 

 

 

 

 

 

 

 

 

Collegamenti esterni

modifica