Deduction theorem

Remarks

The direction from right to left is one step of modus ponens. For the other direction, take a derivation $\psi_1, \dots, \psi_n = \psi$ from $\Gamma \cup \set{\varphi}$. Show by induction on $i$ that $\Gamma \vdash \varphi \to \psi_i$. If $\psi_i$ is an axiom or in $\Gamma$, use axiom 1, $\psi_i \to (\varphi \to \psi_i)$; if $\psi_i = \varphi$, use the derivation of $\varphi \to \varphi$. If $\psi_i$ comes by modus ponens from $\psi_j$ and $\psi_j \to \psi_i$, use axiom 2 and modus ponens twice. For example, from $\set{p \to q, \; q \to r, \; p} \vdash r$, which takes two steps of modus ponens, the theorem gives $\set{p \to q, \; q \to r} \vdash p \to r$. In first-order logic with the rule of generalization, the theorem needs a hypothesis. It holds when $\varphi$ is a sentence, or more generally when the derivation never generalizes on a variable free in $\varphi$. Without this, $\set{P(x)} \vdash \forall x \, P(x)$ holds, but $P(x) \to \forall x \, P(x)$ is not valid.

Going deeper

For a student

The deduction theorem connects the turnstile $\vdash$ with the connective $\to$. It is the reason that proofs in a Hilbert system can be built from proofs under hypotheses, which keeps them manageable. In natural deduction the same principle is a primitive rule, implication introduction. Its semantic counterpart is that $\Gamma \cup \set{\varphi} \models \psi$ if and only if $\Gamma \models \varphi \to \psi$, for logical consequence.