If you'll examine the tautology in I.C. of the last lesson's
homework, you may note something very interesting. If you can show that P
is implied by ~P, you can show P in a few more lines. More generally, you
can derive any formula by showing that it follows from its negation.
Consider, for instance, the following proof for the law of excluded middle
(P v ~P):

               1.       ~(P v ~P)               Assumption
               2.       ~P & ~~P                1, DM
               3.       ~P                      2, Simp.
               4.       ~P v P                  3, Add.
               5.       P v ~P                  4, Comm.
               6.   ~(P v ~P) -> (P v ~P)       1-5, CP
               7.   ~~(P v ~P) v (P v ~P)       6, Impl.
               8.   (P v ~P) v (P v ~P)         7, DN
               9.   P v ~P                      8, Taut.

        We begin by assuming the negation of what we want to prove. We show
that it implies what we want to prove. Then we use a few rules of
replacement to collapse that conditional into what we want. The same method
also works in proofs that have premises. Consider this proof:

        Derive P from

               1.   P v Q                       Premise
               2.   P v ~Q                      Premise
               3.       ~P                      Assumption
               4.       ~Q                      2, 3, DS
               5.       Q v P                   1, Comm.
               6.       P                       4, 5, DS
               7.   ~P -> P                     3-6, CP
               8.   ~~P v P                     7, Impl.
               9.   P v P                       8, DN
              10.   P                           9, Taut.



converted with guide2html by Kochtopf