In mathematical logic, a deduction theorem is a metatheorem that justifies doing conditional proofs from a hypothesis in systems that do not explicitly axiomatize that hypothesis, i.e. to prove an implication A → B, it is sufficient to assume A as a hypothesis and then proceed to derive B.
[1] The deduction theorem is an important tool in Hilbert-style deduction systems because it permits one to write more comprehensible and usually much shorter proofs than would be possible without it.
In certain other formal proof systems the same conveniency is provided by an explicit inference rule; for example natural deduction calls it implication introduction.
In more detail, the propositional logic deduction theorem states that if a formula
is the empty set, the deduction theorem claim can be more compactly written as:
The deduction theorem for predicate logic is similar, but comes with some extra constraints (that would for example be satisfied if
In general a deduction theorem needs to take into account all logical details of the theory under consideration, so each logical system technically needs its own deduction theorem, although the differences are usually minor.
[3] However, there are first-order systems in which new inference rules are added for which the deduction theorem fails.
[4] Most notably, the deduction theorem fails to hold in Birkhoff–von Neumann quantum logic, because the linear subspaces of a Hilbert space form a non-distributive lattice.
From the examples, one can see that we have added three virtual (or extra and temporary) rules of inference to our normal axiomatic logic.
The normal rules of inference (i.e. "modus ponens" and the various axioms) remain available.
Hypothesis is a step where one adds an additional premise to those already available.
This is shown by unindenting one level as follows:[b] In axiomatic versions of propositional logic, one usually has among the axiom schemas (where P, Q, and R are replaced by any propositions): These axiom schemas are chosen to enable one to derive the deduction theorem from them easily.
From these axiom schemas one can quickly deduce the theorem schema P→P (reflexivity of implication), which is used below: Suppose that we have that Γ and H together prove C, and we wish to show that Γ proves H→C.
If the step is the result of applying modus ponens to A and A→S, we first make sure that these have been converted to H→A and H→(A→S) and then we take the axiom 2, (H→(A→S))→((H→A)→(H→S)), and apply modus ponens to get (H→A)→(H→S) and then again to get H→S.
At the end of the proof we will have H→C as required, except that now it only depends on Γ, not on H. So the deduction step will disappear, consolidated into the previous step which was the conclusion derived from H. To minimize the complexity of the resulting proof, some preprocessing should be done before the conversion.
During the conversion, it may be useful to put all the applications of modus ponens to axiom 1 at the beginning of the deduction (right after the H→H step).
Similarly, if A→S is outside the scope of H, apply axiom 1, (A→S)→(H→(A→S)), and modus ponens to get H→(A→S).
Under the Curry–Howard correspondence, the above conversion process for the deduction meta-theorem is analogous to the conversion process from lambda calculus terms to terms of combinatory logic, where axiom 1 corresponds to the K combinator, and axiom 2 corresponds to the S combinator.
Note that the I combinator corresponds to the theorem schema P→P.
If one intends to convert a complicated proof using the deduction theorem to a straight-line proof not using the deduction theorem, then it would probably be useful to prove these theorems once and for all at the beginning and then use them to help with the conversion: helps convert the hypothesis steps.
helps convert modus ponens when the major premise is not dependent on the hypothesis, replaces axiom 2 while avoiding a use of axiom 1. helps convert modus ponens when the minor premise is not dependent on the hypothesis, replaces axiom 2 while avoiding a use of axiom 1.
Now let us assume the induction hypothesis for proofs of length up to n, and let
The deduction theorem is also valid in first-order logic in the following form: Here, the symbol
In the most common versions of the notion of formal proof, there are, in addition to the axiom schemes of propositional calculus (or the understanding that all tautologies of propositional calculus are to be taken as axiom schemes in their own right), quantifier axioms, and in addition to modus ponens, one additional rule of inference, known as the rule of generalization: "From K, infer ∀vK."
Steps that result from application of the rule of generalization are dealt with via the following quantifier axiom (valid whenever the variable v is not free in formula H): Since in our case F is assumed to be closed, we can take H to be F. This axiom allows one to deduce F→∀vK from F→K and generalization, which is just what is needed whenever the rule of generalization is applied to some K in the proof of G. In first-order logic, the restriction of that F be a closed formula can be relaxed given that the free variables in F has not been varied in the deduction of G from
In the case that a free variable v in F has been varied in the deduction, we write
(the superscript in the turnstile indicating that v has been varied) and the corresponding form of the deduction theorem is
[8] To illustrate how one can convert a natural deduction to the axiomatic form of proof, we apply it to the tautology Q→((Q→R)→R).
We normally use the natural-deductive form in place of the much longer axiomatic proof.