Correttezza (logica matematica)

Template:F 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 $\mathrm{\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 $\mathrm{\Gamma }$, allora $\alpha$ è una conseguenza logica di $\mathrm{\Gamma }$, in simboli $\mathrm{\Gamma }⊢\alpha ⟹\mathrm{\Gamma }\models \alpha$.

Dimostrazione

Dalla definizione di $\mathrm{\Gamma }⊢\alpha$, è sufficiente provare che, per ogni derivazione $𝒟$, vale $\mathrm{\Gamma }{⊢}_{𝒟}\alpha ⟹\mathrm{\Gamma }\models \alpha$, dove $\mathrm{\Gamma }{⊢}_{𝒟}\alpha$ significa che $𝒟$ è una dimostrazione di $\alpha$ da $\mathrm{\Gamma }$. Si procederà per induzione sulle derivazioni $𝒟$ di $\alpha$ da $\mathrm{\Gamma }$.

• $𝒟$ è una derivazione atomica, cioè $\alpha$ è una dimostrazione di $\alpha$ da $\mathrm{\Gamma }$. In altre parole, $\alpha \in \mathrm{\Gamma }$. A fortiori, $\mathrm{\Gamma }\models \alpha$.
• $𝒟$ è una derivazione della forma $\frac{{\mathrm{\Gamma }}^{\prime }{⊢}_{{𝒟}_1}\gamma {\mathrm{\Gamma }}^{″}{⊢}_{{𝒟}_2}\delta }{\gamma \wedge \delta }$, dove $\gamma \wedge \delta =:\alpha$. Siano ${\mathrm{\Gamma }}^{\prime }$ e ${\mathrm{\Gamma }}^{″}$ le assunzioni utilizzate in ${𝒟}_1$ e in ${𝒟}_2$ rispettivamente. Allora ${\mathrm{\Gamma }}^{\prime }\cup {\mathrm{\Gamma }}^{\prime }\subseteq \mathrm{\Gamma }$. Dal primo ramo della derivazione $𝒟$, si ha ${\mathrm{\Gamma }}^{\prime }{⊢}_{{𝒟}_1}\alpha$, da cui, per ipotesi induttiva, segue ${\mathrm{\Gamma }}^{\prime }\models \gamma$. Allo stesso modo ${\mathrm{\Gamma }}^{\prime }\models \delta$. In conclusione, essendo ${\mathrm{\Gamma }}^{\prime }\cup {\mathrm{\Gamma }}^{\prime }\subseteq \mathrm{\Gamma }$, segue $\mathrm{\Gamma }\models \gamma$ e $\mathrm{\Gamma }\models \delta$, da cui $\mathrm{\Gamma }\models \gamma \wedge \delta =\alpha$.
• $𝒟$ è una derivazione della forma $\frac{\mathrm{\Gamma },[\mathrm{\neg }\alpha ]{⊢}_{{𝒟}_1}\mathrm{\perp }}{\alpha }$. Per ipotesi induttiva, segue $\mathrm{\Gamma },\mathrm{\neg }\alpha \models \mathrm{\perp }$. In altre parole, per ogni valutazione $\nu$, si ha

$\nu (\mathrm{\Gamma }\cup \{\mathrm{\neg }\alpha \})=1⟹\nu (\mathrm{\perp })=1.$

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

• $𝒟$ è una derivazione della forma $\frac{\mathrm{\Gamma }{⊢}_{{𝒟}_2}\gamma \vee \delta \mathrm{\Gamma },[\gamma ]{⊢}_{{𝒟}_2}\alpha \mathrm{\Gamma },[\delta ]{⊢}_{{𝒟}_3}\alpha }{\alpha }$. Per ipotesi induttiva, segue $\mathrm{\Gamma }\models \gamma \vee \delta$. Similmente, si ottiene $\mathrm{\Gamma },\gamma \models \alpha$ e $\mathrm{\Gamma },\delta \models \alpha$. Sia $\nu$ una valutazione tale che $\nu (\mathrm{\Gamma })=1$. Allora $\nu (\gamma \vee \delta )=1$, ovvero $\nu (\gamma )=1$ o $\nu (\delta )=1$. Se $\nu (\gamma )=1$, e dal fatto che $\mathrm{\Gamma },\gamma \models \alpha$, segue $\nu (\alpha )=1$. Analogamente, se $\nu (\delta )=1$, e dal fatto che $\mathrm{\Gamma },\delta \models \alpha$, segue $\nu (\alpha )=1$. In conclusione, $\mathrm{\Gamma }\models \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

• Template:Collegamenti esterni
• Template:Cita web