Natural Deduction - Hypothetical Derivations

Hypothetical Derivations

A pervasive operation in mathematical logic is reasoning from assumptions. For example, consider the following derivation:

$\cfrac{A \wedge \left ( B \wedge C \right ) \ true}{\cfrac{B \wedge C \ true}{B \ true} \wedge_{ E_1}} \wedge_{ E_2}$

This derivation does not establish the truth of B as such; rather, it establishes the following fact:

If A ∧ (B ∧ C) is true then B is true.

In logic, one says "assuming A ∧ (B ∧ C) is true, we show that B is true"; in other words, the judgement "B true" depends on the assumed judgement "A ∧ (B ∧ C) true". This is a hypothetical derivation, which we write as follows:

$\begin{matrix} A \wedge \left ( B \wedge C \right ) \ true \\ \vdots \\ B \ true \end{matrix}$

The interpretation is: "B true is derivable from A ∧ (B ∧ C) true". Of course, in this specific example we actually know the derivation of "B true" from "A ∧ (B ∧ C) true", but in general we may not a-priori know the derivation. The general form of a hypothetical derivation is:

$\begin{matrix} D_1 \quad D_2 \cdots D_n \\ \vdots \\ J \end{matrix}$

Each hypothetical derivation has a collection of antecedent derivations (the D_i) written on the top line, and a succedent judgement (J) written on the bottom line. Each of the premises may itself be a hypothetical derivation. (For simplicity, we treat a judgement as a premise-less derivation.)

The notion of hypothetical judgement is internalised as the connective of implication. The introduction and elimination rules are as follows.

$\cfrac{ \begin{matrix} \cfrac{}{A \ true} u \\ \vdots \\ B \ true \end{matrix} }{A \supset B \ true} \supset_{I^u} \qquad \cfrac{A \supset B \ true \quad A \ true}{B \ true} \supset_E$

In the introduction rule, the antecedent named u is discharged in the conclusion. This is a mechanism for delimiting the scope of the hypothesis: its sole reason for existence is to establish "B true"; it cannot be used for any other purpose, and in particular, it cannot be used below the introduction. As an example, consider the derivation of "A ⊃ (B ⊃ (A ∧ B)) true":

$\cfrac{\cfrac{\cfrac{{}}{A \ true} u \quad \cfrac{{}}{B \ true} w}{A \wedge B \ true}\wedge_I}{ \cfrac{B \supset \left ( A \wedge B \right ) \ true}{ A \supset \left ( B \supset \left ( A \wedge B \right ) \right ) \ true } \supset_{I^u} } \supset_{I^w}$

This full derivation has no unsatisfied premises; however, sub-derivations are hypothetical. For instance, the derivation of "B ⊃ (A ∧ B) true" is hypothetical with antecedent "A true" (named u).

With hypothetical derivations, we can now write the elimination rule for disjunction:

$\cfrac{ A \vee B \hbox{ true} \quad \begin{matrix} \cfrac{}{A \ true} u \\ \vdots \\ C \ true \end{matrix} \quad \begin{matrix} \cfrac{}{B \ true} w \\ \vdots \\ C \ true \end{matrix} }{C \ true} \vee_{E^{u,w}}$

In words, if A ∨ B is true, and we can derive C true both from A true and from B true, then C is indeed true. Note that this rule does not commit to either A true or B true. In the zero-ary case, i.e. for falsehood, we obtain the following elimination rule:

$\frac{\perp true}{C \ true} \perp_E$

This is read as: if falsehood is true, then any proposition C is true.

Negation is similar to implication.

$\cfrac{ \begin{matrix} \cfrac{}{A \ true} u \\ \vdots \\ p \ true \end{matrix} }{\lnot A \ true} \lnot_{I^{u,p}} \qquad \cfrac{\lnot A \ true \quad A \ true}{C \ true} \lnot _E$

The introduction rule discharges both the name of the hypothesis u, and the succedent p, i.e., the proposition p must not occur in the conclusion A. Since these rules are schematic, the interpretation of the introduction rule is: if from "A true" we can derive for every proposition p that "p true", then A must be false, i.e., "not A true". For the elimination, if both A and not A are shown to be true, then there is a contradiction, in which case every proposition C is true. Because the rules for implication and negation are so similar, it should be fairly easy to see that not A and A ⊃ ⊥ are equivalent, i.e., each is derivable from the other.