Déduction naturelle - Définition

Introduction

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.