next up previous
Next: Monday, February 7 and Up: Lecture Notes Previous: Wednesday, February 2

Friday, February 4

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

We continue the development of rules we didn't include in our basic list.

1. P -> Q premise
2. ~Q     premise
| 3. P premise of subproof
| 4. Q modus ponens, lines 3,1
| 5. Q & ~Q conjunction introduction, lines 2,4
6. ~P negation introduction, lines 3-5.

So (as promised above) we have the rule

P -> Q

~Q

--------  implication elimination 2 (modus tollens)

~P

Now I develop Grantham's disjunction elimination rule:

1. P|Q  premise
2. P->R premise
3. Q->R premise
4. | ~R premise of subproof
5. | ~P modus tollens, lines 2,4
6. | Q  disjunction elimination 2, lines 1,5
7. | ~Q modus tollens, lines 3,4
8. | Q & ~Q conjunction introduction, lines 6,7
9. ~ ~R negation introduction, lines 4-8
10. R double negation elimination, line 9

which justifies the rule

P | Q

P -> R

Q -> R

-------  proof by cases

R

Note that I do not call this rule ``disjunction elimination''.

In combination with implication introduction, this justifies the rule

G |- P|Q

G,P |- R

G,Q |- R

---------  proof by cases with subproofs

G |- R

which really captures the structure of a proof by cases.

Development of New Rules from Proofs (reuse and modularity)

Notice that every proof can be reinterpreted as a new rule!

Rules for Biconditional and Xor

Biconditional                   Xor

P <-> Q           P <-> Q       P <+> Q  P <+> Q

P                 Q             ~P       ~Q

--------          ---------     -------  ---------

Q                 P             Q        P



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

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

---------                       ------------------------

G |- P <-> Q                    G |- P <+> Q

The rules have the names one expects; I won't care about numbering of
these rules as we won't use them often.  Rules for NAND and NOR are
left to your imagination.


A Rule We Do Not Have

We do not have the ability to use biconditional theorems
(equivalences) to ``substitute equals for equals'' as we did in our
Boolean algebra formalization of propositional logic.  (Such a rule is
valid but it takes work to show this).

Proof Strategy

We number the lines in our proofs from the beginning forward to the
end and we may try to prove theorems by writing down the premises and
applying the rules in a forward direction with some success.  But the
best strategy for natural deduction is to work backwards from the goal
to the theorem.  The idea is to look at the topmost connective of the
theorem we are trying to prove and think about what the previous step
of the proof (which presumably uses the introduction rule for that
connective) would look like.  Of course, another possible way to prove
a theorem is to assume its negation and try to prove a contradiction from
it.

Notice that our basic rules allow us three ways to prove a statement with
a given propositional connective at the top:  we can prove it using the
introduction rule for that connective, we can find it as a component of
a premise, or we can deduce it from a contradiction (anything can be
deduced from a contradiction!).  The last case is rather special, since
we don't actually _believe_ any contradictions :-)

An Example of Proof Development

(Grantham proves the same formula in the book; our different
treatment of disjunction makes our proof somewhat shorter).

Goal:  ~(A & B) -> (~A | ~B)

The last step of the proof should be an implication introduction,
appealing to a subproof in which ~(A&B) is the first line and ~A | ~B
is the last.

So we have the following proof sketch:

| 1. ~(A&B) premise of subproof

.
.
.

| n. (~A | ~B) ???
n+1. ~(A & B) -> (~A | ~B) implication introduction, lines 1-n.

Now we try the same goal-directed approach on the disjunction
~A | ~B:  it should be proved by disjunction introduction in a subproof
with hypothesis ~~A and conclusion ~B (or hypothesis ~~B and conclusion
~A, but this is symmetrical).

| 1. ~(A & B) premise of subproof
|| 2. ~~A premise of subsubproof

.
.
.

|| n-1. ~B ???
| n. (~A | ~B) disjunction introduction 2, lines 2-(n-1)
n+1. ~(A & B) -> (~A | ~B) implication introduction, lines 1-n.

Continuing, we think that the natural way to prove ~B is by negation
introduction, using a proof with premise B and conclusion a
contradiction.

| 1. ~(A & B) premise of subproof
|| 2. ~~A premise of subsubproof
||| 3. B premise of subsubsubproof (!)
.
.
.

||| n-2. Q & ~Q (we don't know what Q will be). ???
|| n-1. ~B negation introduction, lines 3-(n-2)
| n. (~A | ~B) disjunction introduction 2, lines 2-(n-1)
n+1. ~(A & B) -> (~A | ~B) implication introduction, lines 1-n.

The proof is now best completed by ``forward'' reasoning.

| 1. ~(A & B) premise of subproof
|| 2. ~~A premise of subsubproof
||| 3. B  premise of subsubsubproof (!)
||| 4. A  double negation elimination, line 2
||| 5. A&B  conjunction introduction, lines 4,3
||| 6. (A&B) & ~(A&B) conjunction introduction, lines 1,5
|| 7. ~B negation introduction lines 3-6.
| 8. (~A | ~B) disjunction introduction 2, lines 2-7
9. ~(A & B) -> (~A | ~B) implication introduction, lines 1-8.

If we chose Q = A&B, the whole proof could be developed in the goal
directed style, and it does seem that of the available formulas this
might have been the best choice.

Readers may like to see a completely ``boxed'' version:
----------------------------------------------------------------
| 1. ~(A & B) premise of subproof                              |
|------------------------------------------------------------- | 
|| 2. ~~A premise of subsubproof                             | |
||---------------------------------------------------------- | |
||| 3. B  premise of subsubsubproof (!)                    | | |
||| 4. A  double negation elimination, line 2              | | |
||| 5. A&B  conjunction introduction, lines 4,3            | | |
||| 6. (A&B) & ~(A&B) conjunction introduction, lines 1,5  | | |
||---------------------------------------------------------- | |
|| 7. ~B negation introduction, lines 3-6                    | |
|------------------------------------------------------------- |
| 8. (~A | ~B) disjunction introduction 2, lines 2-7           |
----------------------------------------------------------------
9. ~(A & B) -> (~A | ~B) implication introduction, lines 1-8.



Randall Holmes
2000-05-05