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.