[proofplan] We construct a map from $\neg\neg P$ to $P$ using the given decision procedure for $P$. Given $n : \neg\neg P$, we perform [disjunction elimination](/theorems/4625) on the evidence $d : P \vee \neg P$. In the left branch we already have evidence for $P$, while in the right branch the evidence for $\neg P$ contradicts $n$, and ex falso supplies evidence for $P$. [/proofplan] [step:Construct the stability map from a decision of $P$] Assume evidence $d : P \vee \neg P$. Here $P \vee \neg P$ is the disjunction type with constructors $\operatorname{inl} : P \to P \vee \neg P$ and $\operatorname{inr} : \neg P \to P \vee \neg P$, the negation $\neg P$ means $P \to \bot$, and the double negation $\neg\neg P$ means $(P \to \bot) \to \bot$. To prove that $P$ is stable, we must construct a map $s : \neg\neg P \to P$. Let $n : \neg\neg P$ be arbitrary. We will define $s(n) : P$ by case analysis on the disjunction evidence $d$. [guided] The definition of stability asks for a construction that turns double-negated evidence into direct evidence. Thus, from the decision evidence $d : P \vee \neg P$, we must build a function $s : \neg\neg P \to P$. The disjunction $P \vee \neg P$ has two constructors: $\operatorname{inl} : P \to P \vee \neg P$, which packages positive evidence for $P$, and $\operatorname{inr} : \neg P \to P \vee \neg P$, which packages a refutation of $P$. To define $s$, take arbitrary evidence $n : \neg\neg P$. Since $\neg P$ means $P \to \bot$, the type $\neg\neg P$ means $\neg P \to \bot$, so this $n$ is a construction that converts any refutation of $P$ into an absurdity. The only remaining information available is the decision $d : P \vee \neg P$, so the natural construction is by disjunction elimination on $d$. [/guided] [/step] [step:Return the positive evidence in the left branch] If $d$ is of the form $\operatorname{inl}(p)$ for evidence $p : P$, define $s(n) := p$. This gives the required evidence for $P$ in the left branch. [/step] [step:Use contradiction and empty-proposition elimination in the right branch] If $d$ is of the form $\operatorname{inr}(r)$ for evidence $r : \neg P$, then $n(r) : \bot$ because $n : \neg P \to \bot$. By the elimination rule for the empty proposition $\bot$, also called [ex falso quodlibet](/theorems/7496), from $n(r) : \bot$ we obtain evidence for $P$. Define $s(n)$ in this branch to be that evidence. [guided] Now suppose the decision evidence takes the negative form $\operatorname{inr}(r)$, where $r : \neg P$. The assumption $n : \neg\neg P$ is, by definition, a map $n : \neg P \to \bot$. Therefore we may apply $n$ to the specific refutation $r : \neg P$, obtaining $n(r) : \bot$. This is an absurdity. The elimination rule for the empty proposition, also called ex falso quodlibet, says that from evidence of $\bot$ one may construct evidence of any proposition. Applying this rule to the proposition $P$ and the contradiction $n(r) : \bot$, we obtain evidence for $P$. This defines $s(n) : P$ in the right branch. [/guided] [/step] [step:Conclude that decidability implies stability] The two branches define $s(n) : P$ for arbitrary $n : \neg\neg P$. Hence we have constructed $s : \neg\neg P \to P$. Therefore $P$ is stable. Since the construction used only the given evidence $d : P \vee \neg P$, every decidable proposition is stable. [/step]