FOM: Re: (ir)rational numbers

[Harvey Friedman]

Shuster 6/19/00 3:06PM wrote:

>>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).
>
>That's a good point: one has to alter the example in the following way:
>Are there two *algebraic* irrational numbers x,y such that x^y is rational?

The well known theorem of Gelfond and Schneider tells us that if x,y are
two algebraic numbers, x not 0 or 1, y irrational, then x^y is
transcendental. Using well known technology, it is clear that this
statement can be put into Pi-0-2 form. So, e.g., if the usual proof is
formalizable in PA, then one can convert it into a proof in HA. The proof
is therefore likely to be constructive - or easily made so - by direct
examination. It would be interesting to see just what the estimates are.

>>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.
>
>Well, one has proven that not both e+pi and e-pi can be rational/algebraic.
>That's all, a simple result with an appropriately simple proof. What else?
>Presumably not a proof of "either e+pi or e-pi is irrational/transcendental.

Yes, a (classical) proof that either e+pi or e-pi is transcendental. But
not a constructive one. This can be put into a form that is closer to
Richman's as follows:

THEOREM 1. (Classically proved, but no constructive proof known). There
exists a nonzero integer n such that e + n(pi) is transcendental.

THEOREM 2. (Constructively proved). There are no two distinct integers n,m
for which e + n(pi) and e + m(pi) are algebraic.

>>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?
>
>"A real number r is irrational" should mean that r is distinct
>from each rational number, where "to be distinct from" ought to
>be understood as "has postive distance from". My feeling is that
>this is just what we have in mind when we talk about irrationals;
>it's at least this what we expect from them.

I wasn't asking for a tutorial on constructivity. My "What does it mean?"
refers to my "contain". Note the possible working answers I gave there in
1:20PM 6/16/00.

In a recent talk at Leeds (the BMC's 2000 celebration), I gave what may be
the first example of a mathematically attractive arithmetic statement that
is easily proved classically but *KNOWN* to be unprovable constructively
(under Church's Thesis, or at least unprovable in any standard
intuitionistic system):

Every multivariate polynomial from Z to Z takes on a value of least magnitude.

In particular, HA + CT proves the negation of the above.

We need more examples like this. There are many even more attractive
candidates for which it seems hopelessly difficult to prove that they have
no constructive proofs.