Gödel–Kolmogorov Double-Negation Translation

Step 1: Fix the intuitionistic rules we may use. Intuitionistic logic keeps modus ponens and the natural deduction rules for $\wedge, \vee, \to$, and defines $\neg P := (P \to \bot)$ where $\bot$ is absurdity ("from a proof of $\bot$, anything follows" — ex falso quodlibet — is intuitionistically valid). What is not assumed is $P \vee \neg P$ or the double-negation elimination law $\neg\neg P \to P$.

**Step 2: Prove the easy direction $P \to \neg\neg P$ intuitionistically.** Assume a proof of $P$. We must produce a proof of $\neg\neg P = (( P \to \bot) \to \bot)$, i.e. assume a proof of $(P \to \bot)$ and derive $\bot$. Applying this assumed function to our proof of $P$ directly yields a proof of $\bot$. So $P \to \neg\neg P$ holds with no case analysis — this direction never needed LEM.

**Step 3: Build a proof of $\neg\neg(P \vee \neg P)$ directly.** We must show $((P \vee \neg P) \to \bot) \to \bot$. Assume a proof $h$ of $(P \vee \neg P) \to \bot$ (i.e. $h$ refutes the disjunction); we must derive $\bot$. Observe that $h$, restricted to the right disjunct, gives a function taking any proof of $P$ to a proof of $\bot$ — that is exactly a proof of $\neg P$ (apply $h$ after wrapping with the right-injection $\text{inr}$). Call this derived proof $n : \neg P$.

Step 4: Close the loop. Since we have $n : \neg P$, we can form $\text{inr}(n) : P \vee \neg P$ (the right disjunct of $P \vee \neg P$, instantiated with proof $n$). Feed this term back into $h$: $h(\text{inr}(n))$ is a proof of $\bot$, exactly the $\bot$ we needed to derive in Step 3. This closes the assumption from Step 3, giving a full intuitionistic proof of $\neg((P\vee\neg P)\to\bot)$, i.e. of $\neg\neg(P \vee \neg P)$.

*Step 5: Why this does not* give $P \vee \neg P$ back.** Step 4 produces $\neg\neg(P \vee \neg P)$, but intuitionistically $\neg\neg Q \to Q$ is not generally derivable (that would require the very LEM-like principle we lack). So the translation is genuinely weaker: it shows classical logic's "law" survives as an irrefutable statement (its negation is always contradictory) even where it cannot be asserted outright — precisely the gap that lets constructive mathematics coexist with, and interpret, classical mathematics via Gödel's negative translation of every formula $\phi \mapsto \phi^N$ (replacing each atomic formula and each connective with its double-negated intuitionistic analogue), which sends every classically-provable arithmetic sentence to an intuitionistically-provable one.