In classical logic ~~p -> p? Intuitionistic? Is the following rule applicable in classical propositional logic?
$\sim (\sim p)\rightarrow p$
In my textbook, it shows that $p \rightarrow\sim(\sim p)$
holds for intuitionistic logic but I was wondering if the converse of that implication was also true? Or would it be:
$\sim p \rightarrow\  \sim(\sim(\sim p))$ ?
 A: The answer is partly negative and partly affirmative. Here
is a proof of p -> ~~p in LJ repectively LM, the later since
we dont need ex falso:
------ (Id)   ------ (Id)
p |- p        f |- f 
-------------------- (L->)
    p, ~p |- f
    ---------- (R->)
    p |- ~~p
   ---------- (R->)
   |- p-> ~~p

Now contraposition (as a meta rule) is also valid
(admissible) in LJ respectively LM, again the later
since we don't need ex falso:
   ...
----------   ------ (Id)
G | A -> B   A |- A
------------------- (Cut)  ------ (Id)
  G, A |- B                f |- f
  ------------------------------- (L->)
         G, ~B, A |- f
        -------------- (R->)
          G, ~B |- ~A
         ------------- (R->)
         G |- ~B -> ~A

So we can apply contraposition on p -> ~~p, and
we get ~~~p -> ~p as a generally valid theorem in LJ.
But ~~p -> p is not provable in LJ, this is DNE,
i.e double negation elimination, and if it were
generally valid, we would have LJ=LK. 
A LJ counter model can be found that shows that DNE isn't
generally valid in LJ. I guess a LM counter model can
also be found, an edit of this post will follow.
Interestingly although ~~p -> p is not provable,
nevertheless the contraposition ~p -> ~~~p is
provable, in LJ and in LM as well, the later again
since ex falso is not needed: 
-------- (Id)  ------ (Id)
~p |- ~p       f |- f
--------------------- (L->)
   ~p, ~~p |- f
   ------------ (R->)
    ~p |- ~~~p
  -------------- (R->)
  |- ~p -> ~~~p

The proof for ~p --> ~~~p is the same as the
proof for p --> ~~p, just replace p by ~p.
Bye
Legend:
LK: Gentzen Sequent Calculus for Classical Logic
LJ: Gentzen Sequent Calculus for Intuitionistic Logic
LM: Gentzen Sequent Calculus for Minimal Logic
