Déduction naturelle

La déduction naturelle, dans sa forme actuelle, est un système formel proposé par Gerhard Gentzen en 1934.

De nombreux logiciens, à commencer par Gottlob Frege et David Hilbert, mais également Bertrand Russell et Alfred North Whitehead avec leurs Principia Mathematica, ont développé la logique sous une forme axiomatique inspirée par la méthode euclidienne : les lois logiques sont déduites à partir d’axiomes en utilisant essentiellement la règle de modus ponens. Cette méthode simple a révélé des difficultés liées au fait que les raisonnements sous hypothèses, pratique pourtant courante en mathématiques, ne sont pas directement représentables[3].

Gerhard Gentzen est le premier à avoir développé des formalismes qui, en abandonnant partiellement la méthode euclidienne, redonnent à la logique le caractère d’un cheminement naturel, c'est-à-dire se rapprochant mieux de la pratique mathématique. La principale idée de Gentzen était simple : remplacer les axiomes logiques nécessaires, mais peu naturels, des systèmes à la Hilbert[4] par des règles de déduction comme l'introduction de la flèche qui code formellement le fait de « poser une hypothèse » dans le cours d'un raisonnement. Ce faisant, Gentzen a développé pour la première fois une présentation très symétrique de la logique dans laquelle chaque connecteur est défini par une paire de règles duales : les introductions et les éliminations. Il a également développé un formalisme dans lequel les déductions ne sont pas des suites de phrases, mais des arbres (ou plus précisément des graphes orientés acycliques). Cette méthode, très suggestive pour l’intuition, a conduit Gentzen à faire de belles découvertes[5], mais elle nuit à l’idée originale qui était de reproduire les formes naturelles de raisonnement. Fitch a modifié la méthode de Gentzen en introduisant une notation fondée sur l'indentation pour représenter astucieusement la structure arborescente des déductions. Cette représentation à la fois formelle et plus naturelle n'est toutefois pas la mieux adaptée pour obtenir les résultats principaux de la déduction naturelle comme la normalisation. Pour cette raison, on s'en tiendra dans cet article à une présentation à la Gentzen, le lecteur intéressé pourra se reporter à l'article dédié au style de Fitch.

Dans les années 1960, Dag Prawitz a poursuivi l'étude de la déduction naturelle et y a démontré un théorème d'élimination des coupures[6].

Il existe plusieurs présentations[7] des règles et des démonstrations en déduction naturelle.

• La présentation historique « à la Prawitz » en arbre de preuve où les hypothèses sont aux feuilles ; c'est celle qui est utilisée dans cet article.

${\displaystyle {\frac {\displaystyle {\frac {\displaystyle {\frac {[p\wedge q]}{q}}{\scriptstyle (\wedge E)}\qquad {\frac {[p\wedge q]}{p}}{\scriptstyle (\wedge E)}}{q\wedge p}}{\scriptstyle (\wedge I)}}{p\wedge q\rightarrow q\wedge p}}{\scriptstyle (\rightarrow I)}}$

• Une présentation où les jugements sont des séquents de la forme ${\displaystyle \Gamma \vdash \varphi }$ où ${\displaystyle \Gamma }$ contient les hypothèses actives et ${\displaystyle \varphi }$ est la formule démontrée. Cette présentation, bien que moins intuitive, est techniquement la plus adaptée à démontrer les propriétés de la déduction naturelle.

${\displaystyle {\frac {\displaystyle {\frac {\displaystyle {\frac {\cfrac {}{p\land q\vdash p\land q}}{p\land q\vdash q}}{\scriptstyle (\wedge E)}\qquad {\frac {\cfrac {}{p\land q\vdash p\land q}}{p\land q\vdash p}}{\scriptstyle (\wedge E)}}{p\land q\vdash q\wedge p}}{\scriptstyle (\wedge I)}}{\emptyset \vdash p\wedge q\rightarrow q\wedge p}}{\scriptstyle (\rightarrow I)}}$

