Aspetti semantici della logica proposizionale modale

CAPITOLO 1
Introduzione
1. Sistemi modali
Sia L un linguaggio proposizionale i cui simboli primitivi sono:
● Variabili enunciative p q r ;
● Un connettivo binario: → ;
● Una costante logica –;
più i segni ( e ). Le formule vengono indicate con lettere greche e de nite
induttivamente come segue:
De nizione 1.1
Ogni variabile proposizionale p è una formula;
Se è una formula, anche ¬ lo è;
Se e sono formule, allora anche → .
Niente altro è una formula
VarL e FormL indicano rispettivamente l insieme di variabili e formule di L.
E possibile fornire molte assiomatizzazioni del calcolo proposizionale classico
(d ora in avanti CPC). La seguente è la lista di schemi d assiomi utilizzata nel
lavoro:
A1: → ( → )
A2: ( → ( → ))→ (( → )→ ( → ))
A3: (( → –)→ ( → –))→ ( → )
più la regola del modus ponens
MP →
I connettivi ∨ ∧ ¬ ↔ e la costante ⊺ possono essere de niti per mezzo dell in-
sieme (funzionalmente completo) {→ –} nel seguente modo:
¬ = → –
∨ = ¬ →
∧ = ¬( → ¬ )
↔ = ( → ) ∧ ( → )
5
1. Introduzione
⊺ = –→ –
Un linguaggio proposizionale modale ML è ottenuto da L con laggiunta del
simbolo ◻ e della corrispondente regola di formazione:
● Se è una formula in ML allora anche ◻ lo è.
E possibile introdurre un ulteriore connettivo ◇ de nendo ◇ =def ¬ ◻ ¬ . Si
può in ne abbreviare la reiterazione di un operatore modale scrivendo ◻n quando
◻ ◻
´¹¹¹¹¹¸¹¹¹¹¹¶
n−volte
e ◇n quando ◇ ◇
´¹¹¹¹¹¹¹¹¸¹¹¹¹¹¹¹¹¹¶
n−volte
.
Si noti che l interpretazione di ◻ come necessario e di ◇ come possibile , che
è quella usualmente data, non è l unica possibile: solo per citarne alcune, ◻ può
essere letto come è dimostrabile , è obbligatorio (logica deontica), è vero adesso
e lo sarà per sempre (con◇ leggibile come è vero adesso o lo sarà in futuro )1. Sarà
chiaro in seguito che una stessa formula può essere vera per una data interpretazione
dei connettivi modali, ma falsa per altre interpretazioni.
Non è certamente scopo di questa tesi proporre un elenco degli innumerevoli
sistemi modali esistenti; ci limiteremo ai principali sistemi cosiddetti normali
De nizione 1.2 Un sistema modale proposizionale è detto normale se è assioma-
tizzato da A1-A3 di CPC, Def◇ più l assioma:
K ∶ ◻ ( → )→ (◻ → ◻ )
la regola del Modus ponens e la regola di necessitazione (RN)
RN ◻
Il sistema K, il minimo sistema modale normale, è quindi un estensione del
calcolo proposizionale classico, e ⊢K signi ca che esiste una sequenza di formule
che termina con tale che ogni fomula della sequenza è un assioma, oppure il
risultato dell applicazione di una regola di inferenza ad un i ∈ .
Assumendo un punto di vista più generale possiamo de nire in maniera più
astratta, e forse più adatta agli scopi di questo lavoro, una logica modale normale.
De nizione 1.3 Dato un insieme di fb , la logica modale normale K è il più
piccolo insieme  ⊆ che contiene tutti i teoremi di CPC, ◻( → )→ (◻ → ◻ ),
Def◇ ed è chiuso rispetto a Modus ponens e RN, cioè se { → ∈  } allora ∈  
e se ∈  allora ◻ ∈  .
Da notare che, stante questa de nizione, la logica classica è in e etti la più
piccola logica modale.
Il considerare sistemi assiomatici piuttosto che logiche, intese come insiemi di
formule chiuse rispetto a certe regole, ha certamente il vantaggio che è possibile
costruire ulteriori logiche semplicemente sfruttando la basa assiomatica di un certo
1Si veda [8], p. 62.
6
1. Introduzione
sistema di partenza aggiungendo ulteriori assiomi; ad esempio da K si possono
ottenere quasi tutti i sistemi normali presentati in questo lavoro.
Gli esempi di cui ci serviremo sono tratti dal seguente elenco:
K = ◻(→ )→ (◻ → ◻q)
D = ◻ →◇
T = ◻ →
B = → ◻◇
4 = ◻ → ◻ ◻
5 =◇ → ◻◇
G =◇◻ → ◻◇
G′ =◇k ◻l → ◻m◇n
M = ◻◇ →◇◻
L = ◻(◻ → )→
C = (◻ ∧ ◻ )→ ◻( ∧ )
F = ◻( ∧ )→ (◻ ∧ ◻ )
R = (◻ ∧ ◻ )↔ ◻( ∧ )
V B =◇◻ ∨ ◻(◻(◻ → )→
MV =◇◻ ∨ ◻
H = ◻(◻ ↔ ))→ ◻
Seguendo una linea iniziata con Lemmon e Scott [29] e seguita da Chellas [10], i
vari sistemi vengono nominati secondo questa regola:
KS1 Sn =def ⋂{∑ ∣∑ è una logica normale e S1 ∪ ∪ Sn ⊆∑}
cioè KS1 Sn è il più piccolo sistema modale contenente tutte gli esempi delle
formule S1 Sn.
E possibile quindi caratterizzare diversi sistemi a partire daK con concatenando
assiomi aggiuntivi. Tra i sistemi più noti nella letteratura sull argomento:
KD: K⊕D
KT: K⊕ T
KTB: KT⊕B
KT4: KT⊕ 4
KT5: KT⊕ 5
Con K ⊆ KD ⊆ KDT ⊆ B S4 ⊆ S5, nel senso che ogni teorema di K è un
teorema di KD e quindi di tutti i sistemi in cui KD è incluso, e così via. In altri
termini, per le relazioni di deducibilità riferite ai vari sistemi, cui prima ci siamo
7
1. Introduzione
riferiti con il simbolo ⊢K per il sistema K, vale la seguente implicazione
⊢K⇒⊢KD⇒⊢KT⇒⊢KTB
E tuttavia possibile dimostrare che D ≠ T ≠ B ≠ S4 ≠ S5, cosicchè l inclusione
diventa propria.
La gura 1.1 indica in che rapporto stanno i vari sistemi.
Figura 1.1. Schema di alcuni sistemi proposizionali modali
L assiomatizzazione di K data nella de nizione 1.2 non è comunque l unica
possibile. Seguendo Chellas [10], è possibile assiomatizzare K come CPC + Def◇
+ RK, dove
RK
( 1 ∧ ∧ n)→
(◻ 1 ∧ ∧ ◻ n)→ ◻
Così RN è RK con n = 0, e K si ottiene facilmente notando che :
(( → ) ∧ )→ (teorema di CPC)
(◻( → ) ∧ ◻ )→ ◻ (per RK)
(◻( → )→ (◻ → ◻ (per CPC)
Con n = 2 e n = 1, si hanno, rispettivamente,
RR
( ∧ )→
(◻ ∧ ◻ )→ ◻
RM →
◻ → ◻
Questo ci permette di indicare logiche di sistemi non normali in termini di regole.
Si avrà così che
Un sistema regolare è dato da CPC + Def◇ + RR.
Un sistema monotono è dato da CPC + Def◇ + RM.
Un sistema classico è dato da CPC + Def◇ + RE.
8
1. Introduzione
dove
RE
↔
(◻ ↔ ◻ )
Ed in generale vale l inclusione CLASS ⊂ MONOT ⊂ REGOL ⊂ NORM ,
nel senso che ogni sistema normale è regolare, quindi monotono e classico.
L oggetto del nostro lavoro sono esclusivamente i sistemi normali; tuttavia, trat-
tando la semantica algebrica, capiterà di fare riferimento a sistemi più deboli (classi-
ci), motivo per cui si è accennato alla questione. Che la semantica algebrica si possa
applicare ai sistemi classici dipende dal risultato seguente, come vedremo meglio nel
capitolo secondo.
Teorema 1.4 Sia una formula modale e sia [ / ] la formula ottenuta rimpiaz-
zando occorrenze di con entrambe sottoformule di . Allora in ogni sistema  
chiuso rispetto a RE vale la seguente regola:
Sost. equiv.
↔
( ↔ [ / ])
Dimostrazione. Per induzione su . Se = p, allora p[ / ] = p e quindi
⊢ p[ / ] ↔ p banalmente. I casi booleani sono immediati. Il caso interessante
riguarda ◻. Si assuma per ipotesi di induzione che ⊢ [ / ] ↔ . Per RE vale
allora ⊢ ◻ [ / ]↔ ◻ . Dal momendo che (◻ )[ / ] = ◻( [ / ]), si ha ⊢ ◻ ↔
(◻ )[ / ]. ⊣
Si noti che nella dimostrazione di Sost equiv si è fatto uso solo di RE: ciò
signi ca che la regola vale non solo nei sistemi classici, ma anche in quelli regolari,
monotoni e normali, in cui RE è derivabile. Questo ha ri essi sulla costruzione delle
cosiddette algebre di Lindembaum, di cui ci occuperemo nel capitolo sulla semantica
algebrica.
Nel corso del lavoro verranno utilizzate anche regole ed assiomi duali:
RK◇
→ ( 1 ∨ ∨ n)
◇ → (◇ 1 ∨ ∨◇ n)
RN◇ ◇
RM◇ →◇ →◇
RR◇
→ ( ∧ )
◇ → (◇ ∧◇ )
e
D◇: ◻ →◇
T◇: ◻ →
B◇: ◇◻ →
4◇: ◇◇ →◇
9
1. Introduzione
5◇: ◇◻ →◇
Tutti facilmente derivabili dalle rispettive regole ed assiomi. Ad esempio, per
RK◇:
⊢ → ( 1 ∨ ∨ n)
⊢ (¬ 1 ∧ ∧ ¬ n)→ ¬ [per logica proposizionele]
⊢ (◻¬ 1 ∧ ∧ ◻¬ n)→ ◻¬ [per RK]
⊢ ¬ ◻ ¬ → (¬ ◻ ¬ 1 ∧ ∧ ¬ ◻ ¬ n) [per logica proposizionale]
⊢◇ → (◇ 1 ∧ ∧◇ n) [◇ = ¬ ◻ ¬]
2. Semantica relazionale
Sia ML un linguaggio enunciativo modale come de nito in precedenza.
De nizione 1.5 Una struttura relazionale è una coppia F = ⟨W R⟩ dove W è un
insieme non vuoto i cui elementi sono detti mondi (o punti) e R è una relazione
tra elementi di W, cioè R ⊆ (WXW ) 2
De niamo ora i modelli relazionali ; le strutture (modelli) relazionali vengono
talvolta chiamati strutture (modelli) di Kripke.
De nizione 1.6 Un modello di Kripke è una tripla M = ⟨W R V ⟩ dove ⟨W R⟩ è
una struttura relazionale, mentre V è una funzione di interpretazione delle variabili
enunciative tale che V: varÐ→ PW
De nizione 1.7 La de nizione di verità in un mondo di un modello relazionale
(in simboli, ⊧Mw ) è per induzione:
(1) ⊧Mw p sse w ∈ V (p)
(2) ⊭Mw –
(3) ⊧Mw → sse ⊧Mw implica ⊧Mw
(4) ⊧Mw ◻ sse per ogni v ∈W , se wRv allora ⊧Mv
Segue quindi dalle de nizioni che
(5) ⊧Mw ¬ sse ⊭Mw
(6) ⊧Mw ∧ sse ⊭Mw e ⊧Mw
(7) ⊧Mw ∨ sse ⊭Mw oppure ⊧Mw
(8) ⊧Mw ◇ sse esiste un v ∈W tale che wRv e ⊧Mv
A partire dalla de nizione 1.7 è possibile de nire la validità in un modello rela-
zionale (simb. ⊧M ) , la validità in un mondo in una struttura (in simboli, ⊧Fw )
e la validità in una struttura (in simboli, ⊧F ).
De nizione 1.8 Sia F = (W R) una struttura relazionale e M = (F V ) un modello
relazionale basato su F. Allora
(1) ⊧M sse ⊧Mw per ogni w ∈W
(2) ⊧Fw sse ⊧
M
w per ogni M basato su F (cioè per ogni V )
2La relazione di accessibilità viene usualmente de nita intuitivamente dicendo che quando w1Rw2,
w1 vede w2, oppure che w2 è accessibile da w1.
10
1. Introduzione
(3) ⊧F  sse ⊧Fw per ogni w ∈W
Talvolta si scriverà ⟨M w⟩ ⊧ (risp. M ⊧ ) invece che ⊧Mw (risp. M ⊧
). Discorso analogo nel caso di validità in strutture. E conveniente estendere la
valutazione V da variabili proposizionali a formule. Scriveremo quindi V ( ) per
indicare l insieme di mondi in cui è vera, cioè
V ( ) = {w ∣ w ⊧ }
Si ha così immediatamente che, dato un mondo w e variabili proposizionali (pi)i∈I ∈
w ∈ V ( ) sse per ogni pi ∈ w ∈ V (pi)
Verranno inoltre rappresentate strutture di Kripke con diagrammi, tracciando
una freccia da w a v se wRv. Per comodità, verranno utilizzati due tipi di diagram-
mi, a seconda che sia utile mettere in luce la validità delle variabili nei singoli mondi,
oppure le relazioni tra i vari mondi. In generale non verranno tracciate freccie che
rappresentino ri essività e transitività quando ciò sarà evidente dalla de nizione
stessa di modello.
Esempio 1.9 Sia dato M = ⟨W R V ⟩ con W = {w v u}, R= {⟨w w⟩ ⟨w v⟩,
⟨v v⟩ ⟨v u⟩} e V(p)= {v}, V(q)={w v}. Questa situazione è rappresentata gra -
camente così:
ONMLHIJKpw
//
//
_^]\XYZ[p
q
v
bb
//
ONMLHIJKu
oppure più semplicemente
○w //○v //●u
dove i mondi ri essivi sono indicati dal segno ○.
Il seguente teorema mostra che la base assiomatica di qualsiasi sistema normale,
ossia il sistema K, è corretto
Teorema 1.10 K⊢ ⇒ F ⊧ , per ogni struttura F.
Dimostrazione. Poichè CL ⊂K, restano da dimostrare la validità di K e RN. Sia
M un modello arbitrario e w1 un mondo qualsiasi. Si supponga che ⊧w1 ◻( → )
e ⊧w1 ◻ . Allora ⊧w2 ( → ) e ⊧w2 per ogni w2 t.c. w1Rw2. Per la semantica di
→, ⊧w2 e quindi ⊧w1 ◻ . Quindi K è valido in ogni mondo di ogni struttura.
Per RN, se ⊢ , allora ∀i wi ⊧ . Questo signi ca che a fortiori si ha wi ⊧ , e
così RN conserva la validità ⊣
Elenchiamo qui i principali tipi di relazione (le condizioni su R) che verranno
utilizzati nel nostro lavoro:
11
1. Introduzione
1. Seriale: ∀w1∃w2w1Rw2
2. Ri essiva: ∀w wRw
3. Simmetrica: ∀w1 2 w1Rw2 → w2Rw1
4. Transitiva: ∀w1 2 3 w1Rw2 ∧w2Rw3 → w1Rw3
5. Euclidea: ∀w1 2 3 w1Rw2 ∧w1Rw3 → w2Rw3
E possibile ora enunciare due teoremi generali, che verranno dimostrati per ogni
caso particolare in seguito.
Teorema 1.11 Per ogni modello M con struttura F = ⟨W Rn⟩,
● Se R è seriale allora ⊧M D
● Se R è ri essiva allora ⊧M T
● Se R è simmetrica allora ⊧M B
● Se R è transitiva allora ⊧M 4
● Se R è euclidea allora ⊧M 5
Se si considerano strutture invece che modelli, la situazione cambia. In generale
vale un teorema più forte del teorema 1.11:
Teorema 1.12 Per ogni struttura F e la relazione R su essa,
● R è seriale se e solo se ⊧F D
● R è ri essiva se e solo se ⊧F T
● R è simmetrica se e solo se ⊧F B
● R è transitiva se e solo se ⊧F 4
● R è euclidea se e solo se ⊧F 5
In generale, per un numero molto vasto di assiomi è possibile trovare una
condizione su R per cui il teorema è soddisfatto.
Le seguenti proposizioni mostrano analiticamente la validità del teorema 1.12
Proposizione 1.13 F ⊧D↔ RF è seriale.
Dimostrazione. (⇒) Se R non è seriale, allora ∀w1∄w2(w1Rw2). Sia V(p)=
(w1). Allora ⊧w1 ◻p e ⊭w1 ◇p, quindi ⊭w1 ◻p→◇p.
(⇐) Sia ⊧w1 ◻ e ⊭w1 ◇ . Allora chiaramente w1 è un punto terminale, quindi
∀w1∄w2(w1Rw2) è condizione necessaria a nchè F ⊭ ◻ → ◇ ; ciò dimostra che
∀w1∃w2 w1Rw2 è condizione su ciente a nchè valga F ⊧ ◻ →◇ con RF seriale.
⊣
Proposizione 1.14 F ⊧ T ↔ RF è ri essiva.
Dimostrazione. (⇒) Il procedimento è analogo a quello precedente. Sia R non
ri essiva, cioè ∄w wRw, e V(p)= w per tutti i w ∈W −w1. Allora ⊧w1 ◻p e ⊭w1 p,
quindi ⊭w1 ◻p→ p.
(⇐)Se F ⊭ ◻ → , allora esiste un w1 tale che ⊧w1 ◻ e ⊭w1 . Dato che
w1Rw1, si avrebbero rispettivamente ⊭w1 ◻ e ⊧w1 , il che è contraddittorio con
quanto appena mostrato. ⊣
12
1. Introduzione
Proposizione 1.15 F ⊧ B ↔ RF è simmetrica.
Dimostrazione. (⇒) Se R non è simmetrica allora ∃w1w2(w1Rw2)∧¬(w2Rw1).
Sia V(p) = (w1). Allora ⊧w1 p, ⊭w1 ◇p e ⊭w1 ◻◇ p; quindi ⊭w1 p→ ◻◇ p.
(⇐) Sia ⊧w1 e ⊭w1 ◻◇ . Allora ∃w2(w1Rw2) in cui ⊭w1 ◇ , quindi w2 ∉ w1 ↓.
Ne deriva che ∃w1 w2(w1Rw2)∧¬(w2Rw1) è condizione necessaria a nchè F ⊭ →
◻◇ , e quindi la simmetria di R è condizione su ciente a nchè F ⊧ → ◻◇ . ⊣
Proposizione 1.16 F ⊧ 4↔ RF è transitiva.
Dimostrazione. (⇒) Se R non è transitiva allora ∀w1 2 3(w1Rw2 ∧ w2Rw3 ∧
¬(w1Rw3). Sia V(p) =(w1 w2). Allora ⊧w1 ◻p, ⊭w2 ◻p e quindi ⊭w1 ◻ ◻ p. Quindi
⊭w1 4
(⇐)Sia ⊧w1 ◻ e ⊭w1 ◻◻ . Allora esiste un w2 tale che w1Rw2 e ⊧w2 , ⊭w2 ◻ .
Ne segue che esiste un w3 tale che w2Rw3 e ⊭w3 . Ma allora ¬(w1Rw3), altrimenti si
avrebbe ⊭w1 ◻p. Quindi ∀w1 2 3(w1Rw2∧w2Rw3∧¬(w1Rw3) è condizione necessaria
a nchè F ⊭ ◻ → ◻ ◻ . R transitiva è dunque condizione su ciente a chè F ⊧
◻ → ◻ ◻ . ⊣
Proposizione 1.17 F ⊧ 5↔ RF è euclidea.
Dimostrazione. (⇒) Se R non è euclidea allora ∀w1 2 3(w1Rw2 ∧ w1Rw3 ∧
¬(w2Rw3 ∧ ¬(w3Rw2). Sia V (p) = w1 2 3. Allora ⊭w2 3 ◻p ma ⊧w1 ◇p e ⊭w1 ◻◇ p.
Quindi ⊭w1 5.
(⇐) Sia ⊧w1 ◇ e ⊭w1 ◻◇ . Allora esiste un w2 in relazione con w1 tale che
⊧w2 e per ogni wn tale che w1Rwn,⊭wn ◇ . Allora chiaramente non si dà wnRw2,
altrimenti ◇ sarebbe valido in wn, nè w2Rwn, altrimenti si avrebbe ⊭w2 ◻¬ e
quindi ⊭w1 ¬ , contrariamente all ipotesi. Quindi condizione necessaria a nchè
F ⊭ ◇ → ◻◇ è che, intuitivamente, dato un mondo w1 e mondi wn in relazione
con esso, esista almeno un w2 ∈Wn che non sia in relazione con i restanti w ∈Wn.
Ne segue che R euclidea è condizione su ciente perchè valga F ⊧ 5. ⊣
Questo conclude la dimostrazione dei teorema 1.12.
Il teorema 1.11 è la direzione (⇒) del teorema 1.12, per cui la precedente di-
mostrazione vale anche per un verso del teorema 1.12. L altro verso però non va-
le se ci limitiamo ai modelli: il motivo di tale indebolimento è chiaramente dato
dalla valutazione V che appunto fa parte del modello. E infatti semplice mo-
strare, ad esempio, un modello non transitivo in cui comunque valga ⊧M 4. Sia
infatti M con W = ⟨w1 w2 w3⟩, R = {⟨w1w2⟩ ⟨w2w3⟩ ⟨wnwn⟩} per n= 1, 2, 3 e
V (p) = ⟨w1 w2 w3⟩. Si noti che R è ri essiva ma non transitiva. Allora si ha
⊧w1 2 3 ◻p e ⊧w1 2 3 ◻ ◻ p e quindi ⊧w1 2 3 ◻p→ ◻ ◻ p.
I seguenti semplici modelli mostrano che è possibile esibire un modello di Kripke
che falsi chino esempi di D, T, B, 4, 5. per D: W = {w1}, R = ø e V(p, q) = ø
per T: W = {w1 w2}, R = {w1w2} e V(p) = {w2}
per B: W = {w1 w2}, R = {w1w2} e V(p) = {w1 w2}
13
1. Introduzione
per 4: W = {w1w2 w3}, R = {⟨w1w2⟩ ⟨w2w3⟩} e V(p) = {w2}
per 5: W = {w1 w2 w3}, R = {⟨w1w2⟩ ⟨w1w3⟩} e V(p) = {w1 w2}
La veri ca è immediata. Per D, basta notare che in un mondo terminale ◻ è
sempre valida mentre ◇ non lo è.
Il concetto di validità generale in una struttura, alla luce del teorema 1.11, ci
permetterà di dare una caratterizzazione semantica di alcune delle principali logiche
modali normali a cominciare da quelle cui si è accennato in precedenza. Infatti si è
visto che ogni formula di K è valida in qualsiasi struttura, ogni formula di KD in
qualsiasi struttura seriale, etc. Possiamo quindi identi care una logica con l insieme
delle formule valide in una determinata classe di strutture, classe che deve appunto
soddisfare i requisiti su R imposti proprio dal teorema 1.11. I risultati di completez-
za che esporremo (per una classe di strutture più ampia di quelle n qui studiate)
permetteranno di far coincidere la caratterizzazione semantica di un sistema sopra
esposta con quella data nella de nizione 1.3. In questo modo otterremo che ogni
teorema di K è valido in ogni struttura (validità) e che, viceversa, ogni formula
valida in ogni struttura è un teorema di K: la de nizione di logica come insieme di
teoremi e quella di logica come insieme di formule valide (sotto opportuni requisiti
su R) vengono a coincidere. Avremo così
K = { ∈ FormML ∣ F ⊧ per ogni struttura F}
KD = { ∈ FormML ∣ F ⊧ per ogni struttura seriale }
KT = { ∈ FormML ∣ F ⊧ per ogni struttura ri essiva}
KTB = { ∈ FormML ∣ F ⊧ per ogni struttura ri essiva e simmetrica}
KT4 = { ∈ FormML ∣ F ⊧ per ogni struttura ri essiva e transitiva}
KT5 = { ∈ FormML ∣ F ⊧ per ogni struttura ri essiva, simmetrica e transitiva}
Come detto, la dimostrazione di completezza verrà data per una classe particolare
di strutture. Invece che lavorare sui singoli schemi di assiomi, infatti, talvolta è
conveniente cercare di pervenire a risultati più generali entro cui si possono ritrovare
tutti i sistemi n qui trattati.
Prima di tutto è necessario dare alcune de nizioni preliminari. Date le de ni-
zioni di verità di ◻ e ◇ è possibile generalizzare a partire dalla relazione Rn così
de nita:
w1R0w2 sse w1 = w2
w1Rnw2 sse (∃w3) tale che w1Rn−1w3 ∧w3Rw2
E possibile estendere quindi la de nizione di verità in caso di operatori ◻n e
◇n:
De nizione 1.18 In un modello di Kripke ⟨W R V ⟩ come precedentemente de nito
valgono:
⊧Mw1 ◻n sse per ogni w2 ∈W se w1Rnw2 allora ⊧Mw2
14
1. Introduzione
⊧Mw1 ◇n sse esiste un w2 ∈W tale che w1Rnw2 e ⊧Mw2
Dimostrazione. La dimostrazione è per induzione su n. Il caso n = 0 è ovvio. Si
supponga che valga per n − 1: si dimostra che vale per n. Allora
⊧w1 ◻
n sse ⊧w1 ◻ ◻
n−1
sse ∀w2(w1Rw2 →⊧w1 ◻n−1 (per la semantica di ◻)
sse ∀w2(w1Rw2 → (∀w3)(w2Rn−1w3 →⊧w3 ))
sse ∀w3∃w2((w1Rw2 ∧w2Rn−1w3)→⊧w3 )
sse ∀w3(w1Rnw3 →⊧w3 )
La dimostrazione nel caso di ◇n è analoga. ⊣
Sia ora:
(G′) ◇k ◻l → ◻m◇n
con k l m n ≥ 0. E immediato veri care che K, T, D, B, 4 e 5 sono casi
particolari di G . Tanto per fare un esempio, T si ottiene da G con (k, m, n) = 0 e
(l) = 1; D con (k, m) = 0 e (l, n) = 1; 5 con (k, m, n) = 1 e l =0; e così via.
La condizione su R non ha, che sappia, una denominazione precisa: potrebbe
essere chiamata k-l-m-n convergenza, ed essere espressa così:
(R′) ∀w1 w2 w3(w1Rkw2 ∧w1Rmw3 → ∃w4(w2Rlw4 ∧w3Rnw4))
Ancora, da R seguono tutte le condizioni caratteristiche su R: ri essività,
transitività, simmetria, ecc.
La validità è data dal seguente teorema:
Teorema 1.19 F = ⟨W R′⟩↔⊧F G′
Dimostrazione. (⇒) Si supponga che esista un modello M tale che M ⊭ ◇k ◻l
→ ◻m◇n . Allora per qualche mondo w1 si ha ⊭ww ◻n◇n e ⊧w1 ◇k ◻l . Deve
quindi esistere un mondo w2 tale che w1Rw2 e ⊧w1 ◻l ; e un mondo w3 tale che
w1Rw3 e ⊭w3 ◇n . Poiche però il modello soddisfa R , deve esserici un w4 tale che
w2Rlw4 e w3Rnw4. Questo signi ca tuttavia che valgono sia ⊧w4 (poichè ⊧w2 ◻l )
che ⊭w4 (poichè ⊭w3 ◇n ). Assurdo, quindi M ⊧◇k ◻l → ◻m◇n .
(⇐) Si neghi R′. Allora per ogni w1 w2 w3 w4 tali che w1Rkw2 ∧ w1Rmw3, o
¬(w2Rlw4) o ¬(w3Rnw4). Si costruisce quindi un modello sulla negazione di R′.
Sia W = (w1 2 3 4 5), R come de nita e V( ) = {w5∣w2Rlw5}. Allora si ha ⊧w2 ◻l
e (dato che non si dà w3Rw4), ⊭w3 ◇n , quindi ⊧w1 ◇k ◻l e ⊭w1 ◻m◇n . Quindi
⊭w1 G′. ⊣
Dalla validità di KG′ segue naturalmente la validità di tutti i sistemi costruiti da K
per aggiunta di assiomi di cui G′ e proprio una generalizzazione. Analogo discorso
vale per la completezza: invece che dimostrare la completezza di KD, KT, KT4,
ecc, sarà su ciente una dimostrazione di completezza generalizzata per KG′ che a
fortiori varrà per tutti i sistemi n qui presentati.
15
1. Introduzione
3. Dimostrazioni di completezza
Si consideri una logica normale S ⊇ K. Dato un qualunque insieme  ⊆ S,
diremo che  è S-coerente se e solo se esiste almeno una formula  non S-derivabile
da  , cioè tale per cui dati 1 n ∈  non si ha ( 1 n)→ ∈ S.
Un insieme di formule  di dice S-coerente massimale se e solo se è S-coerente e
non esiste un insieme S-coerente tale che ⊃  . In altre parole,  non può essere
esteso mantenendo la coerenza.
Diremo inoltre che una logica S è completa se, per ogni formula , si ha
⊧S ⇒⊢S
Il seguente teorema mostra che ogni insieme S-coerente può essere esteso ad un
insieme S-coerente massimale.
Lemma 1.20 (Lindenbaum) Se L è numerabile e  è S-coerente, allora esiste un
 ∗ S-coerente e massimale tale che  ⊆  ∗.
Dimostrazione. Si è supposto L numerabile, quindi è possiile disporre le formule
del linguaggio in una successione. Si de nisce quindi per recursione una successione
di insiemi { i}i∈ ponendo:
 0 =  e  i+1 =
⎧⎪⎪
⎨
⎪⎪⎩
 i ∪ { } se  i ∪ { } è coerente
 i altrimenti
Si noti che la successione è una catena. Poniamo quindi  ∗ = ⋃ { i}. Allora
per induzione su si vede che ogni  i è coerente. Occorre dimostrare che anche
 ∗ lo è. Si procede per assurdo: supponiamo che esista una formula tale che
 ∗ ⊢ e  ∗ ⊢ ¬ . Poiche  ∗ è dato dall unione di (eventualmente in niti)  i, allora
esistono 0 ⊆  e 1 ⊆  , entrambi niti, tali che 0 ⊢ e 1 ⊢ ¬ . Ne consegue
che anche = 0 ∪ 1 ⊆  ∗, quindi ⊢ e ⊢ ¬ . Essendo  ∗ una catena e
0 1 ⊆  ∗, esiste un  i tale che 0 1 ⊆  i e quindi per monotonia otteniamo
 i ⊢ e  i ⊢ ¬ , il che rende  i incoerente, contrariamente all ipotesi. Resta da
dimostrare la massimalità di  ∗. Supponiamo che esista un coerente e massimale,
tale quindi che  ∗ ⊂ . Dato ∈ −  ∗, per qualche i dovremo avere = i e
 i ∪ { i} incoerente, altrimenti sarebbe i ∈  ∗. Ma  i ∪ { i} ∈ , quindi anche
sarebbe incoerente, contrariamente all ipotesi. ⊣
Il seguente teorema enuncia alcune proprietà degli insiemi coerenti massimali.
Teorema 1.21 Sia  un insieme di formule S-coerente massimale. Allora valgono:
a)  ⊢ ⇔ ∈  ;
b) ∈  ⇔ ¬ ∉  ;
c) ∧ ∈  ⇔ ∈  e ∈  
Dimostrazione. (a)Se ∈  , allora c è una derivazione 1 n ⊢ . Ma poichè
1 n ∈  , anche ∈  . Viceversa, sia  ⊢ , e si supponga ∉  . Allora per
16