Théorème de la Déduction

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.