# Deduction Theorem for Hilbert Proof System for Predicate Logic

## Theorem

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

Then the deduction rule:

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

is a derived rule for provable consequences in $\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$.

By definition of $\mathscr H$, then one of the following must occur:

• $\mathbf B \in U$
• $\mathbf B$ is an axiom of $\mathscr H$
• $\mathbf B = \mathbf A$
• $\mathbf B$ is derived from Modus Ponens

In the first two cases, we can craft the following proof of $U \vdash \mathbf A \implies \mathbf B$:

$U \vdash \mathbf A \implies \mathbf B$
Line Pool Formula Rule Depends upon Notes
1 $\mathbf B$ Axiom of $\map {\mathscr H} U$ (None) By definition of provable consequence
2 $\mathbf B \implies \paren{ \mathbf A \implies \mathbf B }$ Axiom 1 (None) True Statement is Implied by Every Statement
3 $\mathbf A \implies \mathbf B$ Modus Ponendo Ponens: $\implies \mathcal E$ 1, 2

$\Box$

Next, if $\mathbf B = \mathbf A$, then $\mathbf A \implies \mathbf B$ is a tautology, and hence satisfies axiom 1 of $\mathscr H$.

$\Box$

Lastly, suppose that $\mathbf B$ is derived from Modus Ponens, so that we have $\mathbf B'$ and $\mathbf B' \implies \mathbf B$ as provable consequences of $U, \mathbf A$.

By the induction hypothesis, we have proofs of $U \vdash \mathbf A \implies \mathbf B'$ and $U \vdash \mathbf A \implies \paren{ \mathbf B' \implies \mathbf B }$.

Then, expanding upon these proofs:

$U \vdash \mathbf A \implies \mathbf B$
Line Pool Formula Rule Depends upon Notes
1 $\mathbf A \implies \mathbf B'$ Induction Hypothesis (None)
2 $\mathbf A \implies \paren{ \mathbf B' \implies \mathbf B }$ Induction Hypothesis (None)
3 $\mathbf A \implies \paren{ \mathbf B' \implies \mathbf B } \implies \paren{ \paren{ \mathbf A \implies \mathbf B' } \implies \paren{ \mathbf A \implies \mathbf B } }$ Axiom 1 (None) Self-Distributive Law for Conditional
4 $\paren{ \mathbf A \implies \mathbf B' } \implies \paren{ \mathbf A \implies \mathbf B }$ Modus Ponendo Ponens: $\implies \mathcal E$ 2, 3
5 $\mathbf A \implies \mathbf B$ Modus Ponendo Ponens: $\implies \mathcal E$ 1, 4

$\Box$

Hence the result by the Second Principle of Mathematical Induction.

$\blacksquare$