[FOM] Intuitionists and excluded-middle

[Dana Scott]

"Lew Gordeew" <legor at gmx.de> wrote:

> But this is very important for most mathematicians. Most students of
> mathematics immediately ask "hey, but which x is the solution - sqrt 
> (2) or
> sqrt(2)^sqrt(2)?"  Now Analysis says it is sqrt(2)^sqrt(2), but  
> clearly the
> LEM proof does no good to this end. I must confess though that our  
> comp sci
> students are less concerned with the answer because they don't know  
> much
> about irrational numbers. :-) :-(

The sqrt(2) argument is fun to consider, especially as the proof of the
irrationality of sqrt(2)^sqrt(2) is hard.  But there are many ways to
give explicitly irrationals a and b so that a^b is rational, where the
proof is fairly elementary.  (I think this has been posted before.)

Consider e, the basis for natural logarithms.  From the power-series
expansion of e^x, it is not hard to argue that each integral power
e^n is irrational. (Hint: consider all those fractions with large
factorials in the denominators.)

Next, consider the natural logarithm, ln(2).  If this were a rational
p/q, then we could conclude that 2^q = e^p, which is impossible.  So,
one solution to the puzzle is to take a = e and b = ln(2).  (Other
examples, perhaps more elementary, can be found by using logs to bases
such as sqrt(3).)

Here is another puzzle asking for a very quick proof using LEM (first
pointed out to me by Paul Halmos): From the construction of the reals
we know that between any two irrationals there is a rational.  Show that
there is also an irrational.  (Hint:  If the irrationals are a < b, then
the average (a+b)/2 is a bad answer because it might be rational.)
Second question: What is a more constructive proof?