Is double negation introduction an axiom of intuitionistic logic or can it be derived?

Question

If I have a rule for negation introduction...

Rule (NegationIntroduction,ProofByNegation)
  Premises
    P=>Q, P=>⌐Q
  Conclusion
    ⌐P

...then it seems to me that I can derive the rule for double negation introduction:

Rule (DoubleNegationIntroduction)
  Premises
    P
  Conclusion
    ⌐⌐P
  Proof
    Suppose
      ⌐P
    Hence
      P
    ⌐P=>P

    Suppose
      ⌐P
    Hence
      ⌐P
    ⌐P=>⌐P

    ⌐⌐P by NegationIntroduction

There are two places where I can see that the reasoning might be faulty. Firstly, the assumption $⌐P$ when $P$ is given as a premise. However, can you not assume anything for the purposes of an argument even if the contrary is known to be true? Secondly, the resulting implication $⌐P=>P$. However, I know that intuitionistically as well as classically we have $A=>(C=>A)$. I have read Propositional Logic - Can you Derive $C \to A$ from $A$ alone, given the introduction rule? for example, so I'm pretty sure that this is okay.

Answer 1

Yes, $A\to \neg \neg A$ is intuitionistically valid, and your proof looks correct.

Many presentations of intuitionistic logic consider $\neg A$ to be an abbreviation for $A\to \bot$, and in that case $A\to\neg\neg A$ is $$ A\to((A\to\bot)\to \bot)$$ which is just an instance of the generally valid $$ A\to((A\to B)\to B) $$