Deduction theorem

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 $E \vdash F$ , then $\vdash E \rightarrow F.$

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

$E_1, E_2, ... , E_{n-1}, E_n \vdash F$ , infer $E_1, E_2, ... , E_{n-1} \vdash E_n \rightarrow F$ , and so on until

$\vdash E_1\rightarrow(...(E_{n-1} \rightarrow (E_n \rightarrow F))...)$ .

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.

Reference

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

Categories: Logic

Deduction theorem

See also

Reference