Déduction naturelle

En logique mathématique, la déduction naturelle est un système formel où les règles de déduction des démonstrations sont proches des façons naturelles de raisonner. C'est une étape importante de l'histoire de la théorie de la démonstration pour plusieurs raisons :

• contrairement aux systèmes à la Hilbert fondés sur des listes d'axiomes logiques plus ou moins ad hoc, la déduction naturelle repose sur un principe systématique de symétrie : pour chaque connecteur, on donne une paire de règles duales (introduction/élimination) ;
• elle a conduit Gentzen à inventer un autre formalisme très important en théorie de la démonstration, encore plus « symétrique » : le calcul des séquents ;
• elle a permis dans les années 1960 d'identifier la première instance de l'isomorphisme de Curry-Howard.

La terminologie « déduction naturelle » a été suggérée, par Gentzen, eu égard à l'aspect peu intuitif des systèmes à la Hilbert.

Les origines de la 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.

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 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, 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.

Les principes de la déduction naturelle

Notion de règle

La déduction naturelle est fondée sur des règles d'inférence qui permettent de déduire des théorèmes à partir d'autres. Par exemple la règle suivante, le modus ponens mais que l'on appelle élimination de la flèche dans ce contexte :

$\frac{pp\to q}{q}$

permet de déduire $q$ à partir d'une démonstration de $p$ et d'une démonstration de $p\to q$. Les formules au-dessus de la barre s'appellent les prémisses et la formule sous la barre s'appelle la conclusion. Dans l'exemple, $p$ et $p\to q$ sont les prémisses et $q$ est la conclusion.

Notion d'arbre de preuve

Une démonstration en déduction naturelle est un arbre de preuve. Voici un arbre de preuve déduisant l'énoncé le sol est glissant des trois hypothèses : (1) il pleut, (2) s'il pleut alors le sol est mouillé et (3) si le sol est mouillé alors le sol est glissant :

$\frac{\frac{\text{il pleut}\text{il pleut}\to \text{sol mouillé}}{\text{sol mouillé}}\text{sol mouillé}\to \text{sol glissant}}{\text{sol glissant}}$

La règle d'élimination de la flèche y est appliquée deux fois.

Notion d'hypothèse

La déduction naturelle fait des raisonnements sous des hypothèses. Une démonstration de q sous l'hypothèse p a la forme :

$\frac{\stackrel{p}{⋮}}{q}$

où les points de suspension verticaux représentent un arbre de preuve de conclusion $q$ et dont certaines feuilles comportent l'hypothèse $p$.

Notion d'hypothèse déchargée

Il existe aussi des règles où une hypothèse est déchargée, c'est-à-dire que l'hypothèse n'est plus supposée à partir de l'application de la règle. Par exemple, à partir d'une démonstration de q sous l'hypothèse p, on peut construire une démonstration de l'implication $p\to q$. On note :

$\frac{\stackrel{[p]}{\stackrel{⋮}{q}}}{p\to q}$

et les crochets dans $[p]$ signifient que l'hypothèse $p$ est déchargée. Cette règle appelée introduction de l'implication est une internalisation du théorème de déduction des systèmes à la Hilbert.

Notion de règle d'introduction et de règle d'élimination

