= Solution
The premise turns an assumed $\neg P$ into a <contradiction>. Use the <negation introduction rule> to obtain $\neg\neg P$, then the supplied classical <double-negation elimination> rule:
|| Line
|| Context
|| Formula
|| Justification
| 1
| $\{1\}$
| $\neg P\to\bot$
| Premise
| 2
| $\{1,2\}$
| $\neg P$
| Temporary assumption
| 3
| $\{1,2\}$
| $\bot$
| <implication elimination rule> $\to\text{-elim}$ on 1, 2
| 4
| $\{1\}$
| $\neg\neg P$
| <negation introduction rule> $\neg\text{-intro}$ on 3; discharge 2
| 5
| $\{1\}$
| $P$
| <double-negation elimination> $\neg\neg\text{-elim}$ on 4
Hence $\boxed{(\neg P\to\bot)\vdash P}$. The final classical rule is essential: deriving $\neg\neg P$ alone is not yet a proof of $P$ in <Intuitionistic propositional logic>.
Back to article page
