[FOM] the power of nonconstructive reasoning

Gabriel Stolzenberg gstolzen at math.bu.edu
Tue Nov 6 20:35:08 EST 2007

   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

   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

More information about the FOM mailing list