In mathematical logic, the deduction theorem states that if a formula F is deducible from E then the implication E → F is demonstrable (i.e. it is "deducible" from the empty set). In symbols, if , then

The deduction theorem may be generalized to a countable sequence of assumption formulas such that from

, infer , and so on until

.

The deduction theorem is a meta-theorem: it is used to deduce proofs in a given theory though it is not a theorem of the theory itself.

See also

conditional proof, propositional calculus.

Reference

• Introduction to Mathematical Logic by Vilnis Detlovs and Karlis Podnieks Podnieks is a comprehensive tutorial. See Section 1.5.