形式主义、直觉主义与柏拉图主义

此定理是课堂上展示形式主义/柏拉图主义与直觉主义分歧的最尖锐例子:古典(非构造性)证明通过对一个未判定命题进行分情形来确立存在性,却从不告诉你哪种情形是真实的,而构造性证明给出显式的值。

古典(非构造性)证明。 考虑 $\sqrt{2}^{\sqrt{2}}$。由排中律,要么 $\sqrt{2}^{\sqrt{2}} \in \mathbb{Q}$ 要么 $\sqrt{2}^{\sqrt{2}} \notin \mathbb{Q}$——我们不需要知道是哪一种。

情形1: 若 $\sqrt{2}^{\sqrt{2}} \in \mathbb{Q}$,取 $a = \sqrt{2}^{\sqrt{2}}, b = \sqrt{2}$:两者都是无理数($\sqrt{2}$ 是无理数,由 $p/q=\sqrt 2$ 中 $p,q$ 奇偶性的经典反证法可得),而根据本情形假设 $a^b = \sqrt{2}^{\sqrt{2}}$ 是有理数。得证。

情形2: 若 $\sqrt{2}^{\sqrt{2}} \notin \mathbb{Q}$,取 $a = \sqrt{2}^{\sqrt{2}}$(由本情形假设为无理数)与 $b = \sqrt{2}$(无理数)。则 $a^b = 2$:$a^b = (\sqrt{2}^{\sqrt{2}})^{\sqrt{2}} = \sqrt{2}^{2} = 2$。因为 $2 \in \mathbb{Q}$,得证。

无论哪种情形,我们都给出了无理数 $a,b$ 使 $a^b \in \mathbb{Q}$——但证明从未告诉我们哪种情形成立,即 $\sqrt{2}^{\sqrt 2}$ 本身是有理数还是无理数。形式主义者立即接受这一点(这是古典一阶逻辑中有效的推导);直觉主义者拒绝将其视为真正的存在性证明,因为它没有产生一个明确的单一 $(a,b)$ 组以及证明正是这一组可行的证明。

构造性证明(消除分情形)。 取 $a = \sqrt{2}$ 及 $b = \log_2 9$。两者都是无理数:$\sqrt 2$ 无理性如上;$\log_2 9$ 无理是因为若 $\log_2 9 = p/q$(最简分数,$q>0$)则 $2^{p/q}=9$,于是 $2^p = 9^q$,但左边是 $2$ 的幂而右边是 $3$ 的幂(当 $q \ge 1$ 时 $9^q$ 只有素因子 $3$),迫使 $p=q=0$,与 $9^q=2^p>1$ 矛盾。

现在显式计算:$a^b = \sqrt{2}^{\log_2 9} = 2^{\frac{1}{2}\log_2 9} = 2^{\log_2 3} = 3$,利用 $\sqrt{2} = 2^{1/2}$,故 $a = \sqrt{2}, b = \log_2 9$ 给出 $a^b = (2^{1/2})^{\log_2 9} = 2^{\frac{1}{2}\log_2 9} = 2^{\log_2 3} = 3 \in \mathbb{Q}$。

这次没有分情形,没有未解决的析取——证明1中原本悬而未决的问题(即 $\sqrt2^{\sqrt2}$ 是否有理?)被完全绕开,任何直觉主义者都接受组 $(\sqrt{2}, \log_2 9)$ 为真正的见证。(历史注记:Gelfond–Schneider(1934年)后来证明 $\sqrt{2}^{\sqrt 2}$ 实际上是无理数——实际上是超越数——从而确定情形2为"真实"的一种,但上述古典证明不需要这样一个深刻定理。)

柯尔莫哥洛夫(1925年)与哥德尔(1933年)各自独立地证明古典逻辑可通过这种"否定翻译"嵌入直觉主义逻辑:你永远无法恢复完整的排中律,但总能恢复其双重否定,这正是将古典算术证明嵌入直觉主义系统所需要的,是后来形式化证明助手中的关键一步。

第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$ 的否定翻译(将每个原子公式和每个联结词替换为其双重否定的直觉主义类似物)来解释古典数学,该翻译将每个古典可证的算术语句都送到一个直觉主义可证的语句。