20130111

Natural Deduction

Natural Deduction is a rule-based system for building proofs of sequents.  It is important to remember when doing these proofs that we are not asserting that the premises are true "in the real world".  Rather, we are exploring the dimensions of the logical world that would exist if  the premises were true.  In this sense, we can think of a proof as an extension of the implication operator.  We will explore this relationship further as we look at the Natural Deduction system.

A proof in Natural Deduction consists of a numbered list of propositions.  Each proposition in the list is either a premise (which we assume to be true) or a proposition whose truth can be proved by applying rules to propositions already in the list.

The rules in Natural Deduction all have a similar format.  Each one states that if the proof  contains propositions of a particular structure, then there is a new proposition which we can add to the proof.  The rules are all syntactic in nature - they make no reference to the meaning of the propositions.  However, when we discuss the rules, we sometimes make reference to our understanding of how the real world works in order to motivate the rules.

There are rules for introducing and eliminating all of the logical operators.

Rules for Conjunction (AND)

The "AND Introduction" Rule

The idea of this rule is that if a proof contains a proposition PHI and a proposition PSI, then we can add the proposition PHI AND PSI.

We call this rule "^i", and represent it graphically as

                                                 PHI      PSI
                                                  PHI ^ PSI

The "AND Elimination" Rules

The idea behind this pair of rules is that if a proof contains a proposition PHI1 AND PHI2, then we can add each of PHI1 and PHI2 to the proof.

"^e1"                                       PHI1 ^ PHI2
                                                       PHI1

"^e2"                                       PHI1 ^ PHI2
                                                       PHI2


Rules for Double Negation (NOT NOT)

Since there are only two truth values in our system and negating a proposition changes its truth value, it is clear that PHI and NOT NOT PHI must have the same truth value.  Thus if either of these propositions occurs in our proof, we can add the other one.  In these notes I will use an exclamation mark to replace the proper "NOT" symbol.

"!!i"                                       PHI
                                             !!PHI

"!!e"                                       !!PHI
                                              PHI


Rules for Implication

We will start with rules related to eliminating the "->" operator.  It is important to remember that when we say "eliminate", what we mean is that we are adding a proposition to a proof which has one fewer -> symbols in it than some previous proposition in the proof.  We are not eliminating the previous proposition, and we are free to use it again if we need it.

Recall the meaning of the proposition "PHI -> PSI".  If this proposition is true, then it is not possible for PHI to be true and PSI to be false.  In other words, if PHI is true and PHI -> PSI is true, then PSI must be true.  This motivates our first rule of -> elimination.

"->e"                                 PHI         PHI -> PSI
                                                    PSI

This rule is also called Modus Ponens, which means "The method of assertion" or "The method of affirmation".