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