Constructive gem: irrational to the power of irrational that is rational
- 28 December 2009
- Gems and stones, Constructive math
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).
andrejbauer@mathstodon.xyz, I will
gladly respond.
You are also welcome to contact me directly.
Comments
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
[...] 引用原文：irrational to the power of irrational that is rational [...]
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 algebraic numbers $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".
What is $2^{\sqrt{2}}, I mean it is rational or irrational?
As far I as I know $2^{\sqrt{2}}$ is irrational, but I do not know how to prove this. Perhaps someone can refer us to a relevant theorem.
It's transcendental. This is immediate from the Gelfond-Schneider theorem. Relatedly, referring back to Andrej's 2011 question, an exponential built from two algebraic irrationals must be transcendental, again by G-S.
In the constructive proof we show witnesses to the claim that there are two irrational numbers $$a$$ and $$b$$ such that $$a^{b}$$ is irrational, and we do this without using LEM. But this proof relies on the proposition that for any two real numbers $$a$$ and $$b$$, $$a^{\log{a}b} = b$$. Maybe we are using LEM in the proof of this proposition? Or did we actually compute the value of $$2^{\log_{2}3}$$ and found it to be 3? And also, what would be a constructive definition of logarithm? Is it an algorithm that computes $$\log_{a}b$$ for any real number $$a$$ and $$b$$? My point is, without some further clarification, the constructive proof looks just like a classical proof that picks out two numbers. It is not using LEM on the surface, but I am not sure if we have managed to avoid it completely; so I hesitate to call this proof constructive, and I know that this is a famous example of constructive proof.
@Koray: Of course this needs to be checked, but constructively exponentials and logarithms work as expected. For instance, "Foundations of Constructive Analysis" by Bishop & Bridges develops enough real analysis, and in particular of convergent power series, to show that there are no surprises.