In doing Russell & Norvig, Ch. 6, p. 181: #6.5, you might find the
following additional rules of inference for the natural-deduction system
that I am introducing in lecture to be useful (though note that you do not
need anything that is not in Ch. 6):

vIntro:  From P                From Q
         -----------           -----------
         Infer (PvQ)           Infer (PvQ)


vElim:   From (PvQ)            From (PvQ)
         and  -P               and  -Q
         ----------            ----------
         Infer Q               Infer P


<=>Intro:  From (P => Q)       From (P => Q)
           and  (Q => P)       and  (Q => P)
           ---------------     ---------------
           Infer (P <=> Q)     Infer (Q <=> P)


<=>Elim:  From (P <=> Q)      From (P <=> Q)
           --------------      --------------
           Infer (P => Q)      Infer (Q => P)


Also:  You can't use natural deduction (or any other syntactic proof-technique)
to prove that you *can't* prove something.  But you can prove that you
can't prove something, by using semantic proof-techniques, such as truth
tables or Wang's Algorithm.


For more details on the natural-deduction system introduced in lecture, see:

Schagrin, Morton L.; Rapaport, William J.; & Dipert, Randall R. (1985),
_Logic: A Computer Approach_ (New York: McGraw-Hill) (SEL: BC138 .S32 1985)