nLab
deduction theorem

Contents

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 BB from the premise AA, then there is also a proof of the conditional statement ABA \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.

References

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