Logica matematica/Calcolo delle proposizioni/Dimostrazione del teorema di compattezza

Wikibooks, manuali e libri di testo liberi.
Jump to navigation Jump to search
Indice del libro

Il teorema di compattezza della soddisfacibilità asserisce che un insieme di proposizioni è soddisfacibile sse è finitamente soddisfacibile. Quella che diamo qui è una dimostrazione costruttiva, cioè, il teorema viene dimostrato costruendo un modello che soddisfa un insieme infinito.

Definizioni[modifica]

Insieme di formule finitamente soddisfacibile[modifica]

Viewmag.png Definizione

Un insieme di formule si dice finitamente soddisfacibile sse ogni suo sottoinsieme finito è soddisfacibile.

Insieme di formule massimale[modifica]

Viewmag.png Definizione

Un insieme di formule si dice massimale sse per ogni di si ha oppure .

Lemma 1[modifica]

Se è un insieme di formule soddisfacibile, allora ogni sottoinsieme è soddisfacibile.

Dimostrazione[modifica]

Supponiamo che sia soddisfacibile, ma che esista un sottoinsieme insoddisfacibile. Allora, per definizione, per ogni modello esiste una formula tale che . Essendo , allora . Quindi, per ogni modello esiste una formula tale che . Dunque, è insoddisfacibile. Contraddizione.

Lemma 2[modifica]

Se è un insieme di formule finitamente soddisfacibile, allora, per ogni formula , oppure è finitamente soddisfacibile.

Dimostrazione[modifica]

Consideriamo una formula . Se , la tesi è ovvia. Sia quindi . Si danno due casi.

  • è soddisfacibile. Per il lemma 1, ogni sottoinsieme di è soddisfacibile, quindi ogni sottoinsieme finito è soddisfacibile. Dunque, è finitamente soddisfacibile.
  • non è soddisfacibile. Comunque si prenda un modello , avremo , quindi , cioè . Quindi è soddisfacibile. Dunque, per il medesimo argomento del caso precedente, è finitamente soddisfacibile.

Lemma 3[modifica]

Se è un insieme di formule massimale finitamente soddisfacibile, allora, per ogni formula , sse .

Dimostrazione[modifica]

() Per definizione, se , allora, per ogni formula , . Se , allora , e dunque, dato che implica , per definizione . Si noti che, per la parte "solo-se" del teorema, non c'è bisogno di supporre che sia massimale e finitamente soddisfacibile.

() Supponiamo per assurdo che , ma . Per il teorema di soddisfacibilità, è insoddisfacibile, e quindi, siccome è finitamente soddisfacibile, per il lemma 2 è finitamente soddisfacibile. Ma siccome , allora , dato che è massimale, e quindi , dunque , e siccome è insoddisfacibile, non è finitamente soddisfacibile, contraddicendo ciò che avevamo precedentemente dedotto.

Dimostrazione[modifica]

() Se è soddisfacibile, allora è finitamente soddisfacibile. Supponiamo che sia soddisfacibile, allora, per il lemma 1, ogni sottoinsieme è soddisfacibile, quindi, ogni sottoinsieme finito di è soddisfacibile. Dunque, è finitamente soddisfacibile.

() Se è finitamente soddisfacibile, allora è soddisfacibile. Osserviamo innanzitutto che, se è finito, la tesi è banalmente dimostrata. Ci occupiamo quindi di infiniti.

La dimostrazione consiste di due parti. Nella prima dimostriamo che un insieme finitamente soddisfacibile si può estendere ad un insieme massimale finitamente soddisfacibile. Nella seconda parte costruiremo un modello per . Siccome abbiamo costruito estendendo , tale modello sarà anche un modello per , quindi la tesi sarà dimostrata.

Cominciamo con l'enumerare tutte le formule del linguaggio: . Definiamo per induzione:

Sia . Osserviamo innanzitutto che , per costruzione. Osserviamo inoltre che è massimale, cioè, per ogni formula , o la sua negazione appartengono a . Infatti, siccome l'enumerazione delle formule è completa, per costruzione dei , presa una qualunque , esisterà un per cui , quindi oppure . Osserviamo anche che ciascun è finitamente soddisfacibile (per induzione: è finitamente soddisfacibile; il passo induttivo è giustificato dal lemma 2). Quindi, è finitamente soddisfacibile, in quanto ogni sottoinsieme finito di è contenuto in qualche . Dobbiamo ora mostrare che è soddisfacibile. Per far questo, costruiamo un modello per esso. Definiamo il modello come:

dove è l'insieme dei simboli proposizionali del linguaggio. Dimostriamo ora, per induzione strutturale sulle formule, che per ogni formula :

sse .

(Passo base) Per costruzione di .

(Passo induttivo) Sia . equivale a ; per ipotesi induttiva, sse . Siccome è massimale, sse . Pertanto, sse , che è la tesi.

Sia . Per definizione, sse e ; per ipotesi induttiva, sse e sse . Siccome è massimale, per il lemma 3 sse ( e ). ( e ) sse, per definizione di congiunzione, e, per il lemma 3, sse , che è la tesi.

Sia . Per definizione, sse o ; per ipotesi induttiva, sse e sse . Siccome è massimale, per il lemma 3 ( o ) sse ( o ). ( o ) sse, per definizione di disgiunzione, e, per il lemma 3, sse , che è la tesi.

Sia . Per definizione, sse o ; per ipotesi induttiva, sse e sse . Siccome è massimale, per il lemma 3 ( o ) sse ( o ). ( o ) sse, per definizione di implicazione, e, per il lemma 3, sse , che è la tesi.

Sia . Per definizione, sse ( sse ); per ipotesi induttiva, sse e sse . Siccome è massimale, per il lemma 3 ( sse ) sse ( sse ). ( sse ) sse, per definizione di doppia implicazione, e, per il lemma 3, sse , che è la tesi.

Abbiamo quindi mostrato che è un modello per ; siccome , abbiamo che , ovvero è soddisfacibile.