[proofplan]
We prove the equivalence by giving rule transformations in both directions. First, assuming double negation elimination, any derivation of $\bot$ from a temporary assumption $\neg A$ can be converted by implication introduction into a derivation of $\neg\neg A$, and then double negation elimination yields $A$. Conversely, assuming proof by contradiction, a derivation of $\neg\neg A$ can be combined with a temporary assumption $\neg A$ by implication elimination to obtain $\bot$, after which proof by contradiction discharges the temporary assumption and yields $A$.
[/proofplan]
[step:Derive proof by contradiction from double negation elimination]
Assume that the rule of double negation elimination is available in addition to the intuitionistic rules. Let $A$ be a formula, and suppose there is a derivation $\Pi$ of $\bot$ from a temporary assumption $\neg A$.
Since $\neg A$ abbreviates $A \to \bot$, the displayed temporary assumption has the form $A \to \bot$. By implication introduction applied to the derivation $\Pi$, discharging the assumption $\neg A$, we obtain a derivation of
\begin{align*}
\neg A \to \bot.
\end{align*}
By the definition of negation, this formula is $\neg\neg A$. Applying double negation elimination to $\neg\neg A$ gives $A$.
Thus every derivation of $\bot$ from a temporary assumption $\neg A$ can be transformed into a derivation of $A$ discharging that assumption. This is exactly the rule of proof by contradiction.
[guided]
We assume double negation elimination and show that proof by contradiction becomes admissible. Fix a formula $A$. The proof-by-contradiction rule starts with a temporary assumption $\neg A$ and a derivation of contradiction from it:
\begin{align*}
[\neg A] \quad \vdots \quad \bot.
\end{align*}
Because negation is defined by $\neg A := A \to \bot$, this temporary assumption is a formula of the natural deduction system, and implication introduction applies to it. Implication introduction says that if, under a temporary assumption $B$, we derive $C$, then we may discharge the assumption $B$ and conclude $B \to C$. Applying this with $B := \neg A$ and $C := \bot$, we obtain
\begin{align*}
\neg A \to \bot.
\end{align*}
By the definition of negation again, $\neg A \to \bot$ is precisely $\neg\neg A$. Now we use the assumed classical rule, double negation elimination:
\begin{align*}
\frac{\neg\neg A}{A}.
\end{align*}
Applying this rule to the derived formula $\neg\neg A$ yields $A$.
Therefore the whole derivation has the form required by proof by contradiction: from a derivation of $\bot$ under the temporary assumption $\neg A$, we conclude $A$ while discharging that assumption.
[/guided]
[/step]
[step:Derive double negation elimination from proof by contradiction]
Assume that the rule of proof by contradiction is available in addition to the intuitionistic rules. Let $A$ be a formula, and suppose $\neg\neg A$ has been derived.
To derive $A$, introduce a temporary assumption $\neg A$. Since $\neg\neg A$ abbreviates $\neg A \to \bot$, implication elimination applied to $\neg\neg A$ and the temporary assumption $\neg A$ gives
\begin{align*}
\bot.
\end{align*}
Now apply proof by contradiction to the derivation of $\bot$ from the temporary assumption $\neg A$. This discharges the assumption $\neg A$ and concludes $A$.
Thus every derivation of $\neg\neg A$ can be transformed into a derivation of $A$, which is exactly double negation elimination.
[guided]
We now assume proof by contradiction and show that double negation elimination becomes admissible. Fix a formula $A$, and suppose we have already derived $\neg\neg A$.
To use proof by contradiction, we must temporarily assume the negation of the desired conclusion. Since the desired conclusion is $A$, introduce the temporary assumption
\begin{align*}
\neg A.
\end{align*}
The available premise is $\neg\neg A$. By the definition of negation, this is the formula
\begin{align*}
\neg A \to \bot.
\end{align*}
Now implication elimination applies: from $\neg A \to \bot$ and $\neg A$, we infer $\bot$. Therefore, under the temporary assumption $\neg A$, we have derived contradiction.
Proof by contradiction is exactly the rule that allows us to discharge this temporary assumption $\neg A$ and conclude $A$. Hence from an arbitrary derivation of $\neg\neg A$, we have constructed a derivation of $A$.
This is precisely the double negation elimination rule:
\begin{align*}
\frac{\neg\neg A}{A}.
\end{align*}
[/guided]
[/step]
[step:Conclude that the two rule extensions prove the same rule instances]
The first derivation shows that intuitionistic natural deduction extended by double negation elimination derives every instance of proof by contradiction. The second derivation shows that intuitionistic natural deduction extended by proof by contradiction derives every instance of double negation elimination. Both transformations used only implication introduction, implication elimination, the definition $\neg A := A \to \bot$, and the chosen additional rule.
Therefore double negation elimination and proof by contradiction are interderivable over intuitionistic natural deduction.
[/step]
