Un métathéorème qui relie la provabilité syntaxique à l'implication : si une formule B est démontrable à partir de l'hypothèse A (éventuellement avec d'autres hypothèses), alors l'implication A → B est démontrable dans le système formel environnant, sous réserve de conditions propres au système concernant la décharge des hypothèses.

Principe

Internalisation du raisonnement conditionnel : les preuves qui utilisent une hypothèse temporaire peuvent être converties en preuves d'une assertion conditionnelle en déchargeant cette hypothèse, reflétant ainsi la conséquence méta-théorique comme implication au niveau objet.

Démonstration

En logique propositionnelle, si en supposant P on parvient à dériver Q au moyen d'une preuve finie, alors on peut construire une preuve de P → Q sans supposer P ; par exemple, un sous-raisonnement qui part de «Supposons P» et aboutit à Q produit le théorème «P implique Q».

Mauvaise application

Appliquer le théorème de la déduction dans des systèmes où il échoue ou exige des restrictions (par ex. certaines logiques modales, systèmes avec hypothèses globales non déchargeables, ou contextes où les règles d'inférence empêchent la décharge), conduisant à des implications au niveau objet invalides.

Conséquence

Permet une construction modulaire des preuves, la formation de théorèmes à partir de raisonnements conditionnels et la mécanisation des preuves dépendant d'hypothèses ; il autorise le passage entre dérivations hypothétiques et théorèmes inconditionnels.

Inversion

La réciproque — si A → B est démontrable alors B est démontrable à partir de A — ne découle pas du théorème lui-même ; pour obtenir B à partir de A il faut encore supposer A ou que A soit démontrable indépendamment, généralement en appliquant modus ponens dans le système.

Limite

Valable dans de nombreux systèmes standards comme les logiques propositionnelle et du premier ordre classiques et intuitionnistes munies des règles usuelles d'introduction/élimination de l'implication, mais il échoue ou nécessite des aménagements dans certaines logiques modales, sous-structurales ou de pertinence et dans des systèmes aux contraintes d'inférence particulières.

Tension sémantique

Tension entre la transformabilité syntaxique garantie par le théorème de la déduction et l'entaillement sémantique : la provabilité à partir d'une hypothèse est une notion syntaxique dépendant des règles de preuve, tandis que l'implication sémantique peut tenir même lorsque le théorème de la déduction n'est pas applicable dans un calcul donné.

Synthèse

Le Théorème De La Déduction fait le pont entre la notion méta-niveau d'assumer des hypothèses pour obtenir des conclusions et la représentation au niveau objet de cette relation comme implication ; il facilite la construction de preuves lorsque la décharge des hypothèses est permise, mais son application exige le respect des conditions propres au système.