Correttezza (logica matematica)
![Niente fonti!](http://upload.wikimedia.org/wikipedia/commons/thumb/6/64/Question_book-4.svg/45px-Question_book-4.svg.png)
In logica matematica, la correttezza o validità (in inglese soundness) è una proprietà fondamentale delle regole logiche e dei calcoli logici.
Una regola logica (o regola di inferenza o regola di derivazione) è corretta se la conclusione è conseguenza logica delle (ossia, segue necessariamente dalle) premesse: se sono vere tutte le premesse allora è necessariamente vera la conclusione (o equivalentemente, non è possibile che le premesse siano tutte vere e la conclusione falsa). Ciò significa che, lette dall'alto verso il basso (dalle premesse alla conclusione), le regole logiche corrette preservano la verità, o equivalentemente, lette dal basso verso l'alto (dalla conclusione alle premesse) le regole logiche corrette preservano la falsità (se la conclusione è falsa, allora è necessariamente falsa almeno una delle premesse).
Un calcolo logico (ad esempio il calcolo dei sequenti o la deduzione naturale) è corretto in senso debole se ogni formula A derivabile in esso è valida, ossia se ogni formula A dimostrabile applicando un numero finito di volte le regole di derivazione del calcolo logico è vera per ogni modello. Un calcolo logico è corretto in senso forte se ogni formula A derivabile in esso a partire da un insieme di formule chiuse X (che fungono da assiomi di una teoria) è conseguenza logica di X. È evidente che la correttezza forte implica la correttezza debole: basta prendere per X un insieme vuoto di formule.
La correttezza è (assieme alla completezza semantica) un requisito essenziale di ogni calcolo logico, pertanto ciascuno di questi presenta un teorema di correttezza (debole o forte) che esprime appunto il fatto che tale calcolo logico è corretto (in senso debole o forte). Il teorema di correttezza debole (risp. forte) è il viceversa del teorema di completezza semantica debole (risp. forte).
Detto in modo intuitivo, un calcolo logico in quanto corretto è in grado di dimostrare solo le verità di una teoria, mentre in quanto completo (semanticamente) è in grado di dimostrare tutte le verità di una teoria.
Teorema di correttezza
Il teorema di correttezza (o soundness theorem) afferma che, per ogni insieme di formule ben formate (fbf), e per ogni fbf , se esiste una dimostrazione di il cui insieme di assunzioni "non scaricabili" è contenuto in , allora è una conseguenza logica di , in simboli .
Dimostrazione
Dalla definizione di , è sufficiente provare che, per ogni derivazione , vale , dove significa che è una dimostrazione di da . Si procederà per induzione sulle derivazioni di da .
- è una derivazione atomica, cioè è una dimostrazione di da . In altre parole, . A fortiori, .
- è una derivazione della forma , dove . Siano e le assunzioni utilizzate in e in rispettivamente. Allora . Dal primo ramo della derivazione , si ha , da cui, per ipotesi induttiva, segue . Allo stesso modo . In conclusione, essendo , segue e , da cui .
- è una derivazione della forma . Per ipotesi induttiva, segue . In altre parole, per ogni valutazione , si ha
- Dal fatto che , segue che , per ogni valutazione . Questo significa che, ogni qual volta , si ha , cioè . Quindi .
- è una derivazione della forma . Per ipotesi induttiva, segue . Similmente, si ottiene e . Sia una valutazione tale che . Allora , ovvero o . Se , e dal fatto che , segue . Analogamente, se , e dal fatto che , segue . In conclusione, .
Gli altri casi seguono analogamente a quanto dimostrato finora.
Voci correlate
- Logica proposizionale
- Teoria del primo ordine
- Consistenza (logica matematica)
- Validità (logica)
Collegamenti esterni
- Validity and Soundness, su Internet Encyclopedia of Philosophy. URL consultato il 22 maggio 2019 (archiviato dall'url originale il 27 maggio 2018).