Teorema di completezza per il calcolo proposizionale

Alessandro Berarducci

15 Ott. 2004

1 Calcolo proposizionale

Definizione 1.1 Un linguaggio proposizionale è un insieme L di simboli chiamati variabili proposizionali.

L’insieme delle formule proposizionali nel linguaggio L è un insieme di espressioni definito induttivamente come segue. Ogni variabile proposizionale A ∈ L è una formula proposizionale. Se ϕ e ψ sono formule proposizionali, lo sono anche ¬ϕ e (ϕ ∧ ψ).

I connettivi ∧ (congiunzione) e ∨ (disgiunzione) si possono introdurre per definizione:

(A ∧ B) per ¬(A → ¬B);

(A ∨ B) per ¬A → B.

Definizione 1.2 Una L-interpretazione è una funzione M che associa ad ogni variabile proposizionale A ∈ L un valore M(A) ∈ {0, 1} (0 per falso, 1 per vero). Estendiamo M ad una funzione dall’insieme di tutte le L-formule proposizionali a {0, 1} stabilendo che M(¬ϕ) = 1 se e solo se M(ϕ) = 0 e che M((α → β)) = 1 se e solo se non si verifica che M(α) = 1 e M(β) = 0.

Definizione 1.3 Una tautologia è una L-formula vera in tutte le Linterpretazioni.

Ad esempio A → A è una tautologia, in quanto risulta vera sia nel caso in cui A è vera, sia nel caso in cui A è falsa.

Definizione 1.4 Fissiamo un linguaggio proposizionale L. Una L-teoria è un insieme Γ di L-formule. Le formule appartenenti a Γ vengono chiamate assiomi della teoria Γ. Un modello di una L-formula ϕ è una L-interpretazione che rende vera ϕ. Un modello di una L-teoria Γ è una L-interpretazione che rende vere tutte le formule di Γ. Diciamo che una L-formula ϕ è conseguenza logica di Γ, e scriviamo Γ ⊧ ϕ, se ogni modello di Γ è modello di ϕ. Se Γ è vuoto scriviamo ⊧ ϕ per Γ ⊧ ϕ. In base alle definizioni ⊧ ϕ se e solo se ϕ è una tautologia.

1.1 Gli assiomi e i teoremi del calcolo proposizionale

Assiomi logici.

Per ogni scelta di formule proposizionali A, B, C (non necessariamente atomiche) abbiamo i seguenti “assiomi logici”:

A0. A → A

A1. A → (B → A)

A2. (A → (B → C)) → ((A → B) → (A → C))

A3. ((¬B → ¬A) → ((¬B → A) → B))

A0, A1, A2, A3 sono “schemi” di assiomi, cioè ognuno rappresenta una infinitá di assiomi. Si noti che ogni istanza di questi schemi è una tautologia.

Regola di inferenza (modus ponens).

\frac{A,A→B}{B}.

Significato: da A e da A → B si può dedurre B.

Teoremi.

Fissiamo un linguaggio L e una L-teoria Γ. I teoremi di Γ sono definiti induttivamente da:

1. Ogni assioma di Γ è un teorema di Γ;

2. ogni assioma logico è un teorema di Γ;

3. se A e A → B sono teoremi di Γ, allora B è un teorema di Γ.

Scriviamo Γ ⊢ B per dire che B è un teorema di Γ. Se Γ è vuoto scriviamo ⊢ B per Γ ⊢ B.

Una dimostrazione formale di B da Γ è una successione finita di formule (B_{0}, B_{1}, …, B_{n}) tale che B_{n} = B e ogni B_{i} o è un assioma logico, o è un assioma di Γ, o si ottiene da due formule precedenti nella successione per modus ponens.

L’insieme dei teoremi di Γ viene indicato con T h(Γ).

Lemma 1.5 Assumiamo che Γ ⊢ θ_{1}, …, Γ ⊢ θ_{n} e che {θ_{1}, …, θ_{n}} ⊢ α. Allora Γ ⊢ α.

Dim. Basta concatenare (mettere in fila) le dimostrazioni di θ_{1}, …, θ_{n} da Γ e farle seguire da una dimostrazione di α da {θ_{1}, …, θ_{n}} per ottenere una dimostrazione di α da Γ (verificare!). QED

1.2 Il teorema di deduzione

Teorema 1.6 (Teorema di deduzione, Herbrand 1930) Siano A e B formule proposizionali e sia Γ un insieme di formule proposizionali. Se Γ, A ⊢ B, allora Γ ⊢ A → B.

