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

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.

• The derivation of the rule about halfway down the page here en.wikibooks.org/wiki/Formal_Logic/Sentential_Logic/… suggests this derivation is fine. In particular, they use the same 'trick' as me, namely repeating the outer premise to derive the implication $⌐P=>P$. The contrasting implication $⌐P=>⌐P$ is not derived, however I assume the rule for negation introduction that they employ is simpler. This is not intuitionistic logic, but I think that at least in this case the principles are the same. Jun 15, 2016 at 13:41

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)$$