有理数となる無理数 $a,b$ の $a^b$ の存在——古典と構成

古典的(非構成的)証明。 $\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が「真」であることを解決したが、上記の古典的証明はそのような深い定理を必要としなかった。)