Natural Deduction - Introduction and Elimination

Introduction and Elimination

Now we discuss the "A true" judgment. Inference rules that introduce a logical connective in the conclusion are known as introduction rules. To introduce conjunctions, i.e., to conclude "A and B true" for propositions A and B, one requires evidence for "A true" and "B true". As an inference rule:


frac{Ahbox{ true} qquad Bhbox{ true}}{A wedge Bhbox{ true}} wedge_I

It must be understood that in such rules the objects are propositions. That is, the above rule is really an abbreviation for:


frac{Ahbox{ prop} qquad Bhbox{ prop} qquad Ahbox{ true} qquad Bhbox{ true}}{A wedge Bhbox{ true}} wedge_I

This can also be written:


frac{A wedge Bhbox{ prop} qquad Ahbox{ true} qquad Bhbox{ true}}{A wedge Bhbox{ true}} wedge_I

In this form, the first premise can be satisfied by the formation rule, giving the first two premises of the previous form. In this article we shall elide the "prop" judgments where they are understood. In the nullary case, one can derive truth from no premises.


frac{ }{tophbox{ true}} top_I

If the truth of a proposition can be established in more than one way, the corresponding connective has multiple introduction rules.


frac{Ahbox{ true}}{A vee Bhbox{ true}} vee_{I1}
qquad
frac{Bhbox{ true}}{A vee Bhbox{ true}} vee_{I2}

Note that in the nullary case, i.e., for falsehood, there are no introduction rules. Thus one can never infer falsehood from simpler judgments.

Dual to introduction rules are elimination rules to describe how to de-construct information about a compound proposition into information about its constituents. Thus, from "A ∧ B true", we can conclude "A true" and "B true":


frac{A wedge Bhbox{ true}}{Ahbox{ true}} wedge_{E1}
qquad
frac{A wedge Bhbox{ true}}{Bhbox{ true}} wedge_{E2}

As an example of the use of inference rules, consider commutativity of conjunction. If A ∧ B is true, then B ∧ A is true; This derivation can be drawn by composing inference rules in such a fashion that premises of a lower inference match the conclusion of the next higher inference.

 cfrac{cfrac{A wedge Bhbox{ true}}{Bhbox{ true}} wedge_{E2} qquad cfrac{A wedge Bhbox{ true}}{Ahbox{ true}} wedge_{E1}} {B wedge Ahbox{ true}} wedge_I

The inference figures we have seen so far are not sufficient to state the rules of implication introduction or disjunction elimination; for these, we need a more general notion of hypothetical derivation.

Read more about this topic:  Natural Deduction

Famous quotes containing the words elimination and/or introduction:

    The kind of Unitarian
    Who having by elimination got
    From many gods to Three, and Three to One,
    Thinks why not taper off to none at all.
    Robert Frost (1874–1963)

    For the introduction of a new kind of music must be shunned as imperiling the whole state; since styles of music are never disturbed without affecting the most important political institutions.
    Plato (c. 427–347 B.C.)