ゲーデル・コルモゴロフ二重否定変換

ステップ1:使用可能な直観主義規則を固定する。 直観主義論理はモーダスポネンスと $\wedge, \vee, \to$ の自然演繹規則を保持し、$\neg P := (P \to \bot)$ と定義する($\bot$ は矛盾であり、「$\bot$ の証明から何でも従う」——ex falso quodlibet——は直観主義的に妥当)。仮定されないのは $P \vee \neg P$ または二重否定除去則 $\neg\neg P \to P$ である。

**ステップ2:易しい方向 $P \to \neg\neg P$ を直観主義的に証明する。** $P$ の証明を仮定する。$\neg\neg P = (( P \to \bot) \to \bot)$ の証明、すなわち $(P \to \bot)$ の証明を仮定して $\bot$ を導く必要がある。この仮定された関数を $P$ の証明に直接適用すると $\bot$ の証明が得られる。したがって $P \to \neg\neg P$ は場合分けなしに成り立つ——この方向はLEMを一切必要としなかった。

**ステップ3:$\neg\neg(P \vee \neg P)$ の証明を直接構築する。** $((P \vee \neg P) \to \bot) \to \bot$ を示す必要がある。$(P \vee \neg P) \to \bot$ の証明 $h$(すなわち $h$ は選言を反証する)を仮定し、$\bot$ を導く必要がある。$h$ を右選言肢に制限すると、$P$ の任意の証明を $\bot$ の証明に写す関数が得られる——これはまさに $\neg P$ の証明である(右注入 $\text{inr}$ で包んでから $h$ を適用)。この導出された証明を $n : \neg P$ と呼ぶ。

ステップ4:輪を閉じる。 $n : \neg P$ を持つので、$\text{inr}(n) : P \vee \neg P$($P \vee \neg P$ の右選言肢、証明 $n$ で具体化)を形成できる。この項を $h$ に戻す:$h(\text{inr}(n))$ は $\bot$ の証明であり、まさにステップ3で導く必要のあった $\bot$ である。これによりステップ3の仮定が閉じられ、$\neg((P\vee\neg P)\to\bot)$、すなわち $\neg\neg(P \vee \neg P)$ の完全な直観主義的証明が得られる。

**ステップ5:なぜこれは $P \vee \neg P$ を取り戻さないのか。** ステップ4は $\neg\neg(P \vee \neg P)$ を生成するが、直観主義的には $\neg\neg Q \to Q$ は一般には導出できない(それにはまさに我々が欠いているLEM的原理が必要となる)。したがってこの翻訳は本質的により弱い:古典論理の「法則」が、直接主張できない場合でも反駁不可能な言明(その否定は常に矛盾する)として生き残ることを示している——これがまさに、構成的数学が古典数学と共存し、それを解釈することを可能にする隙間であり、すべての式 $\phi \mapsto \phi^N$(各原子式と各接続詞をその二重否定直観主義類似物に置き換える)のゲーデルの否定翻訳を通じて、古典的に証明可能なあらゆる算術文を直観主義的に証明可能な文へ送る。