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

Template:Logica matematica Il teorema di compattezza della soddisfacibilità asserisce che un insieme di proposizioni $\mathrm{\Gamma }$ è soddisfacibile sse è finitamente soddisfacibile. Quella che diamo qui è una dimostrazione costruttiva, cioè, il teorema viene dimostrato costruendo un modello che soddisfa un insieme $\mathrm{\Gamma }$ infinito.

Lemma 1

Se $\mathrm{\Gamma }$ è un insieme di formule soddisfacibile, allora ogni sottoinsieme $\mathrm{\Delta }\subseteq \mathrm{\Gamma }$ è soddisfacibile.

Dimostrazione

Supponiamo che $\mathrm{\Gamma }$ sia soddisfacibile, ma che esista un sottoinsieme $\mathrm{\Delta }\subseteq \mathrm{\Gamma }$ insoddisfacibile. Allora, per definizione, per ogni modello ${ℳ}_{𝒱}$ esiste una formula $A\in \mathrm{\Delta }$ tale che ${ℳ}_{𝒱}⊭A$. Essendo $\mathrm{\Delta }\subseteq \mathrm{\Gamma }$, allora $A\in \mathrm{\Gamma }$. Quindi, per ogni modello ${ℳ}_{𝒱}$ esiste una formula $A\in \mathrm{\Gamma }$ tale che ${ℳ}_{𝒱}⊭A$. Dunque, $\mathrm{\Gamma }$ è insoddisfacibile. Contraddizione.

Lemma 2

Se $\mathrm{\Gamma }$ è un insieme di formule finitamente soddisfacibile, allora, per ogni formula $A$, $\mathrm{\Gamma }\cup \{A\}$ oppure $\mathrm{\Gamma }\cup \{\mathrm{\neg }A\}$ è finitamente soddisfacibile.

Dimostrazione

Consideriamo una formula $A$. Se $A\in \mathrm{\Gamma }$, la tesi è ovvia. Sia quindi $A\in ̸\mathrm{\Gamma }$. Si danno due casi.

• $\mathrm{\Gamma }\cup \{A\}$ è soddisfacibile. Per il lemma 1, ogni sottoinsieme di $\mathrm{\Gamma }\cup \{A\}$ è soddisfacibile, quindi ogni sottoinsieme finito $\mathrm{\Delta }\subseteq \mathrm{\Gamma }\cup \{A\}$ è soddisfacibile. Dunque, $\mathrm{\Gamma }\cup \{A\}$ è finitamente soddisfacibile.
• $\mathrm{\Gamma }\cup \{A\}$ non è soddisfacibile. Comunque si prenda un modello ${ℳ}_{𝒱}\models \mathrm{\Gamma }$, avremo ${ℳ}_{𝒱}⊭A$, quindi ${ℳ}_{𝒱}\models \mathrm{\neg }A$, cioè ${ℳ}_{𝒱}\models \mathrm{\Gamma }\cup \{\mathrm{\neg }A\}$. Quindi $\mathrm{\Gamma }\cup \{\mathrm{\neg }A\}$ è soddisfacibile. Dunque, per il medesimo argomento del caso precedente, $\mathrm{\Gamma }\cup \{\mathrm{\neg }A\}$ è finitamente soddisfacibile.

Lemma 3

Se $\mathrm{\Gamma }$ è un insieme di formule massimale finitamente soddisfacibile, allora, per ogni formula $A$, $A\in \mathrm{\Gamma }$ sse $\mathrm{\Gamma }\models A$.

Dimostrazione

($\Rightarrow$) Per definizione, se ${ℳ}_{𝒱}\models \mathrm{\Gamma }$, allora, per ogni formula $B\in \mathrm{\Gamma }$, ${ℳ}_{𝒱}\models B$. Se $A\in \mathrm{\Gamma }$, allora ${ℳ}_{𝒱}\models A$, e dunque, dato che ${ℳ}_{𝒱}\models \mathrm{\Gamma }$ implica ${ℳ}_{𝒱}\models A$, per definizione $\mathrm{\Gamma }\models A$. Si noti che, per la parte "solo-se" del teorema, non c'è bisogno di supporre che $\mathrm{\Gamma }$ sia massimale e finitamente soddisfacibile.

