< ^ >
Part I: Propositional Logic Introduction to Formal Logic

4. Deduction theorem

4.1. Formulas provable under a set of hypotheses

The axiomatic system presented in the previous chapter has the merit of providing a formal definition to the notion of provable proposition. The formal proofs we obtain, however, are not quite intuitive. For instance, the fact that $α → α$ stands for a true proposition (and therefore should be provable) seems to be obvious. In contrast, the formal derivation of it that is given at the end of Chapter 3 is rather involved. Consequently, we need to seek other tools in order to establish the formal derivability of propositions. Introducing the notion of provability under a set of hypotheses is a first step towards this end.
Let $Γ$ be a set of formulas. The set of formulas provable under the set of hypotheses $Γ$ (in short, provable under $Γ$) is inductively defined as follows:
  1. Every hypothesis $α ∈ Γ$ is provable under $Γ$.
  2. Every axiom is provable under $Γ$.
  3. If $((α_0, …, α_n),α)$ is an inference rule, and if $α_0$, ..., and $α_n$ are provable under $Γ$, so is $α$.
When a formula $α$ is provable under a set of hypotheses $Γ$, one writes $Γ ⊢ α$.

4.2. Inference rules under sets of hypotheses

When writing expressions of the form $Γ ⊢ α$, it is usual to write the set of hypotheses $Γ$ as a sequence of formulas. Accordingly, one writes $Γ, α$ instead of $Γ ∪ \text'{' α \text'}'$. For instance, one may write expressions such as the following:
$a, a → b ⊢ b$    $Γ, α ⊢ α$
Then, combining the above notation with the fraction-like notation used for the inference rules, one may depict inference rules under sets of hypotheses. For instance modus ponens under a set of hypotheses $Γ$ may be written as follows:
$Γ ⊢ α$ $Γ ⊢ α → β$
$Γ ⊢ β$
The above conventions allow a derivation under a set of hypotheses to be presented as a derivation tree whose leaves and nodes are expressions of the form $Γ ⊢ α$. For instance, the following tree establishes that $α ∧ β ⊢ β ∧ α$:
$α ∧ β ⊢ α ∧ β$ $α ∧ β ⊢ (α ∧ β) → β$
$α ∧ β ⊢ α ∧ β$ $α ∧ β ⊢ (α ∧ β) → α$ $α ∧ β ⊢ β$ $α ∧ β ⊢ β → α → (β ∧ α)$
$α ∧ β ⊢ α$ $α ∧ β ⊢ α → (β ∧ α)$
$α ∧ β ⊢ β ∧ α$
Remark that in such a tree, the leaves are expressions of the form $Γ ⊢ α$ where $α$ is either an axiom or an hypothesis (i.e., in the second case, $α ∈ Γ$).

4.3. Deduction theorem

The mathematical expression $α ⊢ β$ may be paraphrased by saying that "$α$ entails $β$". Intuitively, the notions of implication and entailment are rather similar. In fact, it happens that if $α$ entails $β$ then $α → β$ is derivable. This fundamental result is established by the next proposition, which is known as the deduction theorem.
Let $α$ and $β$ be two formulas, and let $Γ$ be a set of formulas. If $Γ, α ⊢ β$ then $Γ ⊢ α → β$.
The proof proceeds by induction on the definition of a formula provable under a set of hypotheses
  1. $Γ, α ⊢ β$ because $β$ is a hypothesis.
    There are two subcases:
    1.1. $β ∈ Γ$
    Since $β ∈ Γ$, we have that $Γ ⊢ β$. We may then conclude as follows:
    $Γ ⊢ β$ $Γ ⊢ β → α → β$
    $Γ ⊢ α → β$
    1.2. $β = α$
    We have to show that $Γ ⊢ α → α$. This may be established as follows:
    $Γ ⊢ α → (β→α) → α$ $Γ ⊢ (α → (β→α) → α) → (α → β→α) → α → α$
    $Γ ⊢ α → β→α$ $Γ ⊢ (α → β→α) → α → α$
    $Γ ⊢ α → α$
  2. $Γ, α ⊢ β$ because $β$ is an axiom.
    Similarly to Case 1.1, mutatis mutandis.
  3. $Γ, α ⊢ β$ is the conclusion of an inference rule.
    In this case, there exists a formula $γ$ such that the derivation of $Γ, α ⊢ β$ ends up as follows:
    ⋮ ⋮
    $Γ, α ⊢ γ$ $Γ, α ⊢ γ → β$
    $Γ, α ⊢ β$
    By induction hypothesis, we have that $Γ ⊢ α → γ$ and $Γ ⊢ α → γ → β$. We may then conclude as follows:
    ⋮
    ⋮ $Γ ⊢ α → γ → β$ $Γ ⊢ (α → γ → β) → (α → γ) → α → β$
    $Γ ⊢ α → γ$ $Γ ⊢ (α → γ) → α → β$
    $Γ ⊢ α → β$
Using the notation that has been introduced for writing an inference rule under a set of hypotheses, the deduction theorem may be turned into the following rule:
$Γ, α ⊢ β$
$Γ ⊢ α → β$
We may then prove that $(α ∧ β)→(β ∧ α)$ is derivable by completing the derivation example of Section 4.2 as follows:
$α ∧ β ⊢ α ∧ β$ $α ∧ β ⊢ (α ∧ β) → β$
$α ∧ β ⊢ α ∧ β$ $α ∧ β ⊢ (α ∧ β) → α$ $α ∧ β ⊢ β$ $α ∧ β ⊢ β → α → (β ∧ α)$
$α ∧ β ⊢ α$ $α ∧ β ⊢ α → (β ∧ α)$
$α ∧ β ⊢ β ∧ α$
$⊢ (α ∧ β) → (β ∧ α)$