Eric Schechter
Vanderbilt University
-------------------------------------------------------------------------
Sketch of the example:
To make this message readable with ordinary ascii text, I'll use
^ to denote exponentiation, and use T to denote the square root
of 2.
We ask the question: Do there exist positive, irrational numbers
a and b, such that a^b is rational?
A simple nonconstructive proof of existence goes as follows:
We don't know whether T^T is rational. (Actually, we do know,
if we use the Gelfond-Schneider Theorem, but that's beside
the point -- assume we're just college students, and we can't
use anything that sophisticated.) However, we do know that
either T^T is rational or it is irrational.
If T^T is rational, then use a=b=T and we're done.
If T^T is irrational, then use a=T^T and b=T; a short computation
shows that a^b = 2 and we're done.
So we have proved the existence of numbers a and b, but
we haven't actually found them. This is a classic example
showing that the Law of the Excluded Middle (or equivalently,
Proof by Cases, or Proof by Contradiction), though valid
in classical logic, is not a theorem of intuitionist logic (a
type of constructivism).
End of example.
In case you're wondering, here are some facts that
are related to the arithmetic, but not to the logic:
(i) T^T is irrational, by the Gelfond-Schneider Theorem.
That's a very deep theorem.
(ii) For a short constructive proof of a^b, use
a = square root of 2 and b = log (base 2) of 9.
It's easy to show that those are both irrational.