# Correttezza (logica matematica)

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 $\Gamma$ di formule ben formate (fbf), e per ogni fbf $\alpha$, se esiste una dimostrazione di $\alpha$ il cui insieme di assunzioni "non scaricabili" è contenuto in $\Gamma$, allora $\alpha$ è una conseguenza logica di $\Gamma$, in simboli $\Gamma \vdash \alpha \implies \Gamma \vDash \alpha$.

### Dimostrazione

Dalla definizione di $\Gamma \vdash \alpha$, è sufficiente provare che, per ogni derivazione ${\mathcal {D}}$, vale $\Gamma \vdash _{\mathcal {D}}\alpha \implies \Gamma \vDash \alpha$, dove $\Gamma \vdash _{\mathcal {D}}\alpha$ significa che ${\mathcal {D}}$ è una dimostrazione di $\alpha$ da $\Gamma$. Si procederà per induzione sulle derivazioni ${\mathcal {D}}$ di $\alpha$ da $\Gamma$.
* ${\mathcal {D}}$ è una derivazione atomica, cioè $\alpha$ è una dimostrazione di $\alpha$ da $\Gamma$. In altre parole, $\alpha \in \Gamma$. A fortiori, $\Gamma \vDash \alpha$.
* ${\mathcal {D}}$ è una derivazione della forma ${\frac {\Gamma '\vdash _{{\mathcal {D}}_{1}}\gamma \;\;\;\;\;\;\;\Gamma ''\vdash _{{\mathcal {D}}_{2}}\delta }{\gamma \land \delta }}$, dove $\gamma \land \delta =:\alpha$. Siano $\Gamma '$ e $\Gamma ''$ le assunzioni utilizzate in ${\mathcal {D}}_{1}$ e in ${\mathcal {D}}_{2}$ rispettivamente. Allora $\Gamma '\cup \Gamma '\subseteq \Gamma$. Dal primo ramo della derivazione ${\mathcal {D}}$, si ha $\Gamma '\vdash _{{\mathcal {D}}_{1}}\alpha$, da cui, per ipotesi induttiva, segue $\Gamma '\vDash \gamma$. Allo stesso modo $\Gamma '\vDash \delta$. In conclusione, essendo $\Gamma '\cup \Gamma '\subseteq \Gamma$, segue $\Gamma \vDash \gamma$ e $\Gamma \vDash \delta$, da cui $\Gamma \vDash \gamma \land \delta =\alpha$.
* ${\mathcal {D}}$ è una derivazione della forma ${\frac {\Gamma ,[\neg \alpha ]\vdash _{\mathcal {D_{1}}}\bot }{\alpha }}$. Per ipotesi induttiva, segue $\Gamma ,\neg \alpha \vDash \bot$. In altre parole, per ogni valutazione $\nu$, si ha
       $\nu (\Gamma \cup \{\neg \alpha \})=1\implies \nu (\bot )=1.$
    Dal fatto che $\nu (\bot )=0$, segue che $\nu (\Gamma \cup \{\neg \alpha \})=0$, per ogni valutazione $\nu$. Questo significa che, ogni qual volta $\nu (\Gamma )=1$, si ha $\nu (\neg \alpha )=0$, cioè $\nu (\alpha )=1$. Quindi $\Gamma \vDash \alpha$.
* ${\mathcal {D}}$ è una derivazione della forma ${\frac {\Gamma \vdash _{{\mathcal {D}}_{2}}\gamma \lor \delta \;\;\;\;\;\;\;\Gamma ,[\gamma ]\vdash _{{\mathcal {D}}_{2}}\alpha \;\;\;\;\;\;\;\Gamma ,[\delta ]\vdash _{{\mathcal {D}}_{3}}\alpha }{\alpha }}$. Per ipotesi induttiva, segue $\Gamma \vDash \gamma \lor \delta$. Similmente, si ottiene $\Gamma ,\gamma \vDash \alpha$ e $\Gamma ,\delta \vDash \alpha$. Sia $\nu$ una valutazione tale che $\nu (\Gamma )=1$. Allora $\nu (\gamma \lor \delta )=1$, ovvero $\nu (\gamma )=1$ o $\nu (\delta )=1$. Se $\nu (\gamma )=1$, e dal fatto che $\Gamma ,\gamma \vDash \alpha$, segue $\nu (\alpha )=1$. Analogamente, se $\nu (\delta )=1$, e dal fatto che $\Gamma ,\delta \vDash \alpha$, segue $\nu (\alpha )=1$. In conclusione, $\Gamma \vDash \alpha$.
Gli altri casi seguono analogamente a quanto dimostrato finora.