($\Leftarrow$) Supponiamo per assurdo che $\mathrm{\Gamma }\models A$, ma $A\in ̸\mathrm{\Gamma }$. Per il teorema di soddisfacibilità, $\mathrm{\Gamma }\cup \{\mathrm{\neg }A\}$ è insoddisfacibile, e quindi, siccome $\mathrm{\Gamma }$ è finitamente soddisfacibile, per il lemma 2 $\mathrm{\Gamma }\cup \{A\}$ è finitamente soddisfacibile. Ma siccome $A\in ̸\mathrm{\Gamma }$, allora $\mathrm{\neg }A\in \mathrm{\Gamma }$, dato che $\mathrm{\Gamma }$ è massimale, e quindi $\mathrm{\neg }A\in \mathrm{\Gamma }\cup \{A\}$, dunque $\{\mathrm{\neg }A,A\}\subseteq \mathrm{\Gamma }\cup \{A\}$, e siccome $\{\mathrm{\neg }A,A\}$ è insoddisfacibile, $\mathrm{\Gamma }\cup \{A\}$ non è finitamente soddisfacibile, contraddicendo ciò che avevamo precedentemente dedotto.

Dimostrazione

($\Rightarrow$) Se $\mathrm{\Gamma }$ è soddisfacibile, allora è finitamente soddisfacibile. Supponiamo che $\mathrm{\Gamma }$ sia soddisfacibile, allora, per il lemma 1, ogni sottoinsieme $\mathrm{\Delta }\subseteq \mathrm{\Gamma }$ è soddisfacibile, quindi, ogni sottoinsieme finito di $\mathrm{\Gamma }$ è soddisfacibile. Dunque, $\mathrm{\Gamma }$ è finitamente soddisfacibile.

($\Leftarrow$) Se $\mathrm{\Gamma }$ è finitamente soddisfacibile, allora è soddisfacibile. Osserviamo innanzitutto che, se $\mathrm{\Gamma }$ è finito, la tesi è banalmente dimostrata. Ci occupiamo quindi di $\mathrm{\Gamma }$ infiniti.

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

Cominciamo con l'enumerare tutte le formule del linguaggio: $A_0,A_1,A_2\mathrm{...}$. Definiamo per induzione:

${\mathrm{\Delta }}_0=\mathrm{\Gamma };$

