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

Dimostrazione

Dalla definizione di ${\displaystyle \Gamma \vdash \alpha }$, è sufficiente provare che, per ogni derivazione ${\displaystyle {\mathcal {D}}}$, vale ${\displaystyle \Gamma \vdash _{\mathcal {D}}\alpha \implies \Gamma \vDash \alpha }$, dove ${\displaystyle \Gamma \vdash _{\mathcal {D}}\alpha }$ significa che ${\displaystyle {\mathcal {D}}}$ è una dimostrazione di ${\displaystyle \alpha }$ da ${\displaystyle \Gamma }$. Si procederà per induzione sulle derivazioni ${\displaystyle {\mathcal {D}}}$ di ${\displaystyle \alpha }$ da ${\displaystyle \Gamma }$.

• ${\displaystyle {\mathcal {D}}}$ è una derivazione atomica, cioè ${\displaystyle \alpha }$ è una dimostrazione di ${\displaystyle \alpha }$ da ${\displaystyle \Gamma }$. In altre parole, ${\displaystyle \alpha \in \Gamma }$. A fortiori, ${\displaystyle \Gamma \vDash \alpha }$.
• ${\displaystyle {\mathcal {D}}}$ è una derivazione della forma ${\displaystyle {\frac {\Gamma '\vdash _{{\mathcal {D}}_{1}}\gamma \;\;\;\;\;\;\;\Gamma ''\vdash _{{\mathcal {D}}_{2}}\delta }{\gamma \land \delta }}}$, dove ${\displaystyle \gamma \land \delta =:\alpha }$. Siano ${\displaystyle \Gamma '}$ e ${\displaystyle \Gamma ''}$ le assunzioni utilizzate in ${\displaystyle {\mathcal {D}}_{1}}$ e in ${\displaystyle {\mathcal {D}}_{2}}$ rispettivamente. Allora ${\displaystyle \Gamma '\cup \Gamma '\subseteq \Gamma }$. Dal primo ramo della derivazione ${\displaystyle {\mathcal {D}}}$, si ha ${\displaystyle \Gamma '\vdash _{{\mathcal {D}}_{1}}\alpha }$, da cui, per ipotesi induttiva, segue ${\displaystyle \Gamma '\vDash \gamma }$. Allo stesso modo ${\displaystyle \Gamma '\vDash \delta }$. In conclusione, essendo ${\displaystyle \Gamma '\cup \Gamma '\subseteq \Gamma }$, segue ${\displaystyle \Gamma \vDash \gamma }$ e ${\displaystyle \Gamma \vDash \delta }$, da cui ${\displaystyle \Gamma \vDash \gamma \land \delta =\alpha }$.
• ${\displaystyle {\mathcal {D}}}$ è una derivazione della forma ${\displaystyle {\frac {\Gamma ,[\neg \alpha ]\vdash _{\mathcal {D_{1}}}\bot }{\alpha }}}$. Per ipotesi induttiva, segue ${\displaystyle \Gamma ,\neg \alpha \vDash \bot }$. In altre parole, per ogni valutazione ${\displaystyle \nu }$, si ha

${\displaystyle \nu (\Gamma \cup \{\neg \alpha \})=1\implies \nu (\bot )=1.}$

Dal fatto che ${\displaystyle \nu (\bot )=0}$, segue che ${\displaystyle \nu (\Gamma \cup \{\neg \alpha \})=0}$, per ogni valutazione ${\displaystyle \nu }$. Questo significa che, ogni qual volta ${\displaystyle \nu (\Gamma )=1}$, si ha ${\displaystyle \nu (\neg \alpha )=0}$, cioè ${\displaystyle \nu (\alpha )=1}$. Quindi ${\displaystyle \Gamma \vDash \alpha }$.

• ${\displaystyle {\mathcal {D}}}$ è una derivazione della forma ${\displaystyle {\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 ${\displaystyle \Gamma \vDash \gamma \lor \delta }$. Similmente, si ottiene ${\displaystyle \Gamma ,\gamma \vDash \alpha }$ e ${\displaystyle \Gamma ,\delta \vDash \alpha }$. Sia ${\displaystyle \nu }$ una valutazione tale che ${\displaystyle \nu (\Gamma )=1}$. Allora ${\displaystyle \nu (\gamma \lor \delta )=1}$, ovvero ${\displaystyle \nu (\gamma )=1}$ o ${\displaystyle \nu (\delta )=1}$. Se ${\displaystyle \nu (\gamma )=1}$, e dal fatto che ${\displaystyle \Gamma ,\gamma \vDash \alpha }$, segue ${\displaystyle \nu (\alpha )=1}$. Analogamente, se ${\displaystyle \nu (\delta )=1}$, e dal fatto che ${\displaystyle \Gamma ,\delta \vDash \alpha }$, segue ${\displaystyle \nu (\alpha )=1}$. In conclusione, ${\displaystyle \Gamma \vDash \alpha }$.

Gli altri casi seguono analogamente a quanto dimostrato finora.

Voci correlate

• Logica proposizionale
• Teoria del primo ordine
• Consistenza (logica matematica)
• Validità (logica)

Collegamenti esterni

• (EN) soundness, su Enciclopedia Britannica, Encyclopædia Britannica, Inc.
• Validity and Soundness, su Internet Encyclopedia of Philosophy. URL consultato il 22 maggio 2019 (archiviato dall'url originale il 27 maggio 2018).