• La présentation « à la Fitch » où chaque ligne de la démonstration contient un jugement numéroté. On indente le texte à chaque fois que l'on charge une hypothèse.

1 ${\displaystyle p\land q}$

2 ${\displaystyle p}$

3 ${\displaystyle q}$

4 ${\displaystyle q\land p}$

5 ${\displaystyle p\land q\rightarrow q\land p}$

Concernant la syntaxe, nous renvoyons à l'article calcul des prédicats. La notation ${\displaystyle F[t/x]}$ désigne la formule ${\displaystyle F}$ dans laquelle toutes les occurrences libres de la variable ${\displaystyle x}$ dans ${\displaystyle F}$ sont remplacées par des occurrences du terme ${\displaystyle t}$, après renommage éventuel des occurrences de variables liées de ${\displaystyle F}$ qui apparaissent libres dans ${\displaystyle t}$[8]. Par exemple, si ${\displaystyle F}$ est la formule ${\displaystyle \exists y,y=x}$, alors la notation ${\displaystyle F[y+1/x]}$ ne désigne pas la formule ${\displaystyle \exists y,y=y+1}$, mais la formule ${\displaystyle \exists y',y'=y+1}$ (on a bien pris soin de renommer la variable ${\displaystyle y}$ en ${\displaystyle y'}$ pour éviter le phénomène dit de capture des variables[9]). Le tableau suivant donne les règles de déduction naturelle pour les quantificateurs universel et existentiel[10] :

	Règles d'introduction	Règles d'élimination
pour tout	${\displaystyle {\frac {F}{\forall xF}}{\scriptstyle (\forall I)}}$ à condition que la variable ${\displaystyle x}$ n'apparaisse dans aucune des hypothèses non déchargées.	${\displaystyle {\frac {\forall xF}{F[t/x]}}{\scriptstyle (\forall E)}}$
il existe	${\displaystyle {\frac {F[t/x]}{\exists xF}}{\scriptstyle (\exists I)}}$	${\displaystyle {\frac {\exists xF\quad {\begin{array}{c}[F]\\\vdots \\q\end{array}}}{q}}{\scriptstyle (\exists E)}}$ à condition que la variable x n'apparaisse ni dans la conclusion q ni dans aucune des hypothèses non déchargées ; cette règle décharge l'hypothèse ${\displaystyle F}$.

On notera l'analogie qui n'est pas fortuite entre les règles du connecteur ${\displaystyle \wedge }$ et du quantificateur ${\displaystyle \forall }$, d'une part, et du connecteur ${\displaystyle \vee }$ et du quantificateur ${\displaystyle \exists }$ d'autre part.

Les symétries s'exprimant à travers la dualité introduction/élimination permettent de définir le concept fondamental en théorie de la démonstration de coupure, que l'on appelle aussi redex dans le contexte de la déduction naturelle. Une coupure est la succession d'une règle d'introduction et d'une règle d'élimination portant sur le même connecteur, il y a donc une coupure par connecteur.

Les coupures correspondent à l'utilisation d'un théorème dans le cours d'une preuve. Par exemple, imaginons que l'on cherche à démontrer une propriété ${\displaystyle q}$ et que l'on dispose d'un théorème établissant que ${\displaystyle p\rightarrow q}$. On va alors se ramener à démontrer la propriété ${\displaystyle p}$ et au moyen d'une élimination de l'implication (modus ponens) en déduire la propriété ${\displaystyle q}$ cherchée. Formellement, on va construire la déduction suivante :

${\displaystyle {\frac {\displaystyle {\frac {\vdots }{\displaystyle p\rightarrow q}}\quad {\frac {\vdots }{\displaystyle p}}}{\displaystyle q}}}$

où à gauche figure la déduction du théorème et à droite une déduction de la proposition ${\displaystyle p}$. Maintenant, si l'on considère la déduction du théorème, il y a de fortes chances qu'elle soit de la forme :

${\displaystyle {\frac {\frac {\stackrel {\displaystyle [p]}{\vdots }}{\displaystyle q}}{\displaystyle p\rightarrow q}}}$

