[proofplan] We prove the theorem by induction on a fixed classical Hilbert derivation of $A$. Since $\mathrm{CPC}$ is taken to be $\mathrm{IPC}$ plus excluded-middle axioms and modus ponens, it is enough to show three intuitionistic facts: every intuitionistically provable formula implies its double negation, every excluded-middle instance is intuitionistically double-negation provable, and the induction invariant is preserved by modus ponens. The last point is the double-negation modus ponens argument: from $\neg\neg(B \to C)$ and $\neg\neg B$ we construct $\neg\neg C$ entirely inside $\mathrm{IPC}$. [/proofplan] [step:Fix the proof system and the induction invariant] Let $\mathcal{L}$ denote the set of propositional formulas built from propositional variables, $\bot$, $\wedge$, $\vee$, and $\to$. For every $E \in \mathcal{L}$, write $\neg E$ for $E \to \bot$. We use the Hilbert presentation of $\mathrm{CPC}$ whose axioms are all $\mathrm{IPC}$ axioms together with all formulas of the form $B \vee \neg B$, where $B \in \mathcal{L}$, and whose only inference rule is modus ponens: from $B$ and $B \to C$, infer $C$. For $\mathrm{IPC}$, we use the standard equivalence between its Hilbert presentation and its natural-deduction presentation: a formula is derivable in one presentation exactly when it is derivable in the other. Thus the natural-deduction derivations below establish the corresponding $\mathrm{IPC}$ theorems. Let $D_1,\dots,D_m$ be a fixed $\mathrm{CPC}$ derivation of $A$, so $D_m = A$. We prove by induction on $j \in \{1,\dots,m\}$ that $\mathrm{IPC} \vdash \neg\neg D_j$. [/step] [step:Double-negate every intuitionistic theorem] We first record that for every formula $B \in \mathcal{L}$, $\mathrm{IPC} \vdash B \to \neg\neg B$. By the presentation equivalence just fixed, it suffices to give an intuitionistic natural-deduction derivation. Assume $b:B$. To prove $\neg\neg B$, assume $h:\neg B$, meaning $h:B \to \bot$. Applying $h$ to $b$ gives $\bot$. Discharging $h$ gives $\neg\neg B$, and then discharging $b$ gives $B \to \neg\neg B$. Consequently, if $B$ is an $\mathrm{IPC}$ axiom, then $\mathrm{IPC} \vdash B$ and modus ponens inside $\mathrm{IPC}$ gives $\mathrm{IPC} \vdash \neg\neg B$. [guided] The induction will encounter some lines that are already intuitionistically valid. For such a line $B$, we do not need any classical reasoning; we only need to convert an intuitionistic proof of $B$ into an intuitionistic proof of $\neg\neg B$. We prove the conversion formula $\mathrm{IPC} \vdash B \to \neg\neg B$. Fix a formula $B \in \mathcal{L}$. In intuitionistic natural deduction, assume $b:B$. The target $\neg\neg B$ abbreviates $(B \to \bot) \to \bot$, so assume $h:B \to \bot$. Since $h$ is a proof of $B \to \bot$ and $b$ is a proof of $B$, modus ponens gives $h(b):\bot$. Therefore the temporary assumption $h:B \to \bot$ leads to $\bot$, so we discharge it and obtain $\neg\neg B$. Discharging the original assumption $b:B$ gives $\mathrm{IPC} \vdash B \to \neg\neg B$. Now suppose $B$ is an $\mathrm{IPC}$ axiom. Then $\mathrm{IPC} \vdash B$ by definition of axiomhood. Combining this proof with the already established intuitionistic theorem $B \to \neg\neg B$ by modus ponens inside $\mathrm{IPC}$ yields $\mathrm{IPC} \vdash \neg\neg B$. This handles every line of the classical derivation that is already an intuitionistic axiom. [/guided] [/step] [step:Prove the double negation of each excluded-middle axiom] Let $B \in \mathcal{L}$. We show $\mathrm{IPC} \vdash \neg\neg(B \vee \neg B)$. By the same presentation equivalence, it suffices to give an intuitionistic natural-deduction derivation. Assume $h:\neg(B \vee \neg B)$. To derive $\neg B$, assume $b:B$. By disjunction introduction, $b$ gives $B \vee \neg B$, and then $h$ gives $\bot$. Hence $\neg B$ follows. By disjunction introduction again, this proof of $\neg B$ gives $B \vee \neg B$, and applying $h$ gives $\bot$. Therefore the assumption $h$ is refuted, so $\neg\neg(B \vee \neg B)$ is derivable in $\mathrm{IPC}$. [/step] [step:Show that double negation is preserved by modus ponens] Let $B,C \in \mathcal{L}$. We prove the intuitionistic derivability $\mathrm{IPC} \vdash \neg\neg(B \to C) \to \bigl(\neg\neg B \to \neg\neg C\bigr)$. By the same presentation equivalence, it suffices to give an intuitionistic natural-deduction derivation. Assume $p:\neg\neg(B \to C)$ and $q:\neg\neg B$. To prove $\neg\neg C$, assume $k:\neg C$. Define a derivation of $\neg(B \to C)$ as follows. Assume $f:B \to C$. To obtain $\bot$, it suffices to refute $B$: if $b:B$, then $f(b):C$, and $k(f(b)):\bot$. Thus $f$ gives a proof of $\neg B$. Applying $q:\neg\neg B$ to this proof of $\neg B$ gives $\bot$. Hence $f$ leads to $\bot$, so we have $\neg(B \to C)$. Applying $p:\neg\neg(B \to C)$ to this refutation gives $\bot$. Therefore $k:\neg C$ leads to $\bot$, and so $\neg\neg C$ follows. [guided] This is the only non-mechanical point in the induction. In an ordinary proof by modus ponens, $B \to C$ and $B$ directly give $C$. Here the induction gives only $\neg\neg(B \to C)$ and $\neg\neg B$, so we must show that these double-negated premises still suffice to prove $\neg\neg C$ intuitionistically. Fix formulas $B,C \in \mathcal{L}$. We prove $\mathrm{IPC} \vdash \neg\neg(B \to C) \to \bigl(\neg\neg B \to \neg\neg C\bigr)$. Assume $p:\neg\neg(B \to C)$ and $q:\neg\neg B$. Since $\neg\neg C$ means $(C \to \bot) \to \bot$, assume $k:C \to \bot$ and aim to derive $\bot$. The hypothesis $p$ will yield $\bot$ if we can produce a refutation of $B \to C$. So assume temporarily that $f:B \to C$. We now build a contradiction from $f$ by using $q:\neg\neg B$. To use $q$, we must produce $\neg B$, that is, a map $B \to \bot$. Assume $b:B$. Then $f(b):C$, and applying $k:C \to \bot$ gives $k(f(b)):\bot$. Discharging $b$ gives $\neg B$. Applying $q:\neg\neg B$ to this proof of $\neg B$ gives $\bot$. Thus the temporary assumption $f:B \to C$ leads to $\bot$, so we have constructed $\neg(B \to C)$. Applying $p:\neg\neg(B \to C)$ to this refutation gives $\bot$. Since the temporary assumption $k:C \to \bot$ led to $\bot$, we discharge $k$ and obtain $\neg\neg C$. Discharging $q$ and then $p$ proves $\mathrm{IPC} \vdash \neg\neg(B \to C) \to \bigl(\neg\neg B \to \neg\neg C\bigr)$. [/guided] [/step] [step:Run the induction over the classical derivation] We prove the induction assertion $\mathrm{IPC} \vdash \neg\neg D_j$ for every $j \in \{1,\dots,m\}$. If $D_j$ is an $\mathrm{IPC}$ axiom, the assertion follows from the double-negation conversion for intuitionistic theorems. If $D_j$ is an excluded-middle axiom, then $D_j$ has the form $B \vee \neg B$ for some $B \in \mathcal{L}$, and the assertion follows from the intuitionistic proof of $\neg\neg(B \vee \neg B)$. It remains to handle the case in which $D_j$ is obtained by modus ponens. Then there exist indices $r,s < j$ and formulas $B,C \in \mathcal{L}$ such that $D_r = B$, $D_s = B \to C$, and $D_j = C$. By the induction hypothesis, $\mathrm{IPC} \vdash \neg\neg B$ and $\mathrm{IPC} \vdash \neg\neg(B \to C)$. Using the double-negation modus ponens formula proved above, two applications of modus ponens inside $\mathrm{IPC}$ give $\mathrm{IPC} \vdash \neg\neg C$. Since $D_j = C$, this is exactly $\mathrm{IPC} \vdash \neg\neg D_j$. [/step] [step:Apply the induction to the final line] The induction applies to every line of the fixed $\mathrm{CPC}$ derivation. Since the final line is $D_m = A$, we obtain $\mathrm{IPC} \vdash \neg\neg D_m$. Substituting $D_m = A$ gives $\mathrm{IPC} \vdash \neg\neg A$. This proves Glivenko's theorem. [/step]