The rules I have given you so far work in only one direction. For
instance, you can derive Q from (P -> Q) and P, but you cannot derive Q and
(P -> Q) from P. Since I have given you only the rules that work in one
direction, there are still many things that you cannot prove with what you
have learned here so far. Take, for instance, the following problem:

        Derive P from

               1.   Q -> P          Premise
               2.   ~~Q             Premise

        P logically follows from the premises given, but the rules of
inference alone do not let you derive P from these premises. In addition to
the rules of inference, we need a rule which says that Q is true if ~~Q is
true. There is such a rule, but it is not a rule of inference. Rather, it
is a rule of replacement. The rule is called double negation, and it looks
like this:

        P <-> ~~P

        This means that P implies ~~P, and that ~~P implies P. Unlike the
rules of inference, it works both ways. It is called a rule of replacement,
because it identifies two expressions that can replace one another
anywhere. Whenever you have the negation of the negation of a statement,
for instance, you can replace it with the statement itself. And whenever
you have a statement, you can replace it with the negation of its negation.

        The rules of replacement differ from the rules of inference in one
other respect. You can use a rule of replacement on any part of a
statement. You do not have to use it with an entire line, as you had to
with the rules of inference. For instance, you can derive (P & Q) from (~~P
& Q) simply by double negation.

        Here are the rules of replacement:

        De Morgan's Theorems (DM):          ~(P & Q) <-> (~P v ~Q)
                                            ~(P v Q) <-> (~P & ~Q)

        Commutation (Com.):                 (P v Q) <-> (Q v P)
                                            (P & Q) <-> (Q & P)

        Association (Assoc.):               [P v (Q v R)] <-> [(P v Q) v R]
                                            [P & (Q & R)] <-> [P & (Q & R)]

        Distribution (Dist):        [P & (Q v R)] <-> [(P & Q) v (P & R)]
                                    [P v (Q & R)] <-> [(P v Q) & (P v R)]

        Double Negation (DN):               P <-> ~~P

        Transposition (Trans.):             (P -> Q) <-> (~Q -> ~P)

        Material Implication (Impl.):       (P -> Q) <-> (~P v Q)

        Material Equivalence (Equiv.):  (P <-> Q) <-> [(P -> Q) & (Q -> P)]
                                        (P <-> Q) <-> [(P & Q) v (~P & ~Q)]

        Exportation (Exp.):             [(P & Q) -> R] <-> [P -> (Q -> R)]

        Tautology (Taut.):                  P <-> (P v P)
                                            P <-> (P & P)