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 Di) 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.

Read more about this topic:  Natural Deduction