Deduction theorem

In mathematical logic, the deduction theorem states that if a conclusion can be inferred (by means of some inference rule) from a premise, then it is possible to assert that the premise implies the conclusion.

In symbolic form, the deduction theorem says that if

<math> p \vdash q, <math>

then

<math> \vdash p \rightarrow q. <math>

DT can be used on an argument or a proof which contains any number of hypotheses: from

<math> p_1, p_2, ... , p_{n-1}, p_n \vdash q <math>

one can apply DT to deduce

<math> p_1, p_2, ... , p_{n-1} \vdash p_n \rightarrow q. <math>

Applying DT again yields

<math> p_1, p_2, ... , p_{n-2} \vdash p_{n-1} \rightarrow (p_n \rightarrow q) <math>.

If modus ponens is the only inference rule allowed in a given logical language or theory then there are no restrictions on the use of DT, but if Generalization is used then DT must not be used to implicate a premise which contains a variable which became Generalized in the proof.

Strict formal proofs do not allow the use of DT, nor do they allow the use of theorems proven previously unless the entire proof of the previously proved theorem is included in the new proof. However, such proofs are very hard. The use of DT is a very useful aid to theorem proving (of logical theorems, that is). But DT is a meta-theorem: it is used to deduce the existence of a proof in a given theory from an already existing proof in the given theory, but it does not belong to the theory itself. DT is similar in this sense to mathematical induction: it is a quantum leap of logic.

See also: conditional proof, propositional calculus.

Reference

• ] Podnieks is a comprehensive tutorial. See Section 1.5.