nLab deduction theorem

Idea

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 implication/function type in natural deduction.

References

• Wikipedia, Deduction theorem