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.

L’histoire des théories de la déduction a suivi un cheminement curieux[pas clair]. De nombreux logiciens dont Bertrand Russell et Alfred North Whitehead avec leurs Principia Mathematica ont développé la logique sous une forme axiomatique. Les lois logiques sont déduites à partir d’axiomes logiques, d’une façon qui ressemble à la méthode euclidienne, au moins aux yeux de ceux qui faisaient ces déductions[Qui ?]. Cette méthode pouvait sembler relativement naturelle tant qu’on choisissait comme axiomes des lois dont la vérité logique était évidente. Mais le souci de formuler des systèmes d’axiomes aussi réduits que possible a conduit parfois à des formalismes où l’on déduit des vérités logiques évidentes à partir d’autres qui ne le sont pas. Les méthodes des logiciens[Qui ?] permettaient de justifier tous les raisonnements dont la validité était reconnue mais elles étaient très éloignées de l’idéal d’évidence naturelle que l’on attend de la logique.

La notion de « naturel » est employé par les logiciens[Qui ?] principalement en deux sens. S’il s’agit comme ci-dessus d’évidence naturelle, ou de concepts apparentés comme la déduction naturelle[pas clair], on veut insister sur leur caractère universel et nécessaire pour tout être rationnel[pas clair]. On peut vivre sans jamais savoir que 2+2 = 4 mais on ne peut pas être rationnel sans reconnaître que 2+2 = 4 est nécessaire, dès qu’on nous a appris à le dire[pas clair]. Le second sens de la notion de naturel intervient dans la distinction entre les langues naturelles et les langues formelles, ou artificielles. Les premières sont les langues qui nous sont familières, elles ont été façonnées par des siècles de culture. Les secondes sont inventées par les logiciens pour développer des théories et pour donner des preuves.[pas clair]

Gerhard Gentzen est le premier à avoir développé des formalismes qui redonnent à la logique le caractère d’un cheminement naturel[pas clair]. La principale idée de départ de Gentzen était simple : pas d’axiomes logiques, que des règles de déduction et autant qu’il en faut pour reproduire toutes les formes élémentaires et naturelles de raisonnement. Pour réaliser cette idée, Gentzen a 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 est très suggestive pour l’intuition et elle a conduit Gentzen à faire de belles découvertes[Lesquels ?] 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 renonçant aux déductions arborescentes[réf. nécessaire]. Les déductions de Fitch ne sont cependant pas de simples suites de phrases. Pour donner à une déduction un caractère naturel[pas clair] il faut faire apparaître des relations de dépendance entre les phrases. Au lieu d’une forme arborescente le style de Fitch se sert seulement de barres verticales. Une assertion dépend des phrases qui sont au-dessus d’elle sauf de celles qui sont décalées sur la droite par ces barres. Cette règle simple permet de faire des déductions à la fois formelles et naturelles. Pour le style de Fitch nous renvoyons à l'article qui lui est dédié[Lequel ?] et nous présentons, dans l'article ci-dessous, la méthode originelle de Gentzen.

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[réf. nécessaire].

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 :

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'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 s'écrit :

contient des applications de règles.

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 du fait que le sol est glissant, avec comme hypothèses qu'il pleut, que s'il pleut alors le sol est mouillé et que si le sol est mouillé alors le sol est glissant :

La règle y est appliquée deux fois.

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 de maintenant. 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.

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.

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

Les deux règles qui éliminent ⊥ ont la particularité d'introduire une proposition. Comme souvent, on utilise la notation ¬p comme une abréviation de p → ⊥. La règle de raisonnement par l'absurde (RAA) (reductio ad absurdum) décharge également une hypothèse. 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 (⊥) énonce le fait que de la proposition fausse on peut déduire n'importe quelle autre proposition. 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. On remarquera cependant que si la règle (⊥) peut être vue comme une règle d'élimination du connecteur ⊥, 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.

La page 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).

Discussions[modifier | modifier le code]

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]

Différentes présentations des règles et des démonstrations[modifier | modifier le code]

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

  • Une présentation « à la Prawitz » en arbre de preuve où les hypothèses chargées sont aux feuilles uniquement (c'est la présentation utilisée dans cette article).

  • Une présentation où les jugements sont de la forme contient les hypothèses chargées et est la formule démontrée.

  • 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

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