Une technique de calcul des preuves qui dérive des conclusions à partir d'hypothèses en appliquant des règles d'introduction et d'élimination pour chaque connecteur logique et quantificateur ; les preuves sont organisées en enchaînements d'applications de règles plutôt qu'en instanciations de schémas d'axiomes.

Principe

Chaque connecteur logique et quantificateur est régi par des règles complémentaires d'introduction et d'élimination permettant des pas locaux préservant le sens, conduisant des hypothèses aux conclusions.

Démonstration

Pour prouver A ∧ B à partir d'hypothèses, on applique l'introduction de la conjonction (∧-intro) en démontrant séparément A et B ; pour exploiter A ∧ B, on utilise l'élimination de la conjonction (∧-elim) pour obtenir l'un des conjonctes lorsque nécessaire.

Mauvaise application

Considérer les règles d'introduction/élimination comme des heuristiques facultatives et omettre la libération d'hypothèses temporaires (par exemple ne pas libérer une hypothèse dans →-intro) conduit à des preuves invalides ou non fermées.

Conséquence

Correctement utilisée, la déduction naturelle produit des preuves reflétant le rôle inférentiel des connecteurs, facilite la lisibilité, correspond à un raisonnement informel et rend applicables les procédés de normalisation (élimination des coupes / réduction de preuve).

Inversion

L'inverse est un calcul axiomatique qui déduit des théorèmes à partir d'un ensemble fixe de schémas d'axiomes et de quelques règles d'inférence ; au lieu de règles locales d'introduction/élimination, il construit des chaînes globales depuis les axiomes.

Limite

S'applique principalement aux logiques propositionnelle et du premier ordre avec règles d'introduction/élimination bien définies ; les extensions (modales, sous-structurales) exigent des règles adaptées et peuvent rompre certaines propriétés de normalisation.

Tension sémantique

Entre en tension avec les systèmes hilbertiens : la déduction naturelle met l'accent sur le sens et la structure locale des règles, tandis que les systèmes hilbertiens privilégient des ensembles minimaux de règles et la compacité de la dérivabilité.

Synthèse

La déduction naturelle est un cadre de preuve fondé sur des règles où chaque opérateur logique possède des règles jumelées permettant de construire et déconstruire des formules pas à pas, produisant des preuves qui incarnent le rôle inférentiel des opérateurs.