Can we construct a proof of P from ~~P?  If you consult the rules of inference, you'll not find a rule of inference which allows you to make that inference. It's clear that the rules of inference need to be supplemented.  We call the supplementary rules "Equivalence Rules" and there's an important reason for not lumping them together with the rules of inference.  The equivalence rules we'll list below happen to be pairs of logically equivalent wffs. They work as follows: Wherever you find one of the pair, you are allowed to infer the wff which substitutes the second member of the pair for the first.  

Let's see how this works by listing a few of the equivalence rules, starting with the rule for double negation:

Here's how our Equivalence Rules work in a derivation:

We applied Double Negation to line 1 in order to transform (~A v ~~B) into the equivalent wff (~A v B).  That made it possible then to use the rule of inference hs.  It's very important to notice that we applied DN on a part of line 1, not on the entire wff.  The Equivalence Rules allow this. They allow us to replace equivalent wffs or parts of wffs.

The next rule we'll introduce is Contraposition:

 CONTRA is an equivalence between a conditional and the conditional we get by switching and negating the antecedent and consequent.  Here's how it can work in a derivation. Note that we also use DN in this derivation.

After eliminating the double negation of the consequent from line 1, in line 6 we applied Contraposition. Then we used modus ponens to infer ~A.  Question: Can you come up with a derivation of ~A from the same premises which doesn't use contraposition?  We could have used modus tollens instead.  Our rule base is becoming more powerful as we add new rules, and you'll find that there are often many ways to achieve the same result.  Note also that we applied Contraposition on the entire wff in line 1. Here's a short derivation where we apply the rule to just a part of the line:

Here we have a disjunction whose left disjunct is a conditional. We are free to apply CONTRA to just the conditional, as long as we reproduce the rest of the line as it was before the transformation.  This is an important "freedom". Again, you may apply equivalence rules to parts of wffs, as long as you reproduce the entire wff of which the equivalent part is a part on a new line.

Here are a few more rules. After listing them, we'll look at a derivation which incorportates all of them.

Now a derivation which illustrates the use of these rules:

Again, the Equivalence Rules just express some of the equivalences between wffs. As long as it's listed as a rule, you may use it in a proof. There are, of course, many equivalences which are not stated in our equivlance rules, and you may not use such equivalences in your proofs.  Why not? Such a "proof" would not be a proof in PL, since it uses rules which are not part of the proof theory of PL. Your "proof" might constitute a proof in another formal system, but it is not a proof in PL.

There are four more equivalence rules. We list them below, and comment briefly.  

Biconditional exchange is an important rule, because without it, we can't do anything with biconditionals! Consider the following derivation:

It seems obvious that something like mp should apply to lines 1 and 2. But mp works only on conditionals. So we need to transform the biconditional in line 1 into a conjunction of conditionals, and then break up the conjunction to get the needed conditional for mp.

We've introduced 10 new rules, the Equivalence Rules.  They are summarized on a separate page, as Summary of Equivalence Rules.  Together with the Rules of Inference, you now have all the rules needed to do any proof. The exercises listed below will give you lots of practice in applying the rules.  In the next section, we'll introduce two strategies which will make proofs a bit easier.