next up previous
Next: Friday, February 4 Up: Lecture Notes Previous: Tuesday, February 1

Wednesday, February 2

Will include a fully worked example of what is being asked for in Homework 4.

Homework 2 will be returned.

THERE ARE SOME TYPOS IN HOMEWORK 4, ASSIGNMENT 1 they are corrected in the posted version; I miswrote the right sides of distributive laws several times...

Notes for February 2

Official Rules of Natural Deduction

Today we will present our ``official'' basic rules of natural deduction.


P                P & ~P

~P               -----------  negation elimination
-------          Q


Either version is acceptable.  From a contradiction, we can deduce

G, P |- Q & ~Q

--------------  negation introduction

G |- ~P

To prove ~P, show that a contradiction can be deduced if P is adopted
as a temporary premise.  We will use the notation G,P to abbreviate G u {P}
on the left sides of derivations.


P & Q                              P & Q

------  conjunction elimination 1  ------  conjunction elimination 2
P                                  Q




P & Q

There's nothing much to say about these!



P -> Q

-------  implication elimination 1 (modus ponens)


G, P |- Q

----------  implication introduction

G |- P -> Q

We have talked about these.  Implication introduction 2 (modus tollens)
has not been forgotten, but it is not needed as a basic rule (it can be
derived from the others, and we'll see how to do this).


P | Q                                        P | Q

~P                                           ~Q

---------  disjunction elimination 1         --------  disjunction elimination 2

Q                                            P

I think that Grantham calls these rules of disjunctive syllogism.

G, ~Q |- P                                   G |- ~P |- Q

---------- disjunction introduction 1        ------------- disjunction introduction 2

G |- P | Q                                   G |- P | Q

These are not the same as Grantham's rules of disjunction introduction, but
Grantham's rules are special cases, and I allow use of the same names for
his rules:

Q                                            P

-----  disjunction introduction 2            ----- disjunction introduction 1
       (special case)                              (special case)
P | Q                                        P | Q

If you look at Grantham's rules and compare them with mine, you'll
see why the numbering is the way it is.

The rest of this lecture will be taken up showing that we do not need
other rules listed by Grantham as primitive rules.

Here's why we choose our disjunction introduction rules as we do:

| 1. ~P premise of subproof
| 2. ~P line 1
3. P | ~P  disjunction introduction 2, lines 1-2.

So we have emptyset |- P | ~P, the law of excluded middle.  Look at the 
proof of excluded middle in Grantham's book!

We can derive both double negation rules from the rules given above.

1. P premise
2. | ~P premise of subproof
3. | P & ~P conjunction introduction, lines 1,2
4. ~ ~ P negation introduction, lines 3-4.

1. ~ ~ P premise
2. P | ~P excluded middle (proved above)
3. P disjunction elimination 2, lines 2,1

so we have the rules

P                                       ~ ~ P

--------  double negation introduction  ------- double negation elimination

~ ~ P                                   P

The ability to derive these rules is another advantage of our
strong disjunction introduction rules.

Here's where we stopped on Wednesday.

Randall Holmes