Le leggi modali minimali
Le leggi modali minimali
Lug 03[ad#Ret Big]
Rieccoci di nuovo qui a parlare di logica modale. Nell’ultimo post avevamo lasciato in sospeso
come mai nei dead end tutte le formule boxate sono vere e tutte quelle ◊-ate sono invece false.
La motivazione risiede nel fatto che, come abbiamo detto, i dead end sono mondi che non vedono
nessun altro, neanche se stessi, ossia:
¬∃ j∈W (iRj)
Di conseguenza della nota definizione di forzatura di una formula con box
i╞ □α sse ∀ j∈W (iRj → j╞ α)
segue che la relazione di accessibilità non vale, perciò l’antecedente dell’implicazione è falso quindi
per le tavole di verità l’implicazione è banalmente vera.
Stesso discorso per il diamond, con la differenza però che la sua definizione è una congiunzione
che per essere vera richiede che entrambi i congiunti siano veri, perciò essendo falso il primo,
segue che tutta la congiunzione è falsa.
i╞ ◊α sse ∃ j∈W (iRj ˄ j╞ α)
Ora che abbiamo chiuso questa parentesi possiamo definire due differenti nozioni:
i ╞ α (verità a un mondo)
Ϻ ╞ α (α è vera nel modello Ϻ, ossia è vera in tutti i mondi di Ϻ)
K ╞ α sse Ϻ ╞ α (α è vera in tutti i modelli di Kripke, ossia α è una legge logica minimale)
Come si fa a verificare se una formula è una legge logica?
Più avanti introdurremo un metodo finitario di decisione effettivo per la nozione di legge logica, ma per adesso possiamo procedere intuitivamente come segue.
Prendiamo come esempio la legge K (la distributività del □ sull’implica) che è l’assioma caratteristico di K quindi sappiamo già essere una legge logica. Di conseguenza dimostrando per
assurdo che non lo sia, questo porterà ad una contraddizione. Entriamo meglio nei dettagli.
Vogliamo verificare che K ╞ □(α →β) → (□ α →□β)
Procediamo per assurdo e supponiamo che cosi’ non sia. Quindi che esista un modello
Ϻ =〈W, R, v 〉tale che
i ╡□(α →β) → (□ α →□β)
[Nota: per comodità convenzionale useremo ╡per indicare la nozione di non-forzatura (i ╡ α = i
non forza α).]
Allora avremo per forza che:
(1) i╞ □(α →β) ; (2) i ╡(□ α →□β)
Da (2) segue che:
(3) i╞ □ α ; (4) i ╡□β
Da (4) segue che:
∃ j (iRj ˄ j ╡β)
Ma da (1) e (3) segue che per sia α →β che α devono essere vere a ogni mondo che i vede e
siccome il mondo j è tra questo avremo che:
j╞ α & j╞ α →β
Perciò per definizione di forzatura di una implicazione segue che j╞ β. Quindi β è vera e falsa a j.
Contraddizione.
Articolo precedente: Logica modale. Verità di una formula
Articolo successivo: Teorema di correttezza in K
