déduction naturelle

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.