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".