The following argument is often cited as an example of the necessity of the law of excluded middle and classical logic. We are supposed to demonstrate the existence of two irrational numbers $a$ and $b$ such that their power $a^b$ is rational. By the law of excluded middle, $\sqrt{2}^{\sqrt{2}}$ is rational or not. If it is rational, take $a = b = \sqrt{2}$, otherwise take $a = \sqrt{2}^{\sqrt{2}}$ and $b = \sqrt{2}$. In either case $a^b$ is rational. Let us think about this for a moment, from constructive point of view.

The law of excluded middle is supposed to be used in an essential way here because we do not know whether $\sqrt{2}^{\sqrt{2}}$ is rational. As a matter of fact, it is irrational, so the “essential” use stems from our supposed ignorance, not from a genuine mathematical fact. The argument therefore demonstrates that the law of excluded middle is an excellent way of supporting one’s ignorance (which can be good in many ways, just like good programming languages support programmer’s laziness).

But how hard is it to give a concrete example of two irrational numbers $a$ and $b$ such that $a^b$ is rational? Not hard at all! Take $a = \sqrt{2}$ and $b = 2 \log_2 3$. It is easy to prove that both are irrational, in fact showing that $b$ is irrational is easier than showing that $a$ is. And we have $a^b = 2^{\log_2 3} = 3$. After seeing this *constructive* argument, the *classical* one looks even sillier and just an uneccesary complication. The moral of the story is that constructive mode of thinking should be the default because it produces simpler and concrete mathematics. Only switch to the classical mode if you really have to (and even then, don’t).

Made me think of the example at cut-the-knot.org, which shows that ${\sqrt{2}^\sqrt{2}}^\sqrt{2}$ is rational.

Derek, the link you posted does no such thing. It is exactly the classical argument I outlined above.

But surely, it’s a moot point? $a = \sqrt{2}^{\sqrt{2}}$ is known to be irrational. (Though I admit I haven’t checked the constructive validity of the Gelfond-Schneider theorem.) Moreover, I’ve never seen this famous “non-constructive proof” used as an argument against constructive logic before (I don’t regularly read Wikipedia). It was presented to me as an interesting thought experiment about the nature of disjunction back when I was a student.

P.S. I was curious enough to google “constructive gelfond schneider theorem”. The second and fifth hits are somewhat interesting:

2. http://en.wikipedia.org/wiki/Constructive_proof

(which, unlike the article on excluded middle, makes both points above: yours and mine)

5. http://cs.nyu.edu/pipermail/fom/2005-March/008843.html

The similar problem for $\pi+e$ is considered to be a Mathematical Embarrassment:

http://rjlipton.wordpress.com/2009/12/26/mathematical-embarrassments

An intuitionist logic professor told me that once he was trying to solve a problem from his own book preparing for the next day’s undergrad logic lecture. After hours of unsuccessful thinking he noticed that he was not able to solve it because he was not using PEM. :)

I see the proof of the above theorem in a somewhat different way than “a useless example of non-constructive proof”. Let me make my point using a Car Analogy. You go to a car dealer, and he supplies a car to you, along with a guarantee: He must supply a -working- car to you, if needed. If you never use the car, the contract is implicitly satisfied, otherwise, if you do try to start the car, then two cases may occur: The car starts, and everything is fine, or the car does not start. In this case, you make use of your guarantee, and the dealer supplies a new, working car (or some other car with another guarantee). You do the same for your classical proof of existence of 2 irrational numbers $a$ and $b$ such that $a^b$ is rational: act as if $a=\sqrt{2}$ and $b=\sqrt{2}$ satisfy your theorem. If anyone calls you out on it, by supplying a proof that $\sqrt{2}^\sqrt{2}$ is irrational, you can “backtrack” by supplying new witnesses to your theorem: $a=\sqrt{2}^\sqrt{2}$ and $b=\sqrt{2}$. In a sense, the non-constructive proof does contain “less information” than the constructive proof. However it does supply a “guarantee” as in the above sense, that is you may use your witnesses with the caveat of perhaps needing to substitute them for “correct” witnesses at a further point.

Note though that the non-constructive argument proves something stronger than the constructive one, namely that there exist two irrational

algebraicnumbers $a$, $b$ such that $a^b$ is rational.@Terry: That’s a good point. Can we have a constructive proof of two irrational algebraic numbers whose power is rational?

@Terry: Hmm, actually I do not know what you mean if you have in mind the usual non-constructive proof involving $\sqrt{2}^\sqrt{2}$, because that number is transcedental, as it is the square root of the Gelfand-Schneider Constant.

You can rephrase the theorem into a classically equivalent form that better exposes the constructive content. The theorem may be stated as “it is not the case that for every irrational a and b the number a^b is irrational”. For suppose so. Classically, root 2 is irrational, so by the assumption root 2 to the root 2 power is irrational. So by the assumption again, root 2 to the root 2 to the root 2 is irrational. But this is just 2, which is eminently rational. Contradiction, and we are finished.

This is a perfectly constructive proof of a perfectly reasonable theorem (given that there is a constructive proof of the irrationality of root 2, which there is). But it is not constructively equivalent to the problematic-sounding existence statement. Classical mathematics treats the two forms of the theorem as completely interchangeable, but psychologically, at least, we know that they are not (because we can observe how people react when presented with one or the other form). In any case they are not intuitionistically equivalent, and this is a good thing because intuitionistically there is a difference of computational content between the two theorems.

Oh, damn, I overloaded the word “classically”. In the third sentence I meant “it is known since classical times that”, whereas elsewhere I mean “bivalent logic”.