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

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

Definizioni

Insieme di formule finitamente soddisfacibile

Definizione

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

Insieme di formule massimale

Definizione

Un insieme di formule $\Gamma$ si dice massimale sse per ogni $A$ di ${\mathcal {L}}$ si ha $A\in \Gamma$ oppure $\neg A\in \Gamma$.

Lemma 1

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

Dimostrazione

Supponiamo che $\Gamma$ sia soddisfacibile, ma che esista un sottoinsieme $\Delta \subseteq \Gamma$ insoddisfacibile. Allora, per definizione, per ogni modello ${\mathcal {M_{V}}}$ esiste una formula $A\in \Delta$ tale che ${\mathcal {M_{V}}}\nvDash A$. Essendo $\Delta \subseteq \Gamma$, allora $A\in \Gamma$. Quindi, per ogni modello ${\mathcal {M_{V}}}$ esiste una formula $A\in \Gamma$ tale che ${\mathcal {M_{V}}}\nvDash A$. Dunque, $\Gamma$ è insoddisfacibile. Contraddizione.

Lemma 2

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

Dimostrazione

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

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

Lemma 3

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

Dimostrazione

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

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

Dimostrazione

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

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

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

Cominciamo con l'enumerare tutte le formule del linguaggio: $A_{0},A_{1},A_{2}...$. Definiamo per induzione:

$\Delta _{0}=\Gamma ;$

$\Delta _{i+1}={\begin{cases}\Delta _{i}\cup \{A_{i}\},&{\text{se }}\Delta _{i}\cup \{A_{i}\}{\text{ è finitamente soddisfacibile;}}\\\Delta _{i}\cup \{\neg A_{i}\},&{\text{altrimenti.}}\end{cases}}$

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

${\mathcal {M_{V}}}=\{p|p\in {\mathcal {P}},p\in \Delta \}$

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

$A\in \Delta$ sse ${\mathcal {M_{V}}}\models A$.

(Passo base) Per costruzione di ${\mathcal {M_{V}}}$.

(Passo induttivo) Sia $A=\neg B$. ${\mathcal {M_{V}}}\models \neg B$ equivale a ${\mathcal {M_{V}}}\nvDash B$; per ipotesi induttiva, ${\mathcal {M_{V}}}\nvDash B$ sse $B\not \in \Delta$. Siccome $\Delta$ è massimale, $B\not \in \Delta$ sse $\neg B\in \Delta$. Pertanto, ${\mathcal {M_{V}}}\models \neg B$ sse $\neg B\in \Delta$, che è la tesi.

Sia $A=B\land C$. Per definizione, ${\mathcal {M_{V}}}\models B\land C$ sse ${\mathcal {M_{V}}}\models B$ e ${\mathcal {M_{V}}}\models C$; per ipotesi induttiva, ${\mathcal {M_{V}}}\models B$ sse $B\in \Delta$ e ${\mathcal {M_{V}}}\models C$ sse $C\in \Delta$. Siccome $\Delta$ è massimale, per il lemma 3 $B,C\in \Delta$ sse ($\Delta \models B$ e $\Delta \models C$). ($\Delta \models B$ e $\Delta \models C$) sse, per definizione di congiunzione, $\Delta \models B\land C$ e, per il lemma 3, $\Delta \models B\land C$ sse $B\land C\in \Delta$, che è la tesi.

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

Sia $A=B\to C$. Per definizione, ${\mathcal {M_{V}}}\models B\to C$ sse ${\mathcal {M_{V}}}\nvDash B$ o ${\mathcal {M_{V}}}\models C$; per ipotesi induttiva, ${\mathcal {M_{V}}}\nvDash B$ sse $B\not \in \Delta$ e ${\mathcal {M_{V}}}\models C$ sse $C\in \Delta$. Siccome $\Delta$ è massimale, per il lemma 3 ($B\not \in \Delta$ o $C\in \Delta$) sse ($\Delta \nvDash B$ o $\Delta \models C$). ($\Delta \nvDash B$ o $\Delta \models C$) sse, per definizione di implicazione, $\Delta \models B\to C$ e, per il lemma 3, $\Delta \models B\to C$ sse $B\to C\in \Delta$, che è la tesi.

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

Abbiamo quindi mostrato che ${\mathcal {M_{V}}}$ è un modello per $\Delta$; siccome $\Gamma \subseteq \Delta$, abbiamo che ${\mathcal {M_{V}}}\models \Gamma$, ovvero $\Gamma$ è soddisfacibile.