Deduzione naturale

Da Wikipedia, l'enciclopedia libera.

La deduzione naturale è, nel campo della logica matematica, 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 e con una serie di regole di inferenza il cui numero dipende dai connettivi che definiamo come primitivi.

La storia[modifica | modifica sorgente]

Jan Lukasiewicz 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 Hilbert, Frege e Russell 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 Jaskowski, 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[modifica | modifica sorgente]

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 scrittura


\begin{align} X \\ \vdots\\ B\end{align}

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

La scrittura


\begin{align} \left [A\right ] \\ \vdots\\ B\end{align}

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


\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


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


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


Ex falso quodlibet


\frac{\perp}{A}\perp E


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

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

\frac{\begin{align} \left [A\right ] \\ \vdots\\ \perp \end{align}}{\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 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:

\frac{\begin{align} \left [\neg A\right ] \\ \vdots\\ \perp \end{align}}{A}

Regole per i quantificatori[modifica | modifica sorgente]

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:

\frac{\begin{align} \Gamma \\ \vdots\\ A(x) \end{align}}{\forall x A(x)}\forall I con variabile x libera in \Gamma


\frac{\forall x A(x)}{A(\frac{t}{x})}\forall E


\frac{A(\frac{t}{x})}{\exists x A(x)}\exists I


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


Note[modifica | modifica sorgente]

  1. ^ G. Gentzen, Untersuchungen über das logische Schließen (Mathematische Zeitschrift 39, pp.176–210, 1935)

Bibliografia[modifica | modifica sorgente]

  • S.Jaśkowski. On the Rules of Suppositions in Formal Logic, 1934.
  • G.Gentzen. Untersuchungen über das logische Schliessen. Mathe-matische Zeitschrift , v.39, 1934-35.
  • D.Prawitz. Natural Deduction. Almqvist & Wiksell, Stockholm, 1965.
  • Van Dalen. Logic and Structure. Springer Verlag, Berlin, 1980.
  • J.Pelletier. "A History of Natural Deduction and Elementary Logic Textbooks."

Voci correlate[modifica | modifica sorgente]

Altri progetti[modifica | modifica sorgente]

Collegamenti esterni[modifica | modifica sorgente]