Déduction naturelle

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher
Page d'aide sur l'homonymie Pour les articles homonymes, voir Déduction.

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. L'introduction de la déduction naturelle est motivée par l'aspect peu canonique des systèmes à la Hilbert. 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[1] de l'isomorphisme de Curry-Howard.

Les origines de la déduction naturelle[modifier | modifier le code]

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[2].

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[3] 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 où 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[4] 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[5].

Les principes de la déduction naturelle[modifier | modifier le code]

Notion de règle[modifier | modifier le code]

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 :

permet de déduire à partir d'une démonstration de et d'un démonstration de . 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, et de sont des prémisses et est la conclusion.

Notion d'arbre de preuve[modifier | modifier le code]

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 :

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

Notion d'hypothèse[modifier | modifier le code]

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

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

Notion d'hypothèse déchargée[modifier | modifier le code]

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 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 . On note :

et les crochets dans signifie que l'hypothèse 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[modifier | modifier le code]

La règle se lit : de la prémisse p et la prémisse q, on conclut la formule (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 se lit : de la prémisse , 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[modifier | modifier le code]

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

  • Une présentation où les jugements sont des séquents de la forme contient les hypothèses actives et 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.

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

Déduction naturelle en logique propositionnelle[modifier | modifier le code]

Règles[modifier | modifier le code]

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

Règles d'introduction Règles d'élimination
et
ou
implique
faux

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 pq, 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 pq, 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 pq 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 si la règle (⊥ E) est une règle d'élimination du connecteur ⊥.

Réduction à l'absurde[modifier | modifier le code]

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 a 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[modifier | modifier le code]

  • Voici une démonstration en déduction naturelle de la formule p ∧ q → q ∧ p :
L'hypothèse p ∧ q est déchargée par la règle .
  • Voici une démonstration en déduction naturelle de la formule ((p → ⊥) → ⊥) → p :
L'hypothèse est déchargée par la règle de raisonnement par l'absurde (RAA). L'hypothèse est déchargée par la règle d'introduction (→I).

Déduction naturelle en logique du premier ordre[modifier | modifier le code]

En ce qui concerne la syntaxe, nous renvoyons à l'article calcul des prédicats. La notation désigne la formule dans laquelle toutes les occurrences libres de la variable dans sont remplacées par des occurrences du terme .

Règles d'introduction Règles d'élimination
pour tout

à condition que la variable n'apparaisse dans aucune des hypothèses non déchargées.

il existe
à 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

On notera l'analogie qui n'est pas fortuite entre les règles du connecteur et du quantificateur , d'une part, et du connecteur et du quantificateur d'autre part.

Coupure en déduction naturelle[modifier | modifier le code]

Les symétries s'exprimant à travers la dualité intro/élim 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 une succession d'une règle d'introduction suivi 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é et que l'on dispose d'un théorème établissant que , on va alors se ramener à démontrer la propriété et au moyen d'une élimination de l'implication (modus ponens) en déduire la propriété cherchée. Formellement on va construire la déduction suivante:

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

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

ce qui fait apparaître une coupure sur la formule .

La coupure est donc 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é sous un ensemble fini d'hypothèse , ..., , 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[modifier | modifier le code]

Il existe des systèmes de déduction naturelle pour des logiques modales[réf. nécessaire].

Références[modifier | modifier le code]

  1. Howard, W., The formulas--as--types notion of construction, in Essays on Combinatory Logic, Lambda Calculus, and Formalism, Seldin, J. P. and Hindley, J. R. ed., Academic Press (1980), pp. 479--490.
  2. Le théorème de déduction pallie ce défaut, mais au prix d'une explosion de la taille des déductions
  3. Typiquement les axiomes et qui servent à prouver le théorème de déduction.
  4. Notamment son Hauptsatz qui a comme conséquence la cohérence de la logique.
  5. (en) Dag Prawitz, Natural deduction: A proof-theoretical study, Mineola, New York, Dover Publications, [détail de l’édition] (ISBN 978-0-486-44655-4)
  6. « Cours de logique à l'ENS Lyon ».

Voir aussi[modifier | modifier le code]

Bibliographie[modifier | modifier le code]

  • (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,
  • (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.
  • (en) Dirk van Dalen, Logic and Structure, Springer Verlag, 1994.

Articles connexes[modifier | modifier le code]

Lien externe[modifier | modifier le code]

  • Prouveur : Un démonstrateur en ligne de formules