About the proof of the proposition "there exists irrational numbers a, b such that a^b is rational" 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?
 A: 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.
A: 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.    
A: 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 non-constructivity 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.  
A: 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. 
