LogicaUniPR - Guida Interattiva

Introduzione al Calcolo Logico

Dopo aver definito la sintassi (come scrivere formule corrette) e la semantica (come interpretare il loro valore di verità), il passo successivo è studiare il calcolo logico. Il calcolo logico si occupa di formalizzare i processi di ragionamento, ovvero come derivare conclusioni valide a partire da un insieme di premesse. L'obiettivo è creare sistemi di regole che permettano di costruire dimostrazioni in modo puramente sintattico (manipolando simboli), garantendo al contempo la correttezza semantica (le conclusioni derivate devono essere conseguenze logiche delle premesse).

Un esempio di enunciato che si può voler dimostrare è: "Se $a \Rightarrow b$ è vero e $a \Rightarrow (b \Rightarrow c)$ è vero, allora $a \Rightarrow c$ è vero." Semanticamente, questo significa che $\{(a \Rightarrow b), (a \Rightarrow (b \Rightarrow c))\} \models (a \Rightarrow c)$. Il calcolo logico ci fornisce gli strumenti per dimostrarlo attraverso passaggi formali.

Sistemi di Calcolo

Esistono diversi sistemi di calcolo formale, tra cui:

• Deduzione Naturale (di Gentzen): Cerca di mimare il modo "naturale" in cui si costruiscono i ragionamenti, usando regole di introduzione ed eliminazione per ogni connettivo logico.
• Sistemi Assiomatici (alla Hilbert): Partono da un insieme minimo di assiomi (formule considerate vere) e poche regole di inferenza (tipicamente Modus Ponens) per derivare tutti gli altri teoremi.
• Calcolo dei Sequenti: Un'altra formalizzazione di Gentzen, utile per studiare le proprietà dei sistemi logici.

Lo scopo di questi sistemi è ottenere dimostrazioni (o derivazioni) corrette. Un buon sistema di calcolo dovrebbe essere:

• Corretto (Sound): Tutto ciò che è dimostrabile nel sistema ($\Gamma \vdash P$) deve essere anche una conseguenza logica ($\Gamma \models P$). Non si possono dimostrare falsità.
• Completo (Complete): Tutto ciò che è una conseguenza logica ($\Gamma \models P$) deve essere anche dimostrabile nel sistema ($\Gamma \vdash P$). Il sistema è abbastanza potente da catturare tutte le verità logiche.

La logica proposizionale classica gode di entrambi questi importanti risultati: è corretta e completa.

La notazione $\Gamma \vdash P$ indica che la formula $P$ è derivabile (o dimostrabile) dall'insieme di premesse $\Gamma$ usando le regole del sistema di calcolo. Se $\Gamma = \emptyset$, scriviamo $\vdash P$, e $P$ è un teorema del sistema.

Deduzione Naturale

Il sistema di Deduzione Naturale si basa su regole di inferenza per ciascun connettivo logico. Per ogni connettivo, c'è (tipicamente) una regola per "introdurlo" come connettivo principale di una conclusione, e una regola per "eliminarlo" da una premessa per derivare qualcos'altro.

Una derivazione in deduzione naturale è spesso rappresentata come un albero, dove le foglie sono le premesse (o ipotesi temporanee) e la radice è la conclusione. Alcune regole permettono di "scaricare" (o cancellare) ipotesi temporanee fatte durante la derivazione.

Regole di Inferenza Elementari

(Notazione: $A, B, C$ sono FBF)

• Congiunzione ($\wedge$):
  • Introduzione ($I\wedge$): $\frac{A \quad B}{A \wedge B}$ (Se hai derivato $A$ e hai derivato $B$, puoi concludere $A \wedge B$)
  • Eliminazione ($E\wedge_1$): $\frac{A \wedge B}{A}$ (Da $A \wedge B$, puoi concludere $A$)
  • Eliminazione ($E\wedge_2$): $\frac{A \wedge B}{B}$ (Da $A \wedge B$, puoi concludere $B$)
