deduction theorem


In mathematical logic, the deduction theoremMathworldPlanetmath is the following (meta-)statement:

Δ,AB  iff  ΔAB,

where Δ is a set of formulasMathworldPlanetmathPlanetmath, and A,B are formulas in a logical system where is a (binary) logical connective denoting implicationMathworldPlanetmath or entailment. In words, the statement says that if the formula B is deducibleMathworldPlanetmath from a set Δ of assumptionsPlanetmathPlanetmath, together with the assumption A, then the formula AB is deducible from Δ alone. Conversely, if we can deduce AB from Δ, and if in addition we assume A, then B can be deduced. The deduction theorem conforms with our intuitive understanding of how mathematical proofs work: if we want to prove the statement “A implies B”, then by assuming A, if we can prove B, we have established “A implies B”.

The converse statement of the deduction theorem turns out to be a trivial consequence of modus ponensMathworldPlanetmath: if ΔAB, then certainly Δ,AAB. Since Δ,AA, we get, via modus ponens, Δ,AB as a result.

An apparently weaker version of the deduction theorem is to restrict Δ to a finite setMathworldPlanetmath. However, this version is actually equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath the original version:

Proof.

Clearly, the original version implies the version where Δ is finite. Now assume the “weaker” version and that Δ,AB, where Δ is an arbitrary set of formulas. Then there is a deduction (finite sequencePlanetmathPlanetmath of formulas)

A1,,An+1=B

such that each Ai (where in) is either an axiom, A itself, a formula in Δ, or a formula obtained from an application of an inference rule to earlier formula(s). Let Δ be the set of Ai’s which are in Δ. Then Δ is finite, and clearly the sequence above is a deduction with assumptions in Δ{A} and conclusionMathworldPlanetmath B. Thus Δ,AB. By our (meta)-assumption, ΔAB, which means that there is a deduction

B1,,Bm+1=AB

such that each Bj (where jm) is either an axiom, or a formula in Δ. Then certainly this is also a deduction with assumptions in Δ and conclusion AB. Therefore, ΔAB. ∎

The deduction theorem holds in most of the widely studied logical systems, such as classical propositional logicPlanetmathPlanetmath and predicate logic, intuitionistic logicMathworldPlanetmath, normal modal logics, to name a few. On the other hand, the deduction theorem fails for other systems such as fuzzy logicMathworldPlanetmath. 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

Δ,AB,ΓΔAB,Γ

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).

References

  • 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)
Title deduction theorem
Canonical name DeductionTheorem
Date of creation 2013-03-22 19:13:30
Last modified on 2013-03-22 19:13:30
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 15
Author CWoo (3771)
Entry type Feature
Classification msc 03F03
Classification msc 03B99
Classification msc 03B22
Classification msc 03B47