deduction theorem holds for classical propositional logic

In this entry, we prove that the deduction theorem holds for classical propositional logic. For the logic, we use the axiom system found in this entry (http://planetmath.org/AxiomSystemForPropositionalLogic). To prove the theorem, we use the theorem schema $A\to A$ (whose deduction can be found here (http://planetmath.org/AxiomSystemForPropositionalLogic)).

Proof.

Suppose $A_1,\mathrm{\dots },A_n$ is a deduction of $B$ from $\mathrm{\Delta }\cup \{A\}$. We want to find a deduction of $A\to B$ from $\mathrm{\Delta }$. There are two main cases to consider:

• If $B$ is an axiom or in $\mathrm{\Delta }\cup \{A\}$, then

  $$B,B\to (A\to B),A\to B$$

  is a deduction of $A\to B$ from $\mathrm{\Delta }$, where $A\to B$ is obtained by modus ponens applied to $B$ and the axiom $B\to (A\to B)$. So $\mathrm{\Delta }⊢A\to B$.

• If $B$ is obtained from $A_i$ and $A_j$ by modus ponens. Then $A_j$, say, is $A_i\to B$. We use induction on the length $n$ of the deduction of $B$. Note that $n\ge 3$. If $n=3$, then the first two formulas are $C$ and $C\to B$.

  • If $C$ is $A$, then $C\to B$ is either an axiom or in $\mathrm{\Delta }$. So $A\to B$, which is just $C\to B$, is a deduction of $A\to B$ from $\mathrm{\Delta }$.

  • If $C\to B$ is $A$, then $C$ is either an axiom or in $\mathrm{\Delta }$, and

    $${ℰ}_0,(A\to A)\to ((A\to C)\to (A\to B)),C\to (A\to C),C,A\to C,A\to B$$

    is a deduction of $A\to B$ from $\mathrm{\Delta }$, where ${ℰ}_0$ is a deduction of $A\to A$, followed by two axiom instances, followed by $C$, followed by results of two applications of modus ponens.

  • If both $C$ and $C\to B$ are either axioms are in $\mathrm{\Delta }$, then

    $$C,C\to B,B,B\to (A\to B),A\to B$$

    is a deduction of $A\to B$ from $\mathrm{\Delta }$.

  Next, assume the deduction $ℰ$ of $B$ has length $n>3$.A subsequence of $ℰ$ is a deduction of $A_i\to B$ from $\mathrm{\Delta }\cup \{A\}$. This deduction has length less than $n$, so by induction,

  $$\mathrm{\Delta }⊢A\to (A_i\to B),$$

  and therefore by $(A\to (A_i\to B))\to ((A\to A_i)\to (A\to B))$, an axiom instance, and modus ponens,

  $$\mathrm{\Delta }⊢(A\to A_i)\to (A\to B).$$

  Likewise, a subsequence of $ℰ$ is a deduction of $A_i$, so by induction, $\mathrm{\Delta }⊢A\to A_i$. Therefore, an application of modus ponens gives us $\mathrm{\Delta }⊢A\to B$.

In both cases, $\mathrm{\Delta }⊢A\to B$ and we are done.∎

We record two corollaries:

Corollary 1.

(Proof by Contradiction). If $\mathrm{\Delta }\mathrm{,}A\mathrm{⊢}\mathrm{⟂}$, then $\mathrm{\Delta }\mathrm{⊢}\mathrm{\neg }\mathit{}A$.

Proof.

From $\mathrm{\Delta },A⊢⟂$, we have $\mathrm{\Delta }⊢A\to ⟂$ by the deduction theorem. Since $\mathrm{\neg }A\leftrightarrow ⟂$, the result follows. ∎

Corollary 2.

(Proof by Contrapositive). If $\mathrm{\Delta }\mathrm{,}A\mathrm{⊢}\mathrm{\neg }\mathit{}B$, then $\mathrm{\Delta }\mathrm{,}B\mathrm{⊢}\mathrm{\neg }\mathit{}A$.

Proof.

If $\mathrm{\Delta },A⊢\mathrm{\neg }B$, then $\mathrm{\Delta },A,B⊢⟂$ by the deduction thereom, and therefore $\mathrm{\Delta },B⊢\mathrm{\neg }A$ by the deduction theorem again. ∎

Remark The deduction theorem for the classical propositional logic can be used to prove the deduction theorem for the classical first and second order predicate logic.