Deduzione naturale

La deduzione naturale è, nel campo della logica, un sistema deduttivo. Un sistema deduttivo è una relazione che può sussistere tra un insieme di formule e una formula: se la relazione vale, diciamo che la formula viene dedotta dall'insieme. La deduzione naturale si propone quindi come un metodo per dimostrare che un'affermazione è conseguenza di certe ipotesi. A differenza dei sistemi assiomatici è un sistema senza assiomi, basato su una serie di regole di inferenza il cui numero dipende dai connettivi che definiamo come primitivi.

Jan Łukasiewicz fu il primo durante una serie di seminari in Polonia nel 1926 a parlare della necessità per i matematici di costruire dimostrazioni usando una teoria diversa da quella assiomatica tipica dei sistemi usati fino ad allora da Frege, Russell e Hilbert, e il primo tentativo di teorizzare un sistema di deduzione “naturale” è del suo allievo Stanislaw Jaśkowski nel 1934.

Jaśkowski propose due diversi metodi di rappresentazione della deduzione naturale. Il primo è un metodo grafico basato sulla costruzioni di rettangoli attorno a parti di prove e su di esso si basano le dimostrazioni fatte usando quelli che oggi si chiamano diagrammi di Fitch. Il secondo metodo consiste nell'aggiungere una notazione numerica a sinistra delle formule nella dimostrazione. Su questo sono basati il metodo di Suppes e la variante di Lemmon chiamata sistema L.

La deduzione naturale nella sua formulazione moderna ad albero viene proposta, indipendentemente da Jaśkowski, nel 1935 da Gerhard Gentzen ed è lui il primo a introdurre il termine “deduzione naturale”:

Ich wollte zunächst einmal einen Formalismus aufstellen, der dem wirklichen Schließen möglichst nahe kommt. So ergab sich ein "Kalkül des natürlichen Schließens".^[1]

(Per prima cosa ho voluto costruire un formalismo che si avvicini il più possibile al ragionamento reale. Così nacque il "calcolo della deduzione naturale".)

Nel 1965 Prawitz darà una sintesi completa dei calcoli di deduzione naturale, e trasporterà gran parte del lavoro di Gentzen con i calcoli dei sequenti in deduzione naturale.

Le regole di inferenza consistono di regole di introduzione (I) e regole di eliminazione (E) per ogni costante logica.

Per ogni regola le formule sopra la riga sono dette premesse e la formula sotto la riga conclusione della regola. La sigla a destra della riga sta a indicare la rispettiva regola.

La scrittura

${\displaystyle {\begin{aligned}X\\\vdots \\B\end{aligned}}}$

sta ad indicare che la formula B dipende dalle assunzioni occorrenti nell'insieme X.

La scrittura

${\displaystyle {\begin{aligned}\left[A\right]\\\vdots \\B\end{aligned}}}$

sta ad indicare che la formula A è un'ipotesi ausiliaria che può essere scaricata nel corso della deduzione.

${\displaystyle {\frac {A\land B}{A}}\land E\quad {\frac {A\land B}{B}}\land E\qquad {\frac {A\qquad B}{A\land B}}\land I}$

${\displaystyle {\frac {A}{A\lor B}}\lor I\quad {\frac {B}{A\lor B}}\lor I\quad {\frac {A\lor B\quad {\begin{aligned}\left[A\right]\\\vdots \\C\end{aligned}}\quad {\begin{aligned}\left[B\right]\\\vdots \\C\end{aligned}}}{C}}\lor E}$

${\displaystyle {\frac {\begin{aligned}\left[A\right]\\\vdots \\B\end{aligned}}{A\to B}}\to I\qquad {\frac {A\quad A\to B}{B}}\to E}$

Ex falso quodlibet

${\displaystyle {\frac {\perp }{A}}\perp E}$

Il sistema delle regole ${\displaystyle \land I}$, ${\displaystyle \land E}$, ${\displaystyle \lor I}$, ${\displaystyle \lor E}$, ${\displaystyle \to I}$, ${\displaystyle \to E}$ individua la cosiddetta logica minimale; se a queste si aggiunge ${\displaystyle \perp E}$ si ottiene un sistema di regole per la logica intuizionistica.

Per la definizione intuizionistica di ${\displaystyle \neg A}$ come ${\displaystyle A\to \perp }$ e per le regole ${\displaystyle \to I}$ e ${\displaystyle \to E}$ si vede che le regole

${\displaystyle {\frac {\begin{aligned}\left[A\right]\\\vdots \\\perp \end{aligned}}{\neg A}}\qquad \qquad {\frac {A\quad \neg A}{\perp }}}$

sono derivabili e quindi non serve assumerle.

All'interno della logica classica vale Il principio del terzo escluso ${\displaystyle A\lor \neg A}$ quindi il sistema di regole per la logica classica comprende le regole di inferenza già viste per la logica intuizionistica insieme al principio di riduzione all'assurdo:

${\displaystyle {\frac {\begin{aligned}\left[\neg A\right]\\\vdots \\\perp \end{aligned}}{A}}}$

Sia A(x) una funzione proposizionale cioè una qualsiasi espressione contenente una variabile x e tale che sostituendo a x dei valori arbitrariamente scelti in un opportuno dominio D si ottenga una proposizione e t un qualunque termine del linguaggio.

Allora le regole di inferenza per i quantificatori sono:

${\displaystyle {\frac {\begin{aligned}\Gamma \\\vdots \\A(x)\end{aligned}}{\forall xA(x)}}\forall I}$ con variabile x non libera in ${\displaystyle \Gamma }$

${\displaystyle {\frac {\forall xA(x)}{A({\frac {t}{x}})}}\forall E}$

${\displaystyle {\frac {A({\frac {t}{x}})}{\exists xA(x)}}\exists I}$

${\displaystyle {\frac {\exists xA(x)\qquad \Gamma \ddots {\begin{aligned}\left[A(x)\right]\\\vdots \\C\end{aligned}}}{C}}\exists E}$ con x variabile non libera in C e in ${\displaystyle \Gamma }$.

• Stanislaw Jaśkowski. On the Rules of Suppositions in Formal Logic, 1934.
• Gerhard Gentzen. Untersuchungen über das logische Schliessen. Mathematische Zeitschrift, vol. 39, 1934-35. (traduzione inglese Investigations into Logical Deduction in M. E. Szabo (ed.), The Collected Works of Gerhard Gentzen, Amsterdam, North-Holland, 1969).
• Dag Prawitz. Natural Deduction. Almqvist & Wiksell, Stockholm, 1965.
• Dirk Van Dalen. Logic and Structure. Springer Verlag, Berlin, 1980.

• Gerhard Gentzen
• sequente
• logica classica
• logica intuizionista

• Wikibooks contiene testi o manuali su Logica/Calcolo delle proposizioni/La deduzione naturale

• (EN) Andrzej Indrzejczak, Natural Deduction, su iep.utm.edu.
• (EN) Francis Jeffry Pelletier, A History of Natural Deduction and Elementary Logic Textbooks (PDF), su sfu.ca.
• (EN) Un dimostratore interattivo che utilizza la deduzione naturale, su teachinglogic.liglab.fr.
• (EN) La deduzione naturale visualizzata come gioco del domino, su winterdrache.de.