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 <math> E \vdash F <math>, then <math> \vdash E \rightarrow F. <math>
The deduction theorem may be generalized to a countable sequence of assumption formulas such that from
<math> E_1, E_2, ... , E_{n-1}, E_n \vdash F <math>, infer
<math> E_1, E_2, ... , E_{n-1} \vdash E_n \rightarrow F <math>, and so on until
<math> \vdash E_1\rightarrow(...(E_{n-1} \rightarrow (E_n \rightarrow F))...) <math>.
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 (http://www.ltn.lv/~podnieks/mlog/ml.htm) Podnieks is a comprehensive tutorial. See Section 1.5.