The Deduction Theorem — Mathematics Knowledge System

Overview

The deduction theorem is a metatheorem — a theorem about a formal proof system rather than a theorem stated within it — asserting that Γ ∪ {φ} ⊢ ψ if and only if Γ ⊢ φ → ψ. In Hilbert-style systems, where the only inference rule is typically modus ponens and there is no built-in way to 'assume and discharge' a hypothesis, this equivalence is not automatic; it must be proved, by an induction on the length of the derivation of ψ from Γ ∪ {φ}, showing how to systematically eliminate φ as a bare assumption and replace every line of the original derivation with a corresponding derivation of φ → (that line), using only the axioms and modus ponens. The theorem is what licenses the informal habit, universal in ordinary mathematics, of writing 'assume φ; ...; therefore φ → ψ' — in a Hilbert system that convenience must be earned by the theorem's proof, whereas in natural deduction the analogous move (→-introduction) is simply built directly into the system as a primitive rule. The deduction theorem's converse direction is essentially just one application of modus ponens, so the mathematical content lies entirely in the forward direction.

Intuition

In natural deduction, 'assume φ, derive ψ, conclude φ → ψ' is a primitive move built into the system by fiat — the →-introduction rule. Hilbert-style systems refuse to build in any such shortcut; they insist on deriving everything from a tiny stock of axiom schemas and modus ponens alone, so the deduction theorem has to prove, after the fact, that this convenient shortcut is nevertheless always available: whatever you could derive from Γ plus a temporary hypothesis φ, you could instead have derived as an implication φ → ψ from Γ alone, using only the sanctioned machinery. The proof works by literally rewriting the derivation line by line, prefixing 'φ →' onto every line and patching each step with the K and S axiom schemas so that modus ponens still goes through — a completely mechanical, if tedious, translation.

Formal Definition

Definition

For a Hilbert-style system with modus ponens as its sole rule of inference (and axiom schemas including at least the two below), the deduction theorem states:

\Gamma \cup \{\varphi\} \vdash \psi \iff \Gamma \vdash \varphi \rightarrow \psi

The deduction theorem

\varphi \rightarrow (\psi \rightarrow \varphi) \quad \text{(axiom schema K)}

Used in the base case where ψ is an axiom or premise other than φ

(\varphi \rightarrow (\psi \rightarrow \chi)) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \chi)) \quad \text{(axiom schema S)}

Used in the inductive case where ψ was obtained by modus ponens

\vdash \varphi \rightarrow \varphi \quad \text{(base case: } \psi = \varphi \text{, so } \Gamma \cup \{\varphi\} \vdash \varphi \text{ trivially, giving } \Gamma \vdash \varphi \rightarrow \varphi\text{)}

Immediate corollary

Worked Examples

Any set of formulas including p as a hypothesis derives p in one step (reiterating the hypothesis).
$\Gamma \cup \{p\} \vdash p$
Apply the deduction theorem directly, moving the hypothesis p across the turnstile as an antecedent.
$\Gamma \vdash p \rightarrow p$

Answer: ⊢ p → p follows immediately from the deduction theorem applied to the trivial derivation Γ ∪ {p} ⊢ p, without needing to explicitly invoke axiom schemas K and S.

Practice Problems

Difficulty 3/10

State the deduction theorem precisely, using ⊢ and set notation for the premises.

Difficulty 4/10

Why is the deduction theorem's converse direction (Γ ⊢ φ→ψ implies Γ∪{φ}⊢ψ) considered the 'easy' half?

Difficulty 7/10

Sketch the inductive proof of the forward direction of the deduction theorem, for the case where ψ is obtained from an earlier line χ→ψ and χ by modus ponens.

Quiz

Summary

The deduction theorem: Γ ∪ {φ} ⊢ ψ if and only if Γ ⊢ φ → ψ, in any Hilbert-style system with modus ponens as its sole inference rule.
The backward direction is one modus ponens step; the forward direction requires induction on the derivation, using axiom schemas like K and S to rewrite each line with 'φ →' prefixed.
It justifies the everyday habit of conditional proof ('assume φ; derive ψ; conclude φ→ψ'), a move that natural deduction instead builds in directly as the primitive rule →-introduction.

References

WebsiteWikipedia — Deduction theorem