LogicaUniPR - Guida Interattiva

Vai agli Appunti della Prof.ssa (Cap.8)

Capitolo 8: Logica Proposizionale - Calcolo e Deduzione Naturale

Nei capitoli precedenti abbiamo imparato a scrivere formule logiche (sintassi) e a determinarne il valore di verità (semantica). Ora ci addentriamo nel calcolo logico, ovvero nei metodi formali per costruire dimostrazioni e derivare conclusioni valide a partire da premesse. Ci concentreremo su un sistema molto intuitivo chiamato **Deduzione Naturale**, introdotto da Gerhard Gentzen, che cerca di rispecchiare il modo in cui effettivamente ragioniamo.

8.1 Sistemi di Calcolo: Perché?

Mentre le tavole di verità sono un metodo infallibile per verificare la validità di una formula proposizionale o di una conseguenza logica, diventano impraticabili per formule con molte variabili (ricorda, $2^n$ righe!). I sistemi di calcolo, invece, forniscono un insieme di regole di inferenza puramente sintattiche (basate sulla forma delle formule) per costruire catene di ragionamento valide.

Un buon sistema di calcolo deve essere:

  • Corretto (Sound): Se possiamo dimostrare una formula $P$ a partire da un insieme di premesse $\Gamma$ (scritto $\Gamma \vdash P$), allora $P$ deve essere una conseguenza logica di $\Gamma$ (cioè $\Gamma \models P$). In breve, il sistema non ci permette di dimostrare cose false.
  • Completo (Complete): Se $P$ è una conseguenza logica di $\Gamma$ ($\Gamma \models P$), allora dobbiamo essere in grado di dimostrare $P$ da $\Gamma$ usando il sistema ($\Gamma \vdash P$). In breve, il sistema è abbastanza potente da dimostrare tutte le verità logiche.

La Deduzione Naturale per la logica proposizionale classica è sia corretta che completa.

Una dimostrazione (o derivazione) di una conclusione $C$ da un insieme di premesse (o ipotesi) $H_1, H_2, \dots, H_n$ è una sequenza finita di formule, dove ogni formula è o una premessa, o un assioma del sistema, o è ottenuta da formule precedenti applicando una regola di inferenza. L'ultima formula della sequenza è la conclusione $C$.

8.2 La Deduzione Naturale di Gentzen

