Formalism, intuitionism and Platonism

This theorem is the sharpest classroom illustration of the Formalist/Platonist vs Intuitionist divide: the classical (non-constructive) proof establishes existence via a case split on an undecided proposition, never telling you which case is real, while the constructive proof exhibits explicit values.

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.)

Kolmogorov (1925) and Gödel (1933) independently showed classical logic embeds into intuitionistic logic via this "negative translation": you never regain full LEM, but you can always recover its double negation, which is exactly what is needed to embed classical arithmetic proofs into an intuitionistic system, a key step in later formalized proof assistants.

Step 1: Fix the intuitionistic rules we may use. Intuitionistic logic keeps modus ponens and the natural deduction rules for $\wedge, \vee, \to$, and defines $\neg P := (P \to \bot)$ where $\bot$ is absurdity ("from a proof of $\bot$, anything follows" — ex falso quodlibet — is intuitionistically valid). What is not assumed is $P \vee \neg P$ or the double-negation elimination law $\neg\neg P \to P$.

**Step 2: Prove the easy direction $P \to \neg\neg P$ intuitionistically.** Assume a proof of $P$. We must produce a proof of $\neg\neg P = (( P \to \bot) \to \bot)$, i.e. assume a proof of $(P \to \bot)$ and derive $\bot$. Applying this assumed function to our proof of $P$ directly yields a proof of $\bot$. So $P \to \neg\neg P$ holds with no case analysis — this direction never needed LEM.

**Step 3: Build a proof of $\neg\neg(P \vee \neg P)$ directly.** We must show $((P \vee \neg P) \to \bot) \to \bot$. Assume a proof $h$ of $(P \vee \neg P) \to \bot$ (i.e. $h$ refutes the disjunction); we must derive $\bot$. Observe that $h$, restricted to the right disjunct, gives a function taking any proof of $P$ to a proof of $\bot$ — that is exactly a proof of $\neg P$ (apply $h$ after wrapping with the right-injection $\text{inr}$). Call this derived proof $n : \neg P$.

Step 4: Close the loop. Since we have $n : \neg P$, we can form $\text{inr}(n) : P \vee \neg P$ (the right disjunct of $P \vee \neg P$, instantiated with proof $n$). Feed this term back into $h$: $h(\text{inr}(n))$ is a proof of $\bot$, exactly the $\bot$ we needed to derive in Step 3. This closes the assumption from Step 3, giving a full intuitionistic proof of $\neg((P\vee\neg P)\to\bot)$, i.e. of $\neg\neg(P \vee \neg P)$.

*Step 5: Why this does not* give $P \vee \neg P$ back.** Step 4 produces $\neg\neg(P \vee \neg P)$, but intuitionistically $\neg\neg Q \to Q$ is not generally derivable (that would require the very LEM-like principle we lack). So the translation is genuinely weaker: it shows classical logic's "law" survives as an irrefutable statement (its negation is always contradictory) even where it cannot be asserted outright — precisely the gap that lets constructive mathematics coexist with, and interpret, classical mathematics via Gödel's negative translation of every formula $\phi \mapsto \phi^N$ (replacing each atomic formula and each connective with its double-negated intuitionistic analogue), which sends every classically-provable arithmetic sentence to an intuitionistically-provable one.