形式主義・直観主義・プラトニズム

この定理は形式主義・プラトニズムと直観主義の対立を教室で示す最も鋭い例である:古典的(非構成的)証明は未決定命題に関する場合分けによって存在を確立するが、どちらの場合が実際なのかを決して教えてくれない一方、構成的証明は明示的な値を提示する。

古典的(非構成的)証明。 $\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 \in \mathbb{Q}$ となる無理数 $a,b$ を提示できたが、証明はどちらの場合が成り立つか、すなわち $\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)$ を真の証拠として受け入れる。(歴史的注記:ゲルフォント・シュナイダー(1934年)は後に $\sqrt{2}^{\sqrt 2}$ が実際に無理数——実は超越数——であることを証明し、場合2が「真」であることを解決したが、上記の古典的証明はそのような深い定理を必要としなかった。)

コルモゴロフ(1925年)とゲーデル(1933年)は独立に、この「否定翻訳」を通じて古典論理が直観主義論理に埋め込まれることを示した:完全なLEMを取り戻すことは決してできないが、その二重否定は常に取り戻すことができ、これはまさに古典的な算術証明を直観主義体系に埋め込むために必要なものであり、後の形式化された証明支援系における重要なステップである。

ステップ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$(各原子式と各接続詞をその二重否定直観主義類似物に置き換える)のゲーデルの否定翻訳を通じて、古典的に証明可能なあらゆる算術文を直観主義的に証明可能な文へ送る。