Existence of Irrational $a,b$ with $a^b$ Rational — Classical vs. Constructive

Classical (non-constructive) proof. Consider $\sqrt{2}^{\sqrt{2}}$. By the law of excluded middle, either $\sqrt{2}^{\sqrt{2}} \in \mathbb{Q}$ or $\sqrt{2}^{\sqrt{2}} \notin \mathbb{Q}$ — we do not need to know which.

Case 1: if $\sqrt{2}^{\sqrt{2}} \in \mathbb{Q}$, take $a = \sqrt{2}^{\sqrt{2}}, b = \sqrt{2}$: both are irrational ($\sqrt{2}$ is irrational by the classic proof-by-contradiction on parity of $p,q$ in $p/q=\sqrt 2$), and $a^b = \sqrt{2}^{\sqrt{2}}$ is rational by assumption of this case. Done.

Case 2: if $\sqrt{2}^{\sqrt{2}} \notin \mathbb{Q}$, take $a = \sqrt{2}^{\sqrt{2}}$ (irrational by this case's assumption) and $b = \sqrt{2}$ (irrational). Then $a^b = 2$: $a^b = (\sqrt{2}^{\sqrt{2}})^{\sqrt{2}} = \sqrt{2}^{2} = 2$. Since $2 \in \mathbb{Q}$, done.

Either way we have exhibited irrational $a,b$ with $a^b \in \mathbb{Q}$ — but the proof never tells us which case holds, i.e. whether $\sqrt{2}^{\sqrt 2}$ itself is rational or irrational. A Formalist accepts this immediately (it is a valid derivation in classical first-order logic); an Intuitionist rejects it as a genuine existence proof because it produces no single explicit $(a,b)$ pair together with a proof that that specific pair works.

Constructive proof (removes the case split). Take $a = \sqrt{2}$ and $b = \log_2 9$. Both are irrational: $\sqrt 2$ irrational as above; $\log_2 9$ irrational because if $\log_2 9 = p/q$ in lowest terms with $q>0$ then $2^{p/q}=9$, so $2^p = 9^q$, but the left side is a power of $2$ and the right side a power of $3$ (for $q \ge 1$, $9^q$ has only the prime factor $3$), forcing $p=q=0$, contradicting $9^q=2^p>1$.

Now compute explicitly: $a^b = \sqrt{2}^{\log_2 9} = 2^{\frac{1}{2}\log_2 9} = 2^{\log_2 3} = 3$, using $\sqrt{2} = 2^{1/2}$, so $a = \sqrt{2}, b = \log_2 9$ gives $a^b = (2^{1/2})^{\log_2 9} = 2^{\frac{1}{2}\log_2 9} = 2^{\log_2 3} = 3 \in \mathbb{Q}$.

This time no case split, no unresolved disjunction — Fact 2's original open question (is $\sqrt2^{\sqrt2}$ rational?) is bypassed entirely, and any Intuitionist accepts the pair $(\sqrt{2}, \log_2 9)$ as a genuine witness. (Historical footnote: Gelfond–Schneider (1934) later proved $\sqrt{2}^{\sqrt 2}$ is in fact irrational — indeed transcendental — resolving Case 2 as the "true" one, but the classical proof above needed no such deep theorem.)