In mathematical logic, the deduction theorem is the following (meta-)statement:
where is a set of formulas, and are formulas in a logical system where is a (binary) logical connective denoting implication or entailment. In words, the statement says that if the formula is deducible from a set of assumptions, together with the assumption , then the formula is deducible from alone. Conversely, if we can deduce from , and if in addition we assume , then can be deduced. The deduction theorem conforms with our intuitive understanding of how mathematical proofs work: if we want to prove the statement “ implies ”, then by assuming , if we can prove , we have established “ implies ”.
Clearly, the original version implies the version where is finite. Now assume the “weaker” version and that , where is an arbitrary set of formulas. Then there is a deduction (finite sequence of formulas)
such that each (where ) is either an axiom, itself, a formula in , or a formula obtained from an application of an inference rule to earlier formula(s). Let be the set of ’s which are in . Then is finite, and clearly the sequence above is a deduction with assumptions in and conclusion . Thus . By our (meta)-assumption, , which means that there is a deduction
such that each (where ) is either an axiom, or a formula in . Then certainly this is also a deduction with assumptions in and conclusion . Therefore, . ∎
The deduction theorem holds in most of the widely studied logical systems, such as classical propositional logic and predicate logic, intuitionistic logic, normal modal logics, to name a few. On the other hand, the deduction theorem fails for other systems such as fuzzy logic. A modified version of the deduction theorem is usually available, however.
Remark. In the statement of the deduction theorem, is taken to be a (finite) set, meaning that some of the proof-structural rules, such as the exchange rules, weakening rules, etc…, are assumed automatically. In substructural logics where some of these structural rules are absent, Gentzen’s sequent systems are employed. The form of the deduction theorem then becomes
This is often taken as an inference rule, because the “deduction theorem” usually fails in these logics. Here, is a finite sequence of formulas (as is ). The “deduction theorem” in this context is generally called the right -introduction rule (since the connective is introduced on the right hand side of the succedent).
- 1 J. W. Robbin, Mathematical Logic, A First Course, Dover Publication (2006)
- 2 A. S. Troelstra, H. Schwichtenberg, Basic Proof Theory, 2nd Edition, Cambridge University Press (2000)
- 3 G. Restall, An Introduction to Substructural Logics, Routledge, (2000)
- 4 M. Bergmann, An Introduction to Many-Valued and Fuzzy Logic, Cambridge University Press (2008)
|Date of creation||2013-03-22 19:13:30|
|Last modified on||2013-03-22 19:13:30|
|Last modified by||CWoo (3771)|