The *deduction theorem* in formal logic says (when it holds) that if in some logical framework there is a proof by deduction of some proposition $B$ from the premise $A$, then there is also a proof of the conditional statement $A \to B$ (from no premises).

This hence relates entailment in the metalanguage with implication in the object language.

This seems obvious, but there are formal logical systems where this fails, for instance in the original Birkhoff-vonNeumann quantum logic. On the other hand, it may be taken as an axiom; it is the introduction rule for the conditional operator in natural deduction.

- Wikipedia,
*Deduction theorem*

Last revised on January 26, 2014 at 04:20:06. See the history of this page for a list of all contributions to it.