• Disgiunzione ($\vee$):
  • Introduzione ($I\vee_1$): $\frac{A}{A \vee B}$ (Se hai derivato $A$, puoi concludere $A \vee B$, per qualsiasi $B$)
  • Introduzione ($I\vee_2$): $\frac{B}{A \vee B}$ (Se hai derivato $B$, puoi concludere $A \vee B$, per qualsiasi $A$)
• Implicazione ($\Rightarrow$):
  • Eliminazione ($E\Rightarrow$ o Modus Ponens, MP): $\frac{A \quad A \Rightarrow B}{B}$ (Se hai $A$ e $A \Rightarrow B$, puoi concludere $B$)
• Falsità ($\perp$):
  • Introduzione ($I\perp$ o Eliminazione Negazione $E\neg$): $\frac{A \quad \neg A}{\perp}$ (Da una contraddizione $A$ e $\neg A$, derivi il falso)
  • Eliminazione ($E\perp$ o Ex Falso Quodlibet): $\frac{\perp}{A}$ (Dal falso, puoi concludere qualsiasi formula $A$)

Regole di Inferenza Condizionali (che possono scaricare ipotesi)

Le ipotesi scaricate sono indicate tra parentesi quadre, es. $[A]$.

• Disgiunzione ($\vee$):
  • Eliminazione ($E\vee$ o Prova per Casi):
    $\begin{array}{c} \\ A \vee B \quad \begin{array}{c} [A] \\ \vdots \\ C \end{array} \quad \begin{array}{c} [B] \\ \vdots \\ C \end{array} \\ \hline C \end{array}$
    (Se hai $A \vee B$, e puoi derivare $C$ assumendo $A$, e puoi anche derivare $C$ assumendo $B$, allora puoi concludere $C$. Le ipotesi $[A]$ e $[B]$ vengono scaricate).
• Implicazione ($\Rightarrow$):
  • Introduzione ($I\Rightarrow$):
    $\begin{array}{c} [A] \\ \vdots \\ B \\ \hline A \Rightarrow B \end{array}$
    (Se, assumendo $A$ come ipotesi temporanea, riesci a derivare $B$, allora puoi concludere $A \Rightarrow B$, scaricando l'ipotesi $[A]$).
• Negazione ($\neg$):
  • Introduzione ($I\neg$):
    $\begin{array}{c} [A] \\ \vdots \\ \perp \\ \hline \neg A \end{array}$
    (Se, assumendo $A$, derivi una contraddizione $\perp$, allora puoi concludere $\neg A$, scaricando l'ipotesi $[A]$).
• Regola per Assurdo (RAA - Reductio Ad Absurdum):
  • $\begin{array}{c} [\neg A] \\ \vdots \\ \perp \\ \hline A \end{array}$
    (Se, assumendo $\neg A$, derivi una contraddizione $\perp$, allora puoi concludere $A$, scaricando l'ipotesi $[\neg A]$). Questa regola è caratteristica della logica classica (non intuizionista).

Una formula $P$ si considera "dimostrata" (un teorema, $\vdash P$) se esiste un albero di derivazione la cui radice è $P$ e tutte le foglie sono o premesse date o ipotesi che sono state correttamente scaricate.

Correttezza e Completezza della Deduzione Naturale Proposizionale

Per la logica proposizionale classica, il sistema di Deduzione Naturale (con le regole sopra elencate, inclusa RAA) è:

• Corretto (Sound): Se $\Gamma \vdash P$ (P è derivabile da $\Gamma$), allora $\Gamma \models P$ (P è conseguenza semantica di $\Gamma$). Il sistema non permette di derivare conclusioni false da premesse vere.
• Completo (Complete): Se $\Gamma \models P$ (P è conseguenza semantica di $\Gamma$), allora $\Gamma \vdash P$ (P è derivabile da $\Gamma$). Il sistema è abbastanza potente da derivare tutte le conseguenze logiche valide.

In particolare, se $P$ è una tautologia ($\models P$), allora $P$ è un teorema ($\vdash P$), cioè può essere dimostrata senza premesse.
Questi due teoremi (di Correttezza e Completezza) stabiliscono una forte equivalenza tra la nozione semantica di conseguenza logica e la nozione sintattica di derivabilità.