[FOM] the power of nonconstructive reasoning

[Gabriel Stolzenberg]

   In around 1970, in a lecture entitled, "Aspects of Constructivism,"
Errett Bishop presented a trivial yet pretty observation in number
theory, which I will reconstruct below.  Although I never discussed it
with him, knowing both him and his style of mathematics, he might well
have thought of it as a comment on the following popular illustration
of the alleged power and simplicity of classical reasoning. [See also
the posting, "Benenson," by Robert Black Nov 5.  However, Black says
only that "introductory treatments of the notion of nonconstructive
proof almost always give [it] as an example."  Another popular example
is (or, at least, was) what is often alleged to be Euclid's proof of
the infinitude of primes.  See, for example, Hardy's "A Mathematician's
Apology."]

   Proposition.  There are irrational numbers, x and y, such that
                 x^y is rational.

   Proof.  Set x = sqrt(2).  If x^x is rational, we are done.  If
not, x^x and x are irrational and (x^x)^x = 2.  So we are done.

   This is an extremely simple and elegant "nonconstructive" proof
of the existence of such a pair of irrationals. The one time I recall
seeing this proof in a lecture, it seemed to be taken for granted
that getting a constructive proof would be harder, messier and not
worth the effort.

   However, if, for example, x = sqrt(2) and y = 2log_2(3), which is
irrational (because if log_2(3) = m/n, then 3^n, which is odd, equals
2^m, which is even), then x^y = 3.  So, we are done.

   Here is Bishop's observation.

           1.  For all x, (2^x)^(1/x) = 2.

           2.  The set S of irrational x for which 2^x
               is also irrational is the complement of
               a countable subset of R and, hence, an
               uncountable, dense subset of it.

   Proof of 2.  S is the complement of the union of the set of
rationals and its image under the mapping, r -> log_2(r), both
of which are countable.  (Note that 2^x = y iff x = log_2(y).)


   Gabriel Stolzenberg