FOM: my non-constructive proof

[Harvey Friedman]

Comment on Richman 6/16/00 10:13AM.

>This situation is similar to the classic example of the existence of
>two irrational numbers, x and y, such that x^y (exponentiation) is
>rational. Let a = sqrt 2 and consider the two candidates a^a and
>(a^a)^a = 2. If a^a is rational, the first candidate does it; if not,
>the second does it. This is not a constructive proof even though the
>construction is staring us in the face.

This is not such a good example since it is well known that the existence
of two irrationals, x,y, such that x^y is rational can be proved
constructively. Take x = e and y = ln(2).

A better example, not due to me, is the following.

THEOREM. e + pi is irrational or e - pi is irrational.

Proof: Suppose e + pi and e - pi are rational. Then by addition, 2e is
rational. Contradiction.

One can also prove that e + pi is transcendental or e - pi is
transcendental in this way.

This raises the following question. Does the above proof "contain" a proof
that e + pi is irrational? Obviously not. But how do you prove that?

FIrst of all, what does it mean?

Here is a crude formulation. Note that the above proof is tiny when
appropriately formalized. Can we at least prove that there is no similarly
tiny proof that e + pi is irrational?