Vai al contenuto
Topos Uranos
Italiano

Il teorema di compattezza

Riepilogo

Una deduzione è una successione finita e usa solo un numero finito di premesse; il soddisfacimento di un insieme infinito di formule, invece, esige un’unica assegnazione che dia il valore 11 a infinite formule contemporaneamente, e nulla nella sua definizione dice che basti esaminare parti finite. Il teorema di compattezza afferma che basta: un insieme di formule è soddisfacibile se e solo se lo è ciascuno dei suoi sottoinsiemi finiti. Questa lezione lo dimostra con un argomento semantico diretto, senza passare per la deduzione: si fissano uno a uno i valori delle variabili v1,v2,…v_1, v_2, \ldots, conservando a ogni passo l’invariante per cui ogni sottoinsieme finito dell’insieme resta soddisfacibile da un’assegnazione che rispetta quanto già fissato; se nessuna delle due scelte possibili lo conservasse, l’unione dei due testimoni finiti di quel fallimento contraddirebbe l’invariante precedente, e alla fine ogni formula risulta soddisfatta grazie al lemma di coincidenza, perché ha un numero finito di variabili. Poiché le variabili sono numerate, la costruzione non ha bisogno dell’assioma della scelta. Dalla compattezza seguono le sue forme equivalenti (un insieme è insoddisfacibile se e solo se lo è qualche sua parte finita; una formula è conseguenza di un insieme se e solo se lo è di qualche parte finita) e, con la completezza per insiemi finiti di premesse della lezione precedente, la completezza forte: Γ⊨φ\Gamma \models \varphi implica Γ⊢φ\Gamma \vdash \varphi per ogni insieme Γ\Gamma, da cui la deduzione e la conseguenza semantica coincidono sempre. La lezione si chiude con applicazioni combinatorie: la colorazione di grafi infiniti a partire da quelle delle loro parti finite, le limitazioni finite che si nascondono negli enunciati infiniti e i confini di ciò che un insieme di formule può esprimere.

Obiettivi di apprendimento

  1. Definire gli insiemi finitamente soddisfacibili e dimostrare il teorema di compattezza fissando successivamente i valori delle variabili, spiegando il ruolo dell’invariante, dell’argomento dei due testimoni e del lemma di coincidenza, e perché la costruzione non ha bisogno dell’assioma della scelta.
  2. Enunciare, dimostrare e applicare le forme equivalenti della compattezza, quella dell’insoddisfacibilità e quella della conseguenza, e passare da ciascuna alle altre.
  3. Dedurre la completezza forte dalla compattezza, dalla completezza per insiemi finiti di premesse e dalla monotonia, e ricavarne la coincidenza della deduzione con la conseguenza semantica e della coerenza con la soddisfacibilità.
  4. Codificare in insiemi di formule problemi combinatori su insiemi infiniti (colorazioni, ordini, accoppiamenti) e risolverli con la compattezza, distinguendo ciò che il teorema assicura da ciò che non assicura.

Ciò che si usa dalle lezioni precedenti

Questa lezione lavora quasi interamente nella semantica, e ne usa quanto segue. Un’assegnazione è una funzione v ⁣:V→{0,1}v\colon V \to \{0, 1\} sull’insieme VV delle variabili v1,v2,v3,…v_1, v_2, v_3, \ldots, che si estende in un unico modo a tutte le formule; un’assegnazione soddisfa un insieme Γ\Gamma di formule, v⊨Γv \models \Gamma, se dà il valore 11 a ciascuna di esse, e Γ\Gamma è soddisfacibile se qualche assegnazione lo soddisfa e insoddisfacibile in caso contrario. Tutto ciò si trova nella lezione sulla semantica della logica proposizionale, insieme allo strumento centrale di questa lezione, il lemma di coincidenza: se due assegnazioni coincidono sulle variabili di φ\varphi, che formano un insieme finito V(φ)V(\varphi), danno a φ\varphi lo stesso valore.

Dalla lezione su conseguenza ed equivalenza semantica si usano la definizione di Γ⊨φ\Gamma \models \varphi (ogni assegnazione che soddisfa Γ\Gamma soddisfa φ\varphi), le sue proprietà strutturali, in particolare la monotonia (se Γ⊆Δ\Gamma \subseteq \Delta e Γ⊨φ\Gamma \models \varphi, allora Δ⊨φ\Delta \models \varphi) e la quinta (un insieme insoddisfacibile ha per conseguenza ogni formula), e il teorema di conseguenza e insoddisfacibilità: Γ⊨φ\Gamma \models \varphi se e solo se Γ∪{¬φ}\Gamma \cup \{\neg\varphi\} è insoddisfacibile. Dalla lezione sulle leggi generalizzate di De Morgan e distributive si usa il lemma del valore: ⋀i=1nφi\bigwedge_{i=1}^{n} \varphi_i vale 11 se e solo se tutti i suoi termini valgono 11, e ⋁i=1nφi\bigvee_{i=1}^{n} \varphi_i, se e solo se qualcuno vale 11. Infine, ⊤:=(v1→v1)\top := (v_1 \rightarrow v_1) è una tautologia e ⊥:=¬⊤\bot := \neg\top, una contraddizione.

Dal lato della deduzione, la lezione sui sistemi deduttivi formali ha dimostrato la monotonia (Mon: se Γ⊆Δ\Gamma \subseteq \Delta e Γ⊢φ\Gamma \vdash \varphi, allora Δ⊢φ\Delta \vdash \varphi) e la finitezza (Fin: se Γ⊢φ\Gamma \vdash \varphi, qualche sottoinsieme finito Γ0\Gamma_0 di Γ\Gamma verifica Γ0⊢φ\Gamma_0 \vdash \varphi), e la lezione sulle quattro tecniche di deduzione ha verificato che entrambe valgono nel sistema del corso (gli schemi A1, A2 e A3, il modus ponens e la sostituzione della doppia negazione, SDN), a cui si riferisce d’ora in poi il simbolo ⊢\vdash. Infine, la lezione su correttezza e completezza ha dimostrato il teorema di correttezza (Γ⊢φ\Gamma \vdash \varphi implica Γ⊨φ\Gamma \models \varphi, per ogni Γ\Gamma) e la completezza per insiemi finiti di premesse: se {γ1,…,γk}⊨φ\{\gamma_1, \ldots, \gamma_k\} \models \varphi, allora {γ1,…,γk}⊢φ\{\gamma_1, \ldots, \gamma_k\} \vdash \varphi.