Dim. La dimostrazione è per induzione sulla lunghezza delle derivazioni (= dimostrazioni formali). Si usano solo gli schemi di assiomi A0, A1, A2 concernenti l’implicazione e non lo schema A4 che concerne la negazione. Sia (B_{0}, B_{1}, …, B_{n}) una dimostrazione di B da Γ ∪ {A}. Mostriamo per induzione su i ≤ n, che Γ ⊢ A → B_{i} (poichè B = B_{n} quando arriviamo a i = n abbiamo il risultato desiderato). Supponiamo per ipotesi induttiva che il risultato sia vero per ogni j < i (se i = 0 questa è una assunzione vuota) e mostriamo che vale per i, cioè Γ ⊢ A → B_{i}. Ci sono tre casi da considerare.

Caso 1. B_{i} è un assioma logico. Ne segue che ⊢ B_{i} e quindi a fortiori: a) Γ ⊢ B_{i}. D’altra parte lo schema A1 garantisce che b) Γ ⊢ B_{i} → (A → B_{i}). Concludiamo Γ ⊢ A → B_{i} per MP (modus ponens) da a) e b).

Caso 2. B_{i} è un assioma non logico, cioè B_{i} ∈ Γ∪{A}. Se B_{i} ∈ Γ ragioniamo esattamente come nel caso 1. Se B_{i} = A usiamo lo schema A0 per ottenere Γ ⊢ A → B_{i}.

Caso 3. B_{i} segue da due formule precedenti, diciamo da B_{j} e B_{k} (con j, k < i) per modus ponens. (Notiamo che questo caso si puó verificare solo se i ≠ 0.) Affinchè sia possibile applicare il modus ponens ne segue che una di queste due formule, diciamo B_{k}, è la “premessa maggiore” del modus ponens, cioè B_{k} = B_{j} → B_{i}. Per ipotesi induttiva abbiamo a) Γ ⊢ A → B_{j} e b) Γ ⊢ A → (B_{j} → B_{i}). Per lo schema A2 abbiamo c) Γ ⊢ (A → (B_{j} → B_{i})) → ((A → B_{j}) → (A → B_{i})). Applichiamo ora MP a b) e c) per ottenere d) Γ ⊢ ((A → B_{j}) → (A → B_{i})). Un’ultima applicazione del MP ad a) e d) fornisce il risultato desiderato Γ ⊢ A → B_{i}. QED

1.3 Teorie coerenti

Definizione 1.7 Diciamo che Γ è incoerente (o contraddittoria) se esiste una formula θ tale che Γ ⊢ θ e Γ ⊢ ¬θ. Diciamo che Γ è coerente in caso contrario.

Lemma 1.8 Sono equivalenti:

1. Esiste una formula θ tale che Γ ⊢ θ e Γ ⊢ ¬θ;

2. Per ogni formula φ, Γ ⊢ φ.

Dim. Da (2) segue banalmente (1). Viceversa assumiamo (1) e sia data φ. Vogliamo mostrare che Γ ⊢ φ. Usando la (1) scegliamo θ tale che Γ ⊢ θ e Γ ⊢ ¬θ. Per lo schema di assiomi logici A2 abbiamo Γ ⊢ θ → (¬φ → θ) e similmente Γ ⊢ ¬θ → (¬φ → ¬θ). Per modus ponens Γ ⊢ ¬φ → θ e Γ ⊢ ¬φ → ¬θ. Per lo schema A3 Γ ⊢ (¬φ → ¬θ) → ((¬φ → θ) → φ). Applicando due volte il modus ponens ottengo Γφφ. QED

Quindi Γ è incoerente se e solo se dimostra ogni formula.

Osserviamo che Γ è coerente se e solo se T h(Γ) lo è.

Il seguente risultato mostra che la relazione di derivabilitá “⊢” e il predicato “essere contraddittoria” sono interdefinibili.

Proposizione 1.9 Γ ⊢ ϕ se e solo se Γ ∪ {¬ϕ} è incoerente.

Dim. Se Γ ⊢ ϕ, allora Γ ∪ {¬ϕ} è chiaramente incoerente perchè è una teoria che dimostra sia ϕ che ¬ϕ.

Viceversa assumiamo che Γ∪{¬ϕ} sia incoerente, e che quindi dimostri tutte le formule. Data una formula β abbiamo allora in particolare Γ ∪ {¬ϕ} ⊢ ¬β e Γ ∪ {¬ϕ} ⊢ β. Per il teorema di deduzione Γ ⊢ ¬ϕ → ¬β e Γ ⊢ ¬ϕ → β. Per lo schema A3 Γ ⊢ (¬ϕ → ¬β) → ((¬ϕ → β) → ϕ). Applicando due volte il modus ponens ottengo Γφϕ. QED

