Teorema di correttezza in K
Teorema di correttezza in K
Lug 17[ad#Ret Big]
Dall’ultimo post sulle leggi modali minimali abbiamo in qualche modo avuto gratis la dimostrazione del teorema di correttezza in K. Il teorema di correttezza dice che se una formula è dimostrabile allora è vera.
In simboli:
Se ├ α allora ╞ α
Si dimostra per induzione sulla lunghezza della dimostrazione. Il primo passo è supporre che la lunghezza della dimostrazione sia pari a 1. Se è così allora vuol dire che la formula in questione è un assioma.
Bisognerebbe dimostrare quindi che tutti gli assiomi sono veri in K. Ma noi sappiamo che K verifica tutte le tautologie, perché come abbiamo già detto in passato le formule con connettivi sono verofunzionali, quindi se una formula è tautologica allora automaticamente è anche una legge K.
A questo punto occorrerebbe dimostrare gli assiomi caratteristici di K dato che K è un’estensione assiomatica della logica classica. Ma l’unico assioma caratteristico è la legge K, cioè la distributività del box sull’implica, e abbiamo dimostrato essere una verità logica nel post precedente, quindi almeno su quello siamo a posto.
Ora, sotto l’ipotesi che il teorema di correttezza valga per tutte le formule con lunghezza di dimostrazione ˂ n, dimostriamo che vale per tutte le formule con lunghezza di dimostrazione pari a n.
Se la lunghezza della dimostrazione è pari a n vuol dire che sarà stata applicata una regola di inferenza agli assiomi, quindi in sostanza è sufficiente dimostrare che le regole di inferenza preservano la verità degli assiomi.
Di regole di inferenza noi ne abbiamo solo due: la regola di necessitazione (da ora in poi RN) e il modus ponens (MP).
Dimostriamo che la RN preserva la verità degli assiomi.
Se ╞ α allora ╞ □ α
Supponiamo che ╞ α e che ci sia un modello tale che Ϻ╞ α. Se Ϻ╞ α allora vuol dire che α è vera in tutti i mondi del modello. Quindi, considerando i un mondo arbitrario del modello, allora segue che i╞ α. Se α è vera in tutti i mondi del modello Ϻ allora vuol dire che è vera anche in tutti i mondi accessibili a i, e siccome j è tra questi allora segue che i╞ □ α. Dato che i e j erano mondi arbitrari allora segue che Ϻ╞ □ α e inoltre considerato che Ϻ era un modello arbitrario allora si conclude che ╞ □ α.
Adesso dimostriamo che il MP preserva la verità degli assiomi.
Se ╞ α e ╞ α →β
allora ╞ β
Supponiamo che ╞ α e ╞ α →β e che ci sia un modello tale che Ϻ╞ α e che Ϻ╞ α →β. Ϻ╞ α →β = Ϻ╞ ¬ α ˅ β, ma per ipotesi vale che Ϻ╞ α quindi Ϻ╞ β. E dato che Ϻ era un modello arbitrario segue che╞ β.
Articolo precedente: Le leggi modali minimali