# Logica matematica/Calcolo delle proposizioni/La deduzione naturale

Logica matematica
Copertina Tutti i moduli · Sviluppo
* InsiemiLogica matematica/Insiemi
* Sistemi formaliLogica matematica/Sistemi formali
* Calcolo delle proposizioniLogica matematica/Calcolo delle proposizioni
** Il sistema di Frege-HilbertLogica matematica/Calcolo delle proposizioni/Sistema di Hilbert
** La deduzione naturaleLogica matematica/Calcolo delle proposizioni/La deduzione naturale
** Il calcolo dei sequenti
** I tableaux semanticiLogica matematica/Calcolo delle proposizioni/I tableaux semantici
** La risoluzioneLogica matematica/Calcolo delle proposizioni/La risoluzione
** Esercizi su tavole di veritàLogica matematica/Calcolo delle proposizioni/Esercizi su tavole di verità
* Calcolo dei predicatiLogica matematica/Calcolo dei predicati
* Teoria dei modelliLogica matematica/Teoria dei modelli
* Computabilità
* IncompletezzaLogica matematica/Incompletezza
** Teoremi di incompletezza di GödelLogica matematica/Incompletezza/Teoremi di incompletezza di Gödel
* Intermezzo: EuclideLogica matematica/Intermezzo Euclide
* Intermezzo: i paradossiLogica matematica/Intermezzo paradossi
* Risorse internetLogica matematica/Risorse internet
Modifica il sommario

### La deduzione naturale

Gerhard Gentzen ha notato che il sistema assiomatico di Hilbert è molto lontano dal modo di ragionare che applicano i matematici nella loro attività quotidiana.
Risalire agli assiomi o partire dagli assiomi non è semplice e spesso è molto poco intuitivo, in fondo l'unico esempio significativo di teoria assiomatica che ci è giunta da tempi lontani è la geometria di Euclide.
Gentzen ha cercato un sistema di dimostrazione che fosse semplice ed intuitivo, arrivando alla "deduzione naturale", un sistema di dimostrazione senza assiomi e con una serie di regole il cui numero dipende dai connettivi che definiamo come primitivi.

## Le regole

Per ogni connettivo sono specificate delle regole di inferenza che permettono di introdurre o eliminare una operazione logica nel corso della dimostrazione.
Vediamo quindi le regole:
| ${\Phi \quad \Psi } \over {\Phi \wedge \Psi }$ | | Introduzione di $\wedge$ | ${\Phi \wedge \Psi } \over \Phi$ | ${\Phi \wedge \Psi } \over \Psi$ | Eliminazione di $\wedge$ |
| $\Phi \over {\Phi \vee \Psi }$ | $\Psi \over {\Phi \vee \Psi }$ | Introduzione di $\vee$ | ${\Phi \vee \Psi \quad {\stackrel {(\Phi )}{\stackrel {\vdots }{\chi }}}{\stackrel {(\Psi )}{\stackrel {\vdots }{\chi }}}} \over \chi$ | | Eliminazione di $\vee$ |
| ${\stackrel {(\Phi )}{\stackrel {\vdots }{\Psi }}} \over {\Phi \rightarrow \Psi }$ | | Introduzione di $\rightarrow$ | ${\Phi \quad \Phi \rightarrow \Psi } \over \Psi$ | | Eliminazione di $\rightarrow$ |
| ${\stackrel {(\Phi )}{\stackrel {\vdots }{false}}} \over {\neg \Phi }$ | | Introduzione di $\neg$ | ${false} \over {\Phi }$ | ${\neg \neg \Phi } \over {\Phi }$ | Eliminazione di $\neg$ |
Vediamo come si utilizza questo schema prendendo come esempio la prima regola. Questa ci dice che se abbiamo una dimostrazione di $\Phi$ e una dimostrazione di $\Psi$ (la riga sopra la barra orizzontale) possiamo derivare la frase $\Phi \wedge \Psi$ che è da considerarsi dimostrata. La regola si può anche utilizzare in senso inverso, se devo dimostrare la congiunzione (frase sotto la riga orizzontale) devo procurarmi una dimostrazione delle due sentenze che la compongono (frasi sopra la riga).
Nelle regole le sentenze che assumiamo come ipotesi sono indicate tra parentesi. Nella regola di introduzione dell' $\rightarrow$ per esempio vediamo il teorema di deduzione: se dall' assunzione di $\Phi$ ottengo la dimostrazione di $\Psi$ allora posso derivare che $\Phi$ implica $\Psi$.

## Esempi

Proviamo a dimostrare:
$\Phi \rightarrow \Phi$
con la deduzione naturale è estremamente semplice, basta ipotizzare $\Phi$ e quindi utilizzare la regola di introduzione di $\rightarrow$.
${\stackrel {(\Phi )}{\Phi \over {\Phi \rightarrow \Phi }}}$
Svolgiamo ora anche il secondo esempio che avevamo proposto con il sistema di Hilbert.
$(\Phi \rightarrow \Psi \wedge \Psi \rightarrow \chi )\rightarrow (\Phi \rightarrow \chi )$
La dimostrazione è:
${{{{3.(\Phi )\quad {{1.(\Phi \rightarrow \Psi \wedge \Psi \rightarrow \chi )} \over {2.\Phi \rightarrow \Psi }}} \over {4.\Psi }}\quad {{5.(\Phi \rightarrow \Psi \wedge \Psi \rightarrow \chi )} \over {6.\Psi \rightarrow \chi }}} \over {{7.\chi } \over {8.\Phi \rightarrow \chi }}} \over {9.(\Phi \rightarrow \Psi \wedge \Psi \rightarrow \chi )\rightarrow (\Phi \rightarrow \chi )}$
la dimostrazione si svolge con questi passaggi:
1. ipotizziamo l' antecedente dell' implicazione che vogliamo dimostrare $\Phi \rightarrow \Psi \wedge \Psi \rightarrow \chi$
2. usiamo la regola di eliminazione della congiunzione tenendo solo la parte $\Phi \rightarrow \Psi$
3.ora inseriamo $\Phi$ come ipotesi
4. possiamo derivare $\Psi$ utilizzando la regola di eliminazione dell' implicazione
5. ipotizziamo ancora l' antecedente
6. usiamo la regola di eliminazione della congiunzione tenendo solo la parte $\Psi \rightarrow \chi$
7. usiamo la regola di eliminazione dell' implicazione per derivare $\chi$
8. ora usiamo la regola di introduzione dell' implicazione per trasformare l' ipotesi $\Phi$ in una implicazione
9. ora usiamo la regola di introduzione dell' implicazione per arrivare alla formula che volevamo dimostrare

## Collegamenti esterni

* (EN) Un dimostratore interattivo che utilizza la deduzione naturale.