Corollario 1.10 Supponiamo che le teorie Γ∪{¬ϕ} e Γ∪{¬ϕ} siano entrambe incoerenti. Allora anche Γ lo è.

Dim. Poichè Γ ∪ {¬ϕ} è incoerente abbiamo Γ ⊢ ϕ. Ne segue che i teoremi di Γ coincidono con quelli di Γ ∪ {ϕ}, ed essendo quest’ultima teoria incoerente lo è anche Γ. QED

1.4 Teorie complete

Definizione 1.11 Una L-teoria coerente Γ si dice completa se data una Lformula ϕ o Γ ⊢ ϕ o Γ ⊢ ¬ϕ.

Definizione 1.12 Fissato un linguaggio proposizionale L, una L-teoria Γ si dice coerente massimale se è coerente e non è propriamente inclusa in alcun’altra L-teoria coerente.

Osservazione 1.13 Supponiamo che Γ sia coerente massimale e Γ ⊢ ϕ. Allora ϕ ∈ Γ.

Dim. Se ϕ ∉ Γ allora Γ ∪ {¬ϕ} è una estensione propria di Γ ed è pertanto incoerente. Ma siccome Γ ⊢ ϕ, Γ e Γ ∪ {ϕ} hanno gli stessi teoremi, e pertanto anche Γ sarebbe incoerente. QED

Teorema 1.14 Sono equivalenti:

1. Γ è coerente massimale;

2. Γ è coerente e per ogni formula ϕ, ϕ ∈ Γ oppure ¬ϕ ∈ Γ.

Dim. 1 → 2. Supponiamo che ϕ ∉ Γ e ¬ϕ ∉ Γ. Allora entrambe le teorie Γ ∪ {θ} e Γ ∪ {¬θ} estendono propriamente Γ. Ma per il Lemma 1.10 una di queste due teorie è coerente, contraddicendo la massimalià di Γ.

2 → 1. Assumendo (2) dobbiamo mostrare che Γ non è estendibile ad una teoria coerente Δ ⊃ Γ. Infatti se ϕ ∈ Δ \ Γ, per (2) abbiamo ¬ϕ ∈ Γ. Ma allora Δ conterrebbe sia ϕ che ¬ϕ e pertanto non sarebbe coerente. QED

Lemma 1.15 Consideriamo una famiglia {T_{i} | i ∈ I} di L-teorie che formano una catena, cioè per ogni i, j ∈ I T_{i} ⊂ T_{j} o T_{j} ⊂ T_{i}. Sia ⋃_{i∈I} T_{i} l’unione della catena. Se ⋃_{i∈I} T_{i} ⊢ φ, allora esiste i ∈ I tale che T_{i} ⊢ φ.

Dim. Consideriamo l’insieme S ⊂ ⋃_{i} T_{i} degli assiomi utilizzati nella dimostrazione di φ. S è ovviamente un insieme finito, ed essendo incluso nell’unione della catena ⋃_{i} T_{i} è incluso in una delle T_{i} (qui si usa l’ipotesi che le T_{i} formino una catena).QED

Corollario 1.16 Siano T_{i}, per i ∈ I, L-teorie coerenti. Una condizione sufficiente affinchè l’unione ⋃_{i∈I} T_{i} sia coerente è che le T_{i} formino una catena, cioè per ogni i, j ∈ I T_{i} ⊂ T_{j} o T_{j} ⊂ T_{i}.

Dim. Se ⋃_{i∈I} T_{i} è incoerente dimostra una contraddizione (ovvero dimostra una formula B e la sua negazione). Per il lemma precedente esisterebbe allora un T_{i} da cui si deduce la stessa contraddizione. QED Lemma 1.17 (Lemma di Lindembaum) Ogni L-teoria coerente Γ è contenuta in una L-teoria coerente massimale.

Dim. Per semplicità consideriamo dapprima il caso in cui L sia numerabile. Possiamo allora fissare una enumerazione {ϕ_{n} | n ∈ N} dell’insieme delle Lformule. Sia T_{0} = Γ e induttivamente definiamo T_{n+1} come T_{n} ∪ {ϕ_{n}} se questa teoria è coerente, e come T_{n} ∪ {¬ϕ_{n}} nel caso contrario. Per il lemma 1.10 T_{n+1} è coerente se T_{n} lo è. Quindi per induzione tutte le T_{n} sono coerenti e per per il corollario precedente lo è la loro unione T′ = ⋃_{n∈N} T_{n}. Data una qualsiasi formula θ ∈ {ϕ_{n} | n ∈ N}, T′ deve contenere una delle due formule θ o ¬θ (se θ = ϕ_{n}, o θ o la sua negazione appartiene a T_{n+1}). Quindi per il Lemma 1.14 T′ è coerente massimale.

