Proof of double negation elimination using natural deduction

Solution 1:

The rules you list comprise a natural deduction system for intuitionistic logic. The sequent $\lnot A\to \bot\vdash A$ is not valid in intuitionistic logic, so it is not provable in your system.

To prove $\lnot A\to \bot\vdash A$, you need to be working with a natural deduction system for classical logic, which means adding an additional rule to your system. One common choice is to add double negation elimination itself; this makes your proof a valid one. Other common choices are adding reductio ad absurdum (proof by contradiction) or the law of excluded middle.