${\mathrm{\Delta }}_{i+1}=\{\begin{array}{cc}{\mathrm{\Delta }}_i\cup \{A_i\},& \text{se }{\mathrm{\Delta }}_i\cup \{A_i\}\text{ è finitamente soddisfacibile;}\\ {\mathrm{\Delta }}_i\cup \{\mathrm{\neg }{A}_i\},& \text{altrimenti.}\end{array}$

Sia $\mathrm{\Delta }=\bigcup _i{\mathrm{\Delta }}_i$. Osserviamo innanzitutto che $\mathrm{\Gamma }\subseteq \mathrm{\Delta }$, per costruzione. Osserviamo inoltre che $\mathrm{\Delta }$ è massimale, cioè, per ogni formula $A$, $A$ o la sua negazione appartengono a $\mathrm{\Delta }$. Infatti, siccome l'enumerazione delle formule è completa, per costruzione dei ${\mathrm{\Delta }}_i$, presa una qualunque $A$, esisterà un $i$ per cui $A=A_i$, quindi $A\in {\mathrm{\Delta }}_i\subseteq \mathrm{\Delta }$ oppure $\mathrm{\neg }A\in {\mathrm{\Delta }}_i\subseteq \mathrm{\Delta }$. Osserviamo anche che ciascun ${\mathrm{\Delta }}_i$ è finitamente soddisfacibile (per induzione: ${\mathrm{\Delta }}_0=\mathrm{\Gamma }$ è finitamente soddisfacibile; il passo induttivo è giustificato dal lemma 2). Quindi, $\mathrm{\Delta }$ è finitamente soddisfacibile, in quanto ogni sottoinsieme finito di $\mathrm{\Delta }$ è contenuto in qualche ${\mathrm{\Delta }}_i$. Dobbiamo ora mostrare che $\mathrm{\Delta }$ è soddisfacibile. Per far questo, costruiamo un modello per esso. Definiamo il modello ${ℳ}_{𝒱}$ come:

${ℳ}_{𝒱}=\{p|p\in 𝒫,p\in \mathrm{\Delta }\}$

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

$A\in \mathrm{\Delta }$ sse ${ℳ}_{𝒱}\models A$.

(Passo base) Per costruzione di ${ℳ}_{𝒱}$.

(Passo induttivo) Sia $A=\mathrm{\neg }B$. ${ℳ}_{𝒱}\models \mathrm{\neg }B$ equivale a ${ℳ}_{𝒱}⊭B$; per ipotesi induttiva, ${ℳ}_{𝒱}⊭B$ sse $B\in ̸\mathrm{\Delta }$. Siccome $\mathrm{\Delta }$ è massimale, $B\in ̸\mathrm{\Delta }$ sse $\mathrm{\neg }B\in \mathrm{\Delta }$. Pertanto, ${ℳ}_{𝒱}\models \mathrm{\neg }B$ sse $\mathrm{\neg }B\in \mathrm{\Delta }$, che è la tesi.

Sia $A=B\wedge C$. Per definizione, ${ℳ}_{𝒱}\models B\wedge C$ sse ${ℳ}_{𝒱}\models B$ e ${ℳ}_{𝒱}\models C$; per ipotesi induttiva, ${ℳ}_{𝒱}\models B$ sse $B\in \mathrm{\Delta }$ e ${ℳ}_{𝒱}\models C$ sse $C\in \mathrm{\Delta }$. Siccome $\mathrm{\Delta }$ è massimale, per il lemma 3 $B,C\in \mathrm{\Delta }$ sse ($\mathrm{\Delta }\models B$ e $\mathrm{\Delta }\models C$). ($\mathrm{\Delta }\models B$ e $\mathrm{\Delta }\models C$) sse, per definizione di congiunzione, $\mathrm{\Delta }\models B\wedge C$ e, per il lemma 3, $\mathrm{\Delta }\models B\wedge C$ sse $B\wedge C\in \mathrm{\Delta }$, che è la tesi.

Sia $A=B\vee C$. Per definizione, ${ℳ}_{𝒱}\models B\vee C$ sse ${ℳ}_{𝒱}\models B$ o ${ℳ}_{𝒱}\models C$; per ipotesi induttiva, ${ℳ}_{𝒱}\models B$ sse $B\in \mathrm{\Delta }$ e ${ℳ}_{𝒱}\models C$ sse $C\in \mathrm{\Delta }$. Siccome $\mathrm{\Delta }$ è massimale, per il lemma 3 ($B\in \mathrm{\Delta }$ o $C\in \mathrm{\Delta }$) sse ($\mathrm{\Delta }\models B$ o $\mathrm{\Delta }\models C$). ($\mathrm{\Delta }\models B$ o $\mathrm{\Delta }\models C$) sse, per definizione di disgiunzione, $\mathrm{\Delta }\models B\vee C$ e, per il lemma 3, $\mathrm{\Delta }\models B\vee C$ sse $B\vee C\in \mathrm{\Delta }$, che è la tesi.

Sia $A=B\to C$. Per definizione, ${ℳ}_{𝒱}\models B\to C$ sse ${ℳ}_{𝒱}⊭B$ o ${ℳ}_{𝒱}\models C$; per ipotesi induttiva, ${ℳ}_{𝒱}⊭B$ sse $B\in ̸\mathrm{\Delta }$ e ${ℳ}_{𝒱}\models C$ sse $C\in \mathrm{\Delta }$. Siccome $\mathrm{\Delta }$ è massimale, per il lemma 3 ($B\in ̸\mathrm{\Delta }$ o $C\in \mathrm{\Delta }$) sse ($\mathrm{\Delta }⊭B$ o $\mathrm{\Delta }\models C$). ($\mathrm{\Delta }⊭B$ o $\mathrm{\Delta }\models C$) sse, per definizione di implicazione, $\mathrm{\Delta }\models B\to C$ e, per il lemma 3, $\mathrm{\Delta }\models B\to C$ sse $B\to C\in \mathrm{\Delta }$, che è la tesi.

Sia $A=B\leftrightarrow C$. Per definizione, ${ℳ}_{𝒱}\models B\leftrightarrow C$ sse (${ℳ}_{𝒱}\models B$ sse ${ℳ}_{𝒱}\models C$); per ipotesi induttiva, ${ℳ}_{𝒱}\models B$ sse $B\in \mathrm{\Delta }$ e ${ℳ}_{𝒱}\models C$ sse $C\in \mathrm{\Delta }$. Siccome $\mathrm{\Delta }$ è massimale, per il lemma 3 ($B\in \mathrm{\Delta }$ sse $C\in \mathrm{\Delta }$) sse ($\mathrm{\Delta }\models B$ sse $\mathrm{\Delta }\models C$). ($\mathrm{\Delta }\models B$ sse $\mathrm{\Delta }\models C$) sse, per definizione di doppia implicazione, $\mathrm{\Delta }\models B\leftrightarrow C$ e, per il lemma 3, $\mathrm{\Delta }\models B\leftrightarrow C$ sse $B\leftrightarrow C\in \mathrm{\Delta }$, che è la tesi.

Abbiamo quindi mostrato che ${ℳ}_{𝒱}$ è un modello per $\mathrm{\Delta }$; siccome $\mathrm{\Gamma }\subseteq \mathrm{\Delta }$, abbiamo che ${ℳ}_{𝒱}\models \mathrm{\Gamma }$, ovvero $\mathrm{\Gamma }$ è soddisfacibile.