Déduction naturelle

Pour les articles homonymes, voir Déduction.

La déduction naturelle est un système formel proposé par Gerhard Gentzen en 1934 pour représenter les preuves en logique du premier ordre de manière aussi proche que possible des façons naturelles de raisonner. L'introduction de la déduction naturelle motivée par l'aspect peu canonique des systèmes à la Hilbert est une étape importante de l'histoire de la théorie de la démonstration pour plusieurs raisons :

• contrairement aux systèmes à la Hilbert basé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 : chaque connecteur est défini par 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, 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.

Les origines de la déduction naturelle

L’histoire des théories de la déduction a suivi un cheminement curieux. 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. 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 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 principalement en deux sens. S’il s’agit comme ci-dessus d’évidence naturelle, ou de concepts apparentés comme la déduction naturelle, on veut insister sur leur caractère universel et nécessaire pour tout être rationnel. 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. 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.

Gerhard Gentzen est le premier à avoir développé des formalismes qui redonnent à la logique le caractère d’un cheminement naturel. 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 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. Les déductions de Fitch ne sont cependant pas de simples suites de phrases. Pour donner à une déduction un caractère naturel 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é et nous présentons, dans l'article ci-dessus, 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.

Les principes de la déduction naturelle

La déduction naturelle fait des raisonnements sous des hypothèses. La démonstration de q sous l'hypothèse p s'écrit:

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 on rencontre la règle :

Les règles fondamentales de la déduction naturelle

Les propositions au-dessus de la barre s'appellent les prémisses et la proposition sous la barre s'appelle la conclusion. La règle ci-dessus élimine le connecteur →. En fait, dans la déduction naturelle, il y a deux types de règles: des règles d'introduction et des règles d'élimination. Nous allons, dans un premier temps, présenter les règles qui régissent les connecteurs →, ∧ et ⊥.

L'hypothèse

Les règles d'introduction

Dans la règle d'introduction de la flèche l'hypothèse p est déchargée, ce qui se dénote en la mettant entre crochets.

Les règles d'élimination

Les règles qui régissent ⊥ (faux)

Ce sont deux règles qui éliminent ⊥, mais qui 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 (reductio ad absurdum) décharge également une hypothèse.

La signification des règles

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 ∧ énonce 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.

Quelques exemples

• Soit à démontrer p ∧ q → q ∧ p.

Les deux hypothèses sont déchargées par la règle .

• Démontrons ¬¬p → p autrement dit ((p → ⊥) → ⊥) → p.

Ici les deux hypothèses sont déchargées chacune par une règle différente : l'hypothèse est déchargée par la règle d'introduction de la flèche, l'hypothèse par la règle de raisonnement par l'absurde.

Les autres connecteurs et les quantificateurs

Les règles de la disjonction

Introduction

Élimination

Cette règle décharge les deux hypothèse p et q.

Les règles de la quantification universelle

En ce qui concerne la syntaxe, nous renvoyons à l'article calcul des prédicats. Nous ne donnons que les règles.

Introduction

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

Élimination

Les règles de la quantification existentielle

Introduction

Élimination

Cette règle décharge l'hypothèse P

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.

La notation P[a / x] désigne la formule P dans laquelle toutes les occurrences libres de la variable x dans P sont remplacées par des occurrences du terme a.

Coupure en déduction naturelle

Références

• (en) Dirk van Dalen, Logic and Structure, Springer Verlag, 1994.

Voir aussi

• Calcul des prédicats
• Calcul des propositions
• Logique classique
• Calcul des séquents
• Logique intuitionniste
• Théorème de complétude

Lien externe

• prouveur Un démonstrateur en ligne de formules

• Portail des mathématiques
• Portail de la logique
• Portail de l’informatique