nLab deduction theorem




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


Last revised on April 8, 2023 at 06:57:59. See the history of this page for a list of all contributions to it.