La Deduzione Naturale si basa sull'idea di avere, per ogni connettivo logico, delle regole per "introdurlo" (come connettivo principale della conclusione di un'inferenza) e delle regole per "eliminarlo" (usare una formula che ha quel connettivo come principale per derivare qualcos'altro).

Le derivazioni sono spesso rappresentate come alberi di derivazione, dove le foglie sono le premesse iniziali o ipotesi temporanee, e la radice è la conclusione finale. Alcune regole permettono di "scaricare" o "cancellare" le ipotesi temporanee fatte durante la dimostrazione.

Useremo la seguente notazione per una regola di inferenza:
$\frac{\text{Premessa}_1 \quad \text{Premessa}_2 \quad \dots}{\text{Conclusione}} \quad (\text{NomeRegola})$

8.2.1 Regole di Inferenza Elementari

Queste regole non scaricano ipotesi.

  • Congiunzione ($\wedge$):
    • Introduzione dell'AND ($I\wedge$): Se hai derivato $A$ e hai derivato $B$, puoi concludere $(A \wedge B)$.
      $\frac{A \quad B}{(A \wedge B)} \quad (I\wedge)$
    • Eliminazione dell'AND ($E\wedge_1$ e $E\wedge_2$): Da $(A \wedge B)$, puoi concludere $A$. E da $(A \wedge B)$, puoi concludere $B$.
      $\frac{(A \wedge B)}{A} \quad (E\wedge_1)$
      $\frac{(A \wedge B)}{B} \quad (E\wedge_2)$
  • Disgiunzione ($\vee$):
    • Introduzione dell'OR ($I\vee_1$ e $I\vee_2$): Se hai derivato $A$, puoi concludere $(A \vee B)$ (per qualsiasi $B$). Simmetricamente, se hai $B$, puoi concludere $(A \vee B)$.
      $\frac{A}{(A \vee B)} \quad (I\vee_1)$
      $\frac{B}{(A \vee B)} \quad (I\vee_2)$
  • Implicazione ($\Rightarrow$):
    • Eliminazione dell'Implicazione ($E\Rightarrow$, o Modus Ponens - MP): Se hai derivato $A$ e hai derivato $(A \Rightarrow B)$, puoi concludere $B$.
      $\frac{A \quad (A \Rightarrow B)}{B} \quad (E\Rightarrow \text{ o MP})$
  • Falsità ($\perp$) e Negazione ($\neg$):
    • Introduzione del Falso ($I\perp$, o Eliminazione della Negazione $E\neg$): Se hai derivato sia $A$ che $(\neg A)$ (una contraddizione), puoi concludere $\perp$.
      $\frac{A \quad (\neg A)}{\perp} \quad (I\perp \text{ o } E\neg)$
    • Eliminazione del Falso ($E\perp$, o Ex Falso Quodlibet - EFQ): Dal falso ($\perp$), puoi concludere qualsiasi formula $A$.
      $\frac{\perp}{A} \quad (E\perp \text{ o EFQ})$

8.2.2 Regole di Inferenza Condizionali (che scaricano ipotesi)

Queste regole introducono un connettivo "scaricando" un'ipotesi fatta temporaneamente per la loro applicazione. L'ipotesi scaricata viene solitamente indicata tra parentesi quadre $[A]$ e numerata per indicare quale applicazione di regola l'ha scaricata.

  • Introduzione dell'Implicazione ($I\Rightarrow$): Se, assumendo temporaneamente $A$ come ipotesi, riesci a derivare $B$, allora puoi concludere $(A \Rightarrow B)$ e "scaricare" (non dipendere più da) l'ipotesi $A$.
    $\begin{array}{c} [A]^u \\ \vdots \\ B \\ \hline (A \Rightarrow B) \end{array} \quad (I\Rightarrow, u)$
    L'etichetta $u$ indica che l'ipotesi $A$ marcata con $u$ è stata scaricata da questa regola.
  • Introduzione della Negazione ($I\neg$): Se, assumendo temporaneamente $A$, riesci a derivare una contraddizione ($\perp$), allora puoi concludere $(\neg A)$ e scaricare l'ipotesi $A$.
    $\begin{array}{c} [A]^u \\ \vdots \\ \perp \\ \hline (\neg A) \end{array} \quad (I\neg, u)$
  • Eliminazione della Disgiunzione ($E\vee$, o Prova per Casi): Se hai $(A \vee B)$, e puoi derivare una formula $C$ assumendo $A$, e puoi anche derivare la stessa formula $C$ assumendo $B$, allora puoi concludere $C$. Le ipotesi $A$ e $B$ vengono scaricate.
    $\begin{array}{c c c} & [A]^u & [B]^w \\ & \vdots & \vdots \\ (A \vee B) & C & C \\ \hline \multicolumn{3}{c}{C} \end{array} \quad (E\vee, u, w)$
  • Regola per Assurdo (RAA - Reductio Ad Absurdum) o Introduzione della Doppia Negazione (DN): Se, assumendo temporaneamente $(\neg A)$, riesci a derivare una contraddizione ($\perp$), allora puoi concludere $A$ e scaricare l'ipotesi $(\neg A)$. Questa regola è tipica della logica classica.
    $\begin{array}{c} [\neg A]^u \\ \vdots \\ \perp \\ \hline A \end{array} \quad (RAA, u)$

Una dimostrazione (o derivazione) di $\Gamma \vdash P$ è un albero costruito secondo queste regole, le cui foglie non scaricate sono tutte formule in $\Gamma$, e la cui radice è $P$. Se $\Gamma$ è vuoto, $\vdash P$ significa che $P$ è un teorema del sistema.

8.3 Esempi di Derivazioni in Deduzione Naturale

Esempio 1: Dimostrare $\vdash (A \Rightarrow (B \Rightarrow (A \wedge B)))$

Vogliamo dimostrare che questa formula è un teorema (non dipende da premesse).

Derivazione:

[A]^1   [B]^2
----------- (I∧)
 (A ∧ B)
----------- (I⇒, 2)
(B ⇒ (A ∧ B))
----------------- (I⇒, 1)
(A ⇒ (B ⇒ (A ∧ B)))

Spiegazione:

  1. Assumiamo temporaneamente $A$ (ipotesi 1) e $B$ (ipotesi 2).
  2. Con $A$ e $B$ disponibili, applichiamo $(I\wedge)$ per ottenere $(A \wedge B)$.
  3. Ora, poiché da $B$ (ipotesi 2) abbiamo derivato $(A \wedge B)$ (sotto l'ipotesi 1 ancora attiva), possiamo applicare $(I\Rightarrow)$ per concludere $(B \Rightarrow (A \wedge B))$, scaricando l'ipotesi $B$ (marcata con 2).
  4. Ora, poiché da $A$ (ipotesi 1) abbiamo derivato $(B \Rightarrow (A \wedge B))$, possiamo applicare $(I\Rightarrow)$ per concludere $(A \Rightarrow (B \Rightarrow (A \wedge B)))$, scaricando l'ipotesi $A$ (marcata con 1).

Tutte le ipotesi sono state scaricate, quindi la formula è un teorema.

Esempio 2: Dimostrare $A \Rightarrow B, B \Rightarrow C \vdash A \Rightarrow C$ (Sillogismo Ipotetico)

Derivazione:

[A]^1   A ⇒ B
----------- (E⇒)
     B      B ⇒ C
     ----------- (E⇒)
          C
     ----------- (I⇒, 1)
      A ⇒ C

Spiegazione:

  1. Le premesse date sono $A \Rightarrow B$ e $B \Rightarrow C$.
  2. Assumiamo temporaneamente $A$ (ipotesi 1).
  3. Da $A$ (ipotesi 1) e $A \Rightarrow B$ (premessa), otteniamo $B$ per $(E\Rightarrow)$.
  4. Da $B$ (appena derivato) e $B \Rightarrow C$ (premessa), otteniamo $C$ per $(E\Rightarrow)$.
  5. Poiché assumendo $A$ (ipotesi 1) abbiamo derivato $C$, possiamo concludere $A \Rightarrow C$ per $(I\Rightarrow)$, scaricando l'ipotesi $A$.

Le foglie non scaricate sono le premesse date, quindi la derivazione è corretta.

8.4 Correttezza e Completezza

Come menzionato, il sistema di Deduzione Naturale per la logica proposizionale classica è:

  • Corretto: Se $\Gamma \vdash P$, allora $\Gamma \models P$. Ogni formula dimostrabile è una conseguenza logica. Non si possono dimostrare falsità.
  • Completo: Se $\Gamma \models P$, allora $\Gamma \vdash P$. Ogni conseguenza logica è dimostrabile.

Questi due teoremi (la cui dimostrazione è complessa e va oltre gli scopi di questo corso introduttivo) sono fondamentali perché stabiliscono che la derivabilità sintattica ($\vdash$) e la conseguenza semantica ($\models$) coincidono per la logica proposizionale. Ciò significa che possiamo usare la Deduzione Naturale con la certezza che i nostri ragionamenti formali rispecchiano le verità logiche.

8.5 Esercizi del Capitolo 8

Esercizio 8.1: Dimostrare Teoremi Semplici

Usando le regole della Deduzione Naturale, dimostra i seguenti teoremi:

  1. $\vdash A \Rightarrow A$ (Identità)
  2. $\vdash \neg \neg A \Rightarrow A$ (Doppia Negazione, usando RAA)
  3. $\vdash (A \wedge \neg A) \Rightarrow \perp$ (Principio di Non Contraddizione, forma implicativa)

Esercizio 8.2: Derivazioni con Premesse

Dimostra le seguenti derivazioni:

  1. $A \vee B, \neg A \vdash B$ (Sillogismo Disgiuntivo)
  2. $A \Rightarrow B, \neg B \vdash \neg A$ (Modus Tollens)

Esercizio 8.3 (da `19_esempi_esame.pdf`): Dimostrazione più complessa

Dimostra: $\vdash (A \Rightarrow (B \Rightarrow C)) \Rightarrow ((A \Rightarrow B) \Rightarrow (A \Rightarrow C))$