Deduction theorem

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. Deduction theorems exist for both propositional logic and first-order logic.^[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 ${\displaystyle B}$ is deducible from a set of assumptions ${\displaystyle \Delta \cup \{A\}}$ then the implication ${\displaystyle A\to B}$ is deducible from ${\displaystyle \Delta }$; in symbols, ${\displaystyle \Delta \cup \{A\}\vdash B}$ implies ${\displaystyle \Delta \vdash A\to B}$. In the special case where ${\displaystyle \Delta }$ is the empty set, the deduction theorem claim can be more compactly written as: ${\displaystyle A\vdash B}$ implies ${\displaystyle \vdash A\to B}$. The deduction theorem for predicate logic is similar, but comes with some extra constraints (that would for example be satisfied if ${\displaystyle A}$ is a closed formula). 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.

The deduction theorem holds for all first-order theories with the usual^[2] deductive systems for first-order logic.^[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.