What does the classical proof of the proposition "there exists irrational numbers a, b such that $a^b$ is rational" want to reveal? I know it has something to do with the difference between classical and constructive mathematics but am not quite clear about it. Materials I found online does not give quite clear explanations either. Could someone give a better explanation?

2$\begingroup$ It is sad that this is a researchlevel question. $\endgroup$ – Andrej Bauer Mar 24 '15 at 13:19

2$\begingroup$ @AndrejBauer: remember that MathOverflow had a slightly wider remit in 2011; I suspect that if this were asked today, it would get migrated to math.stackexchange. $\endgroup$ – Peter LeFanu Lumsdaine Mar 24 '15 at 14:06
Presumably, the proof you have in mind is to use $a=b=\sqrt2$ if $\sqrt2^{\sqrt2}$ is rational, and otherwise use $a=\sqrt2^{\sqrt2}$ and $b=\sqrt 2$. The nonconstructivity here is that, unless you know some deeper number theory than just irrationality of $\sqrt 2$, you won't know which of the two cases in the proof actually occurs, so you won't be able to give $a$ explicitly, say by writing a decimal approximation.

4$\begingroup$ @David : The second one is the rational one. en.wikipedia.org/wiki/Gelfond–Schneider_theorem $\endgroup$ – Andy Putman Feb 28 '11 at 23:01

15$\begingroup$ I think the reason the $\sqrt{2}$ case is interesting is that the proof that $\sqrt{2}$ is irrational is very easy, and taught to young undergraduates. But the Gelfond–Schneider theorem is much more advanced. So for a student who is not very advanced, this gives a nice example of an existence proof where the student isn't in possession of a proof that any particular number is a witness. That's a nice pedagogical tool to develop students' intuition that the proof of an existence statement does not have to construct the thing that is shown to exist. Examples like $e^{\ln(2)} = 2$ don't do that. $\endgroup$ – Carl Mummert Mar 2 '11 at 15:23

3$\begingroup$ Carl's remark is right on the money. I have used exactly this example in a sophomorelevel introduction to proofs course for exactly this purpose. (Unfortunately the most common reaction was utter confusion...) $\endgroup$ – Pete L. Clark Apr 24 '11 at 22:10

5$\begingroup$ @Carl, Pete: I think that the strategystealing proof that the first player has a winning strategy at Chomp (en.wikipedia.org/wiki/Chomp) is also a good example to convince students of this fact. $\endgroup$ – Maxime Bourrigan Apr 25 '11 at 1:20

2$\begingroup$ I just feel like saying $(\sqrt{2})^{\log_2 9}$. But more seriously, it is unpedagocial to speak about what we know and do not know when explaining the form of a given proof. The proof in question is not constructive because it employs the inference rule of excluded middle  and the proof remains nonconstructive no matter what else you prove or know. However, the proof can be transformed to a different proof which is constructive (assuming there is a constructive proof of irrationality of $\sqrt{2}^{\sqrt{2}}$). $\endgroup$ – Andrej Bauer Mar 24 '15 at 13:15
The proposition can also be proved without explicitly knowing any particular irrational number:
Fix a positive rational number $c$. Then for any positive irrational real number number $a$, the equation $a^b = c$ has a solution, and the solutions for different $a$ are different. Now assume that there would be no irrational numbers $a$ and $b$ such that $a^b$ is rational. Then all these solutions would be rational, thus we would have an injective mapping from the positive irrational real numbers to the rationals; however we know that the rationals are countable and the positive irrational reals are not, so there is no such injection, and we have a contradiction.



$\begingroup$ @EmilJeřábek — Ah, of course! Thanks! I don't know in which way I was thinking, but somehow I wanted to map pairs $(a,b)$ or $(a,c)$ into the rationals, or something like that. But this is nice: simple and elegant, and it brilliantly does the job. $\endgroup$ – jmc Mar 24 '15 at 12:14

2$\begingroup$ This proof can be made constructive easily enough. It is a constructive theorem (basically an exercise in Bishop and Bridges) that for any countable sequence, there is a positive real $x$ which differs from all its members. Using this, construct $x$ which differs from all rational $q$ and from all $c^q$ where $q$ is rational. Let $y$ be such that $x^y=c$. Then both $x$ and $y$ are irrational. $\endgroup$ – Matt F. Mar 24 '15 at 12:33
From a more abstract point of view, suppose you have a set $X$, a subset $\mathcal{I} \subset X$, an element $a \subset \mathcal{I}$ and a map $b : X \to X$ satisfying $b^n(a) \not\in \mathcal{I}$ for some $n$.
Then necessarily there exists $m$ such that $b^m(a) \in \mathcal{I}$ and $b^{m+1}(a) \not\in \mathcal{I}$.
The proof you refer to is not really mysterious; it's only presented to look mysterious, specifically by the choice of $\sqrt{2}$. There are plenty of choices for irrational $a$ and $b$, such that $a^{b^n}$ is rational for some $n$, and exactly the same conclusion can be drawn.
The classical proof You have mentioned shows how powerful logic may be. The crucial point of the proof is the use of the law of excluded middle (A or not(A)). In that case we are lucky to have knowledge of which of the two possibilities:
i) $\sqrt{2}^{\sqrt{2}}$ is rational or ii) $\sqrt{2}^{\sqrt{2}}$ is not rational
takes place to be. But You can imagine a statement A about natural numbers such that neither A nor not(A) is provable (in, say, ZFC). Now we may use analogously the particular statement of the law of excluded middle "A or not(A)" in some proof of some statement B. In that case the statement B is proved both by supposing A and by supposing not(A) and at the same time we know in advance that we shall not resolve which of the cases has the place to be. In such a proof the purely logical priciple of excluded middle becomes even more important (or at least as important) than the axioms of actual mathematical structure (in this case that of natural numbers). It is this power that made some mathematicians (e. g. intuitionists under the head of Brouwer) to think that logical principles such as that of exluded middle have caused the paradoxes discovered in the beginning of the XX century. For a classical mathematician the proof of B would be a legitimate proof since he/she believes that either A or not(A) is valid for natural numbers even if we shall never prove neither of them. (This position is often called platonism because it presupposes the "independent existence" of natural numbers.) Intuitionist, however, says that it is a hypothesis and to turn this reasoning into a valid proof one should prove that indeed one of those possiblities has the place to be.