Insieme finitamente soddisfacibile

Definizione: Un insieme di formule $\Gamma$ è finitamente soddisfacibile se e solo se ogni sottoinsieme finito di $\Gamma$ è soddisfacibile.

Nel seguito, si scriverà $\Delta \subset_{FIN} \Gamma$ e $\Delta\subseteq_{FIN}\Gamma$ per indicare che $\Delta$ è un sottoinsieme finito (rispettivamente proprio o meno) di $\Gamma$.

Teorema di compattezza

Si vuol e dimostrare il seguente teorema:

Teorema (di compattezza): Un insieme è soddisfacibile se e solo se è finitamente soddisfacibile.

Osservazione: Verificare la soddisfacibilità di un insieme infinito corrisponde a mostrare l’esistenza di una valutazione che verifca contemporaneamente tutte le (infinite) formule dell’insieme. Invece, considerare la soddisfacibilità dei suoi sottoinsiemi finiti non obbliga, in linea di principio, a considerare la stessa valutazione per tutti i sottoinsiemi.

La parte complicata della dimostrazione è provare che la soddisfacibilità di tutti i sottoinsiemi finiti di $\Gamma$ (in base a valutazioni potenzialmente diverse) comporta la soddisfacibilità dell’intero insieme $\Gamma$, cioè l’esistenza di una valutazione che soddisfa contemporaneamente tutte le formule di $\Gamma$.

Viceversa, se un insieme $\Gamma$ è soddisfacibile, allora è banale mostrare che anche ogni suo sottoinsieme (finito) $\Delta$ è soddisfacibile:

Infine, è banale anche il caso in cui $\Gamma$ è finito: se $\Gamma$ è finitamente soddisfacibile, tutti i suoi sottoinsiemi finiti sono soddisfacibili, ma uno di questi è $\Gamma \subseteq_{FIN}\Gamma$, qiundi $\Gamma$ è soddisfacibile.

Schema della dimostrazione

La dimostrazione della “parte difficile” del teorema di compattezza segue uno schema per certi versi simile a quello del teorema di completezza di $\Tau_{CPL}$.

• Si mostrerà (LFC2) che, dato un insieme finitamente soddisfacibile $\Gamma$, lo si può estendere in un insieme che ha una “struttura forte” (è finitamente soddisfacibile e, in più, anche completo) $\Gamma^*$.
• Si mostrerà (LFC1) che, a partire da un insieme ifntamente soddisfacibile e completo $\Gamma^$, si può definire una valutazione $v$ tale che $v\models \Gamma^$. Siccome $\Gamma^$ è un’estensione di $\Gamma$, cioè $\Gamma \subseteq\Gamma^$, da $v\models \Gamma^*$ si deduce che $v\models \Gamma$.

Insieme completo

Definizione: Un insieme di formule $\Gamma$ è completo se e solo se, per ogni formula $H\in FORM$, si ha che $H\in \Gamma$ oppure $\neg H\in \Gamma$.

Osservazione: Per definizione, un insieme completo di formule è infinito (dovendo contenere un elemento per ognuna delle possibili formule della logica proposizionale classica, che sono infinite).

Proprietà degli insiemi completi finitamente soddisfacibili

Proposizione (PFC1): Sia $\Gamma$ un insieme di formule completo e finitamente soddisfacibile.