---
tag: 9X08XK5RV2
kind: statement
role: theorem
name: Deduction theorem
msc: [03B05, 03F03]
uses: [1MGMQX43B8, 0NMG7W7Q11]
about: [1MGMQX43B8]
sources:
  - url: https://en.wikipedia.org/wiki/Deduction_theorem
same_as:
  wikidata: Q1182249
  wikipedia: Deduction theorem
---

## Statement

Consider the standard [[Hilbert system|1MGMQX43B8]] for propositional logic, with modus ponens as its only rule.
Let $\Gamma$ be a set of formulas, and let $\varphi$ and $\psi$ be formulas.
Then $\Gamma \cup \set{\varphi} \vdash \psi$ if and only if $\Gamma \vdash \varphi \to \psi$.

## 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.

## Explanations

### L1 human

The theorem says that "assume $\varphi$ and prove $\psi$" is a correct way to prove "if $\varphi$ then $\psi$".
Mathematicians use this all the time without thinking.
The theorem shows that a Hilbert system, which has no rule for assumptions, still allows it.

### L2 human

The deduction theorem connects the turnstile $\vdash$ with the connective $\to$.
It is the reason that proofs in a [[Hilbert system|1MGMQX43B8]] can be built from proofs under hypotheses, which keeps them manageable.
In [[natural deduction|6KT3BJZ7D1]] 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|1HK0VYWTV7]].