Il caso in cui L non è numerabile si dimostra applicando il lemma di Zorn all’insieme di tutte le L-teorie coerenti contenenti Γ ordinate per inclusione. Le ipotesi del lemma di Zorn sono verificate grazie al Corollario 1.16. QED

1.5 Teorema di completezza per la logica proposizionale

Lemma 1.18 Sia T una L-teoria coerente massimale.

1. Se (α → β) ∈ T, allora β ∈ T o ¬α ∈ T.

2. Se (α → β) ∉ T, allora α ∈ T e ¬β ∈ T.

Dim. (1) Supponiamo che (α → β) ∈ T. Se non vale la (1) allora per la massimalià ¬β ∈ T e α ∈ T. Per modus ponens anche β ∈ T, contraddicendo la coerenza di T.

(2) Supponiamo (α → β) ∉ T. Per la massimalità ¬(α → β) ∈ T.

Mostriamo che α ∈ T. In caso contrario per la massimalità ¬α ∈ T. Ora {α, ¬α} è una teoria incoerente e pertanto dimostra β. Applicando due volte il teorema di deduzione ¬α → (α → β). D’altra parte siccome ¬α ∈ T, per modus ponens T ⊢ α → β. Sappiamo però che ¬(α → β) ∈ T e quindi T sarebbe incoerente.

Resta da dimostrare che ¬β ∈ T. In caso contrario per la massimalità β ∈ T. Per lo schema A1 T ⊢ β → (α → β). Per modus ponens T ⊢ α → β. Sappiamo però che ¬(α → β) ∈ T e quindi T sarebbe incoerente. QED

Teorema 1.19 (Teorema di completezza) Se Γ è coerente, Γ ha un modello.

Dim. Sia Γ coerente. Per il lemma di Lindembaum esiste una estensione Δ ⊆ Γ coerente massimale. Osserviamo che ogni modello di Δ è anche un modello di Γ. basta quindi trovare un modello M della teoria coerente massimale Δ.

Definiamo M: L → {0, 1} come segue: M(A) = 1 se A ∈ Δ, M(A) = 0 se ¬A ∈ Δ. Questa è una buona definizione di M in quanto Δ è coerente massimale. Estendiamo M a tutte le formule proposizionali usando le tavole di verità. Mostriamo per induzione sulla lunghezza delle formule, che per ogni formula ϕ si ha: M(ϕ) = 1 se A ∈ Δ e M(ϕ) = 0 se ¬ϕ ∈ Δ. Il caso in cui ϕ è una variabile proposizionale di L è vero per definizione di M. Il caso ϕ = ¬θ è ovvio. Per dimostrare il caso ϕ = (α → β) possiamo usare il lemma precedente e l’ipotesi induttiva. Infatti se (α → β) ∈ Δ, per il lemma β ∈ Δ o ¬α ∈ Δ. Per ipotesi induttiva M(β) = 1 o M(¬α) = 1. Per le tavole di verità M(α → β) = 1. Infine se (α → β) ∉ Δ, per il lemma α ∈ Δ e ¬β ∈ Δ. Per ipotesi induttiva M(α) = 1 e M(¬β) = 1. Per le tavole di verità M(α → β) = 0. QED

Corollario 1.20 Se T ⊧ ϕ allora T ⊢ ϕ.

Dim. Se T ⊬ ϕ allora T ∪ {¬ϕ} è coerente e per il teorema di completezza ha un modello. Tale modello testimonia T |̸= ϕ. QED Lemma 1.21 (Teorema di correttezza) Se T ⊢ ϕ allora T ⊧ ϕ.

Dim. Tutte le L-interpretazioni verifica gli assiomi logici A0-A4. Se una Linterpretazione verifica le due premesse di una applicazione del modus ponens, allora verifica anche la conclusione. Ne segue per induzione sulla lunghezza delle dimostrazioni che se una L-interpretazione verifica tutti gli assiomi di T essa verifica anche ϕ. QED

Teorema 1.22 (Compattezza) Se T ⊧ ϕ allora esiste una sottoteoria finita T′ di T tale che T′ ⊧ ϕ.

Dim. Per il teorema di correttezza e completezza la relazione ⊧ equivale a ⊢. Rimpiazzando ⊧ con ⊢ il teorema di compattezza diventa ovvio in quanto una qualsiasi dimostrazione usa solo un numero finito di assiomi. QED