En effet, le moyen le plus naturel de démontrer que ${\displaystyle p\rightarrow q}$ est de poser l'hypothèse ${\displaystyle p}$, en déduire ${\displaystyle q}$ et conclure au moyen de la règle d'introduction de l'implication qui décharge l'hypothèse ${\displaystyle p}$. Si l'on revient à la déduction de ${\displaystyle q}$ ci-dessus, on voit donc que dans ce cas celle-ci est de la forme :

${\displaystyle {\frac {{\frac {\frac {\stackrel {\displaystyle [p]}{\vdots }}{\displaystyle q}}{\displaystyle p\rightarrow q}}\quad {\frac {\vdots }{\displaystyle p}}}{\displaystyle q}}}$

ce qui fait apparaître une coupure sur la formule ${\displaystyle p\rightarrow q}$.

La coupure est ainsi le motif le plus utilisé lorsque l'on formalise les raisonnements mathématiques, à tel point que Gentzen en fera une règle à part entière du calcul des séquents. C'est dans ce dernier formalisme (et c'est sans doute la raison pour laquelle il l'a introduit) qu'il a pu démontrer son théorème d'élimination des coupures établissant la possibilité d'associer à toute déduction d'une propriété ${\displaystyle p}$ sous un ensemble fini d'hypothèse ${\displaystyle p_{1}}$, ..., ${\displaystyle p_{k}}$, une déduction normale, c'est-à-dire sans coupure, de la même proposition sous les mêmes hypothèses.

En raison de la présence de la règle de réduction par l'absurde qui comme on l'a vu n'est ni une règle d'élimination, ni une règle d'introduction, ce théorème n'est pas aisé à démontrer en déduction naturelle. Il l'a toutefois été pour la logique intuitionniste, c'est-à-dire dans le sous-système sans la règle de l'absurde, par Dag Prawitz. La procédure de normalisation des déductions définie par Prawitz est à l'origine de très nombreux développements, notamment la découverte de l'analogie profonde entre les arbres de preuves de la déduction naturelle et les lambda-termes typés exprimée par la correspondance preuves/programmes.

Il existe des systèmes de déduction naturelle pour d'autres logiques que la logique classique, comme par exemple les logiques modales.

• (en) Stanislaw Jaśkowski. On the Rules of Suppositions in Formal Logic, 1934.
• Gerhard Gentzen (trad. R. Feys et J. Ladrière), Recherches sur la déduction logique [« Untersuchungen über das logische schließen »], Presses Universitaires de France, 1955
• (de) Gerhard Gentzen. Untersuchungen über das logische Schliessen. Mathematische Zeitschrift, v.39, 1934-35. (traduction anglaise Investigations into Logical Deduction, dans M. E. Szabo (ed.), The Collected Works of Gerhard Gentzen, Amsterdam, North-Holland, 1969.)
• (en) Dag Prawitz. Natural Deduction. Almqvist & Wiksell, Stockholm, 1965.
• J. Dopp, Logiques construites par une methode de deduction naturelle, Gauthier Villars, 1962, 196 pages
• (en) Dirk van Dalen, Logic and Structure, Springer Verlag, 1994. Chapitre 2.8 Natural Dedduction, pages 90-95.
• (en) Pelletier, Jeff, "A History of Natural Deduction and Elementary Logic Textbooks."
• Michel de Rougemont et Richard Lassaigne, Logique et fondements de l'informatique (logique du premier ordre, calculabilité et lambda calcul), Paris, Hermes Science Publications, 1997, 248 p. (ISBN 2-86601-380-8) exposé succinct pages 41-43, mais où les axiomes et le fonctionnement sont donnés.
• J.-Y. Girard, Le Point Aveugle, Cours de Logique, ed. Hermann, Paris, collection « Visions des Sciences », Tome 1 : Vers la Perfection, 280 pp., mai 2006. Chapitre 4 : Cas intuitionniste : LJ et NJ, plus précisément pages 81-96. LJ étant dans cet ouvrage le calcul des séquents et NJ la déduction naturelle.