哥德尔–柯尔莫哥洛夫双重否定翻译

第1步:固定我们可使用的直觉主义规则。 直觉主义逻辑保留分离规则以及 $\wedge, \vee, \to$ 的自然演绎规则,并定义 $\neg P := (P \to \bot)$,其中 $\bot$ 表示荒谬("从 $\bot$ 的证明可推出任何东西"——爆炸原理——在直觉主义中成立)。不被假设的是 $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$ 无需任何分情形即成立——这个方向从未需要排中律。

**第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$ 一般不可推导(那将需要我们恰好缺乏的类排中律原理)。因此这个翻译确实更弱:它表明古典逻辑的"定律"即使无法被直接断言,也能作为一个不可反驳的命题(其否定总是矛盾的)幸存下来——正是这个缝隙让构造性数学得以与古典数学共存,并通过哥德尔对每个公式 $\phi \mapsto \phi^N$ 的否定翻译(将每个原子公式和每个联结词替换为其双重否定的直觉主义类似物)来解释古典数学,该翻译将每个古典可证的算术语句都送到一个直觉主义可证的语句。