Logique et ensemblesNotion · Glossaire
déduction naturelle
La déduction naturelle est un système formel de logique où une preuve se construit à partir de prémisses et d’hypothèses temporaires, au moyen de règles d’introduction et d’élimination associées aux connecteurs et, en logique du premier ordre, aux quantificateurs. Elle rend explicites chaque étape du raisonnement et les hypothèses dont dépend une conclusion, ce qui facilite la vérification des preuves, notamment par ordinateur.
Sommaire
Ce que vous allez apprendre
- Distinguer les règles d'introduction des règles d'élimination.
- Suivre une dérivation complète de P et Q vers Q et P.
- Repérer une hypothèse non déchargée et distinguer validité formelle et vérité des prémisses.
- Différencier la déduction naturelle d'un système à la Hilbert.
En clair
Imaginez un raisonnement écrit comme une suite de petits gestes contrôlables. Si l'on sait « P et Q », on peut garder P ou garder Q. Inversement, si P et Q ont été établis séparément, on peut les réunir en « P et Q ».
La déduction naturelle organise une preuve avec de telles règles, adaptées à chaque mot logique. Elle décompose ainsi un raisonnement en étapes dont chacune indique précisément ce qui est utilisé et ce qui est obtenu.
Définition
La déduction naturelle est un système formel de règles d'inférence. Une dérivation part de prémisses ou d'hypothèses temporaires et produit une conclusion. À chaque connecteur logique, comme « et », « ou », « non » ou « si… alors… », correspondent des règles d'introduction et des règles d'élimination. Les premières construisent une formule ayant ce connecteur principal ; les secondes exploitent une formule qui le possède déjà.
Pour deux propositions nommées P et Q, l'introduction de la conjonction autorise le passage de P et de Q à . Son élimination autorise le passage de à P, ou à Q. Certaines règles ouvrent une hypothèse provisoire ; celle-ci doit être refermée, ou « déchargée », lorsque la règle qui en dépend est appliquée.
Dans la logique du premier ordre, aussi appelée calcul des prédicats, le même principe s'étend aux quantificateurs « pour tout » et « il existe ». Le choix précis des règles dépend de la logique formalisée, notamment classique ou intuitionniste. Le trait distinctif reste une preuve gouvernée par des règles locales plutôt que par un catalogue d'axiomes logiques à instancier.
Un exemple, pas à pas
On veut établir « Q et P » à partir de l'unique prémisse « P et Q ». Les lettres P et Q désignent deux propositions quelconques. La donnée est donc , et la conclusion visée est .
1. Appliquer l'élimination de la conjonction à la prémisse donne P.
2. Appliquer l'autre élimination de la conjonction à la même prémisse donne Q.
3. Appliquer l'introduction de la conjonction à Q puis à P donne . Un arbre de dérivation permet de vérifier quelles occurrences de la prémisse alimentent chaque branche.
Le contrôle se refait de bas en haut : la dernière règle exige Q et P, exactement les deux résultats obtenus aux étapes précédentes. La conclusion ne dépend d'aucune hypothèse supplémentaire.
En pratique
Écrire une preuve. On choisit la règle selon le connecteur principal de la conclusion ou d'une prémisse disponible. Une introduction convient pour construire le connecteur visé ; une élimination convient pour exploiter une formule déjà obtenue.
Relire un raisonnement. Pour chaque ligne, on repère les prémisses citées et la règle appliquée. Si une conclusion ne correspond pas exactement à la sortie de cette règle, l'étape doit être corrigée.
Faire vérifier une preuve. Un assistant de preuve encode les règles et contrôle chaque transition. Cette voie est préférable à une justification informelle lorsque la dérivation est longue ou que ses dépendances deviennent difficiles à suivre.
À ne pas confondre
Un système à la Hilbert. Il utilise typiquement de nombreux schémas d'axiomes et peu de règles d'inférence. La déduction naturelle emploie au contraire des règles d'introduction et d'élimination propres aux connecteurs. Si une preuve progresse surtout par instanciation d'axiomes logiques, elle relève du premier cadre.
Limites et pièges
Une hypothèse temporaire reste ouverte. Une conclusion peut alors dépendre d'elle sans que cette dépendance soit visible. Il faut marquer la portée de chaque hypothèse et vérifier que la règle appropriée la décharge avant d'annoncer une conclusion sans hypothèse.
Les prémisses ne sont pas automatiquement vraies. Une dérivation montre que la conclusion suit formellement des prémisses données. Si l'une d'elles est fausse dans la situation étudiée, la correction des règles ne suffit pas à garantir la vérité factuelle de la conclusion.
Les règles varient avec la logique choisie. Une règle admise en logique classique peut ne pas l'être en logique intuitionniste. Avant de réutiliser une dérivation, il faut identifier le calcul employé et contrôler que chacune de ses règles y est autorisée.
« Sans axiomes » demande une précision. La déduction naturelle évite les axiomes logiques caractéristiques des systèmes à la Hilbert, mais une preuve peut toujours partir de prémisses mathématiques ou d'hypothèses. Il faut donc distinguer les axiomes du calcul et les données de la démonstration.
Pour aller plus loin
axiome — Pour situer précisément ce qu'un système formel admet au départ et ce qu'une dérivation doit établir.
Raisonnement par l'absurde — Pour examiner une forme de raisonnement dont le statut dépend des règles et de la logique choisies.
Conjecture abc : la preuve que personne ne comprend sera vérifiée par ordinateur — Pour voir pourquoi la vérification informatique devient décisive face à une preuve difficile à contrôler humainement.
Explorez les mathématiques autrement
Retrouvez nos magazines, podcasts et jeux pour explorer les mathématiques autrement.
Découvrir les offres