La règle $\frac{pq}{p\wedge q}$ se lit : de la prémisse p et la prémisse q, on conclut la formule $p\wedge q$ (p et q). C'est une règle d'introduction (ici la règle d'introduction du « et ») car le connecteur « et » apparaît dans la conclusion.

La règle $\frac{p\wedge q}{p}$ se lit : de la prémisse $p\wedge q$, on conclut la formule p. C'est une règle d'élimination (ici la règle d'élimination du « et ») car le connecteur « et » est éliminé et n'est plus dans la conclusion.

Différentes présentations des règles et des démonstrations

Il existe plusieurs présentations 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.

$\frac{\frac{\frac{[p\wedge q]}{q}(\wedge E)\frac{[p\wedge q]}{p}(\wedge E)}{q\wedge p}(\wedge I)}{p\wedge q\to q\wedge p}(\to I)$

• Une présentation où les jugements sont des séquents de la forme $\mathrm{\Gamma }⊢\phi$ où $\mathrm{\Gamma }$ contient les hypothèses actives et $\phi$ 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.

$\frac{\frac{\frac{\frac{}{p\wedge q⊢p\wedge q}}{p\wedge q⊢q}(\wedge E)\frac{\frac{}{p\wedge q⊢p\wedge q}}{p\wedge q⊢p}(\wedge E)}{p\wedge q⊢q\wedge p}(\wedge I)}{\mathrm{\varnothing }⊢p\wedge q\to q\wedge p}(\to 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 $p\wedge q$

2 $p$

3 $q$

4 $q\wedge p$

5 $p\wedge q\to q\wedge p$

Déduction naturelle en logique propositionnelle

Règles

Le tableau suivant donne les règles d'introduction et les règles d'élimination des connecteurs →, ∧, ∨ et ⊥.

	Règles d'introduction	Règles d'élimination
et	$(\wedge \mathrm{I})\frac{pq}{p\wedge q}$	$(\wedge \mathrm{E})\frac{p\wedge q}{p}\frac{p\wedge q}{q}$
ou	$(\vee \mathrm{I})\frac{p}{p\vee q}(\vee \mathrm{I})\frac{q}{p\vee q}$	$(\vee \mathrm{E})\frac{p\vee q\begin{array}{c}[p]\\ ⋮\\ r\end{array}\begin{array}{c}[q]\\ ⋮\\ r\end{array}}{r}$
implique	$(\to \mathrm{I})\frac{\stackrel{[p]}{\stackrel{⋮}{q}}}{p\to q}$	$(\to \mathrm{E})\frac{pp\to q}{q}$
faux	$(\mathrm{\perp }\mathrm{I})\frac{p\mathrm{\neg }p}{\mathrm{\perp }}$	$(\mathrm{\perp }\mathrm{E})\frac{\mathrm{\perp }}{p}$

La règle d'élimination de ⊥ a la particularité d'introduire une proposition. Comme souvent, on utilise la notation ¬p comme une abréviation de p → ⊥. Si l'on a une démonstration de p et une démonstration de q, on a une démonstration de p ∧ q, c'est ce qu'énonce la règle (∧ I). La règle (→ I) dit que si de l'hypothèse p on peut déduire q alors on peut déduire p → q, l'hypothèse p est alors enlevée de l'ensemble des hypothèses, on dit qu'elle est déchargée. Les deux règles d'élimination du connecteur ∧ énoncent que si l'on a une démonstration de p ∧ q on a immédiatement une démonstration de p (première règle) et on a aussi une démonstration de q (deuxième règle). La règle d'élimination de → est le modus ponens bien connu depuis Aristote. La règle (⊥ E) énonce le fait que de la proposition fausse on peut déduire n'importe quelle autre proposition. On remarque que la règle (⊥ E) est une règle d'élimination du connecteur ⊥.

Réduction à l'absurde

$(RAA)\frac{\stackrel{[\mathrm{\neg }p]}{\stackrel{⋮}{\perp }}}{p}$

La règle (RAA) est celle du raisonnement par l'absurde, c'est elle qui donne à la déduction naturelle son caractère non intuitionniste (c'est-à-dire « classique »). Dans ce cas, l'hypothèse ¬ p est déchargée. La règle (RAA) n'est pas une règle d'élimination, encore moins une règle d'introduction. On voit donc que cette règle créée un biais dans la régularité introduction-élimination de la déduction naturelle intuitionniste, rendant très malaisé de démontrer le théorème de normalisation. Il est probable que c'est cela qui a conduit Gentzen à développer le calcul des séquents.

L'article calcul des propositions donne une variante de la déduction naturelle avec des séquents spécifiques, dit « naturels », où les hypothèses sont gardées comme un contexte et où les hypothèses n'ont pas à être déchargées, mais disparaissent du contexte.

Exemples de démonstration

• Voici une démonstration en déduction naturelle de la formule p ∧ q → q ∧ p :

$\frac{\frac{\frac{[p\wedge q]}{q}(\wedge E)\frac{[p\wedge q]}{p}(\wedge E)}{q\wedge p}(\wedge I)}{p\wedge q\to q\wedge p}(\to I)$

L'hypothèse p ∧ q est déchargée par la règle $\to I$.

• Voici une démonstration en déduction naturelle de la formule ((p → ⊥) → ⊥) → p :

$\frac{\frac{\frac{[(p\to \mathrm{\perp })\to \mathrm{\perp }][p\to \mathrm{\perp }]}{\mathrm{\perp }}(\to E)}{p}(RAA)}{((p\to \mathrm{\perp })\to \mathrm{\perp })\to p}(\to I)$

L'hypothèse $p\to \mathrm{\perp }$ est déchargée par la règle de raisonnement par l'absurde (RAA). L'hypothèse $(p\to \mathrm{\perp })\to \mathrm{\perp }$ est déchargée par la règle d'introduction (→I).

Déduction naturelle en logique du premier ordre

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

	Règles d'introduction	Règles d'élimination
pour tout	$\frac{F}{\mathrm{\forall }xF}(\mathrm{\forall }I)$ à condition que la variable $x$ n'apparaisse dans aucune des hypothèses non déchargées.	$\frac{\mathrm{\forall }xF}{F[t/x]}(\mathrm{\forall }E)$
il existe	$\frac{F[t/x]}{\mathrm{\exists }xF}(\mathrm{\exists }I)$	$\frac{\mathrm{\exists }xF\begin{array}{c}[F]\\ ⋮\\ q\end{array}}{q}(\mathrm{\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 $F$.

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

Coupure en déduction naturelle

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é $q$ et que l'on dispose d'un théorème établissant que $p\to q$. On va alors se ramener à démontrer la propriété $p$ et au moyen d'une élimination de l'implication (modus ponens) en déduire la propriété $q$ cherchée. Formellement, on va construire la déduction suivante :

$\frac{\frac{⋮}{p\to q}\frac{⋮}{p}}{q}$

où à gauche figure la déduction du théorème et à droite une déduction de la proposition $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 :

$\frac{\frac{\stackrel{[p]}{⋮}}{q}}{p\to q}$

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

$\frac{\frac{\frac{\stackrel{[p]}{⋮}}{q}}{p\to q}\frac{⋮}{p}}{q}$

ce qui fait apparaître une coupure sur la formule $p\to 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é $p$ sous un ensemble fini d'hypothèse $p_1$, ..., $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.

Autres logiques

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

Bibliographie

• Modèle:En Stanislaw Jaśkowski. On the Rules of Suppositions in Formal Logic, 1934.
• Modèle:Ouvrage
• Modèle: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.)
• Modèle:En Dag Prawitz. Natural Deduction. Almqvist & Wiksell, Stockholm, 1965.
• J. Dopp, Logiques construites par une methode de deduction naturelle, Gauthier Villars, 1962, 196 pages
• Modèle:En Dirk van Dalen, Logic and Structure, Springer Verlag, 1994. Chapitre 2.8 Natural Dedduction, pages 90–95.
• Modèle:En Pelletier, Jeff, "A History of Natural Deduction and Elementary Logic Textbooks."
• Modèle:Ouvrage 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., Modèle:Date-. 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.

Voir aussi

Articles connexes

• Règle d'introduction (logique)
• Règle d'élimination (logique)

Lien externe

• Lévy, Michel, Prouveur en déduction naturelle propositionnelle
• Exercices de déduction naturelle, outil développé à l'ENS Rennes