# Deduction Theorem

## Theorem

Let $\mathscr H$ be instance 1 of a Hilbert proof system.

Then the deduction rule:

- $\dfrac{U,\mathbf A \vdash \mathbf B}{U \vdash \mathbf A \implies \mathbf B}$

is a derived rule for $\mathscr H$.

## Proof

For any proof of $U, \mathbf A \vdash \mathbf B$, we indicate how to transform it into a proof of $U \vdash \mathbf A \implies \mathbf B$ without using the deduction rule.

This is done by applying the Second Principle of Mathematical Induction to the length $n$ of the proof of $U,\mathbf A \vdash \mathbf B$.

If $n = 1$, then one of the following must occur:

In the first case, obviously $U \vdash \mathbf B$.

By **Axiom 1**, $U \vdash \mathbf B \implies \left({\mathbf A \implies \mathbf B}\right)$.

By Modus Ponens, $U \vdash \mathbf A \implies \mathbf B$.

In the second case, $U \vdash \mathbf A \implies \mathbf A$ by the Law of Identity.

Finally, in the third case, we have $U \vdash \mathbf B$.

As in the first case, we conclude $U \vdash \mathbf A \implies \mathbf B$.

If $n > 1$, the only other option for arriving at $U, \mathbf A \vdash \mathbf B$ is through Modus Ponens.

That is to say, two earlier lines of the proof contain:

- $U, \mathbf A \vdash \mathbf C$
- $U, \mathbf A \vdash \mathbf C \implies \mathbf B$

for some WFF $\mathbf C$.

But then these sequents have shorter proofs.

Hence, they satisfy the induction hypothesis.

Thus, we may infer:

- $U \vdash \mathbf A \implies \mathbf C$
- $U \vdash \mathbf A \implies \left({\mathbf C \implies \mathbf B}\right)$

This allows us to give the following proof of $U \vdash \mathbf A \implies \mathbf B$:

Line | Pool | Formula | Rule | Depends upon | Notes | |
---|---|---|---|---|---|---|

1 | $U \vdash \mathbf A \implies \mathbf C$ | Hypothesis | ||||

2 | $U \vdash \mathbf A \implies \left({\mathbf C \implies \mathbf B}\right)$ | Hypothesis | ||||

3 | $U \vdash \left({\mathbf A \implies \left({\mathbf C \implies \mathbf B}\right)}\right) \implies \left({\left({\mathbf A \implies \mathbf C}\right)\implies \left({\mathbf A \implies \mathbf B}\right)}\right)$ | Axiom 2 | ||||

4 | $U \vdash \left({\mathbf A \implies \mathbf C}\right)\implies \left({\mathbf A \implies \mathbf B}\right)$ | Modus Ponendo Ponens: $\implies \mathcal E$ | 2, 3 | |||

5 | $U \vdash \mathbf A \implies \mathbf B$ | Modus Ponendo Ponens: $\implies \mathcal E$ | 1, 4 |

The result follows by the Second Principle of Mathematical Induction.

$\blacksquare$

## Sources

- 2012: M. Ben-Ari:
*Mathematical Logic for Computer Science*(3rd ed.) ... (previous) ... (next): $\S 3.3.2$: Theorem $3.14$