I.   Using the method described in lesson 11, write derivations
            for the following problems:

           A.   Derive ~(P & ~P) from scratch

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

           B.   Derive P from

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

      II.   As preludes to the next lesson, write derivations for the
            following problems:

           A.   Derive Q from

               1.   P & ~P                      Premise
               2.   P                           1, Simp.
               3.   ~P & P                      2, Comm.
               4.   ~P                          3, Simp.
               5.   P v Q                       4, Add.
               6.   Q                           4, 5, DS

           B.   Derive ~P <-> (P -> ~P) from scratch

               1.       ~P                      Assumption
               2.           P                   Assumption
               3.           ~P                  1, R
               4.       P -> ~P                 2-3, CP
               5.   ~P -> (P -> ~P)             1-4, CP
               6.       P -> ~P                 Assumption
               7.       ~P v ~P                 6, Impl.
               8.       ~P                      7, Taut.
               9.   (P -> ~P) -> ~P             6-8, CP
              10.   [~P -> (P -> ~P)] & [(P -> ~P) -> ~P]
                                                5, 9, Conj.
              11.   ~P <-> (P -> ~P)            10, Equiv.

        or, using the method described in lesson 11,

               1.       ~[~P <-> (P -> ~P)]     Assumption
               2.       ~([~P & (P -> ~P)] v [~~P & ~(P -> ~P)])
                                                1, Equiv.
               3.       ~[~P & (P -> ~P)] & ~[~~P & ~(P -> ~P)]
                                                2, DM
               4.       ~[~P & (P -> ~P)]       3, Simp.
               5.       ~~P v ~(P -> ~P)        4, DM
               6.       ~~P v ~(~P v ~P)        5, Impl.
               7.       ~~P v ~~P               6, Taut.
               8.       ~~P                     7, Taut.
               9.       ~[~~P & ~(P -> ~P)] & ~[~P & (P -> ~P)]
                                                3, Comm.
              10.       ~[~~P & ~(P -> ~P)]     9, Simp.
              11.       ~~~P v ~~(P -> ~P)      10, DM
              12.       ~P v ~~(P -> ~P)        11, DN
              13.       ~P v (P -> ~P)          12, DN
              14.       ~P v (~P v ~P)          13, Impl.
              15.       ~P v ~P                 14, Taut.
              16.       ~P                      15, Taut.
              17.       ~P v [~P <-> (P -> ~P)] 16, Add.
              18.       ~P <-> (P -> ~P)        8, 17, DS
              19.   ~[~P <-> (P -> ~P)] -> [~P <-> (P -> ~P)]
                                                1-18, CP
              20.   ~~[~P <-> (P -> ~P)] v [~P <-> (P -> ~P)]
                                                19, Impl.
              21.   [~P <-> (P -> ~P)] v [~P <-> (P -> ~P)]
                                                20, DN
              22.   ~P <-> (P -> ~P)            21, Taut.