[FOM] Intuitionists and excluded-middle

[Dana Scott]

Several correspondents have pointed out how easy it
is to see that between any two irrationals there is
another irrational.  But a few questions remain.

First, the Halmos trick using the LEM is as follows.
Assume a and b are irrational and a < b.  Now the
average lies between, but it might be rational.
So, divide the interval [a, b] into THIRDS:

     a < (2 a + b)/3 < (a + 2 b)/3 < b.

A moments thought (left to the reader) shows that
not BOTH of the intermediate points can be rational.
However, this does not show WHICH of the two is irrational.
(Actually we need only assume that EITHER a OR b is
irrational for this argument to work.)

The argument with averages is not so bad, however.  Consider
TWO averages:

     a < (3 a + b)/4 < (a + b)/2 < b.

By the LEM, (a + b)/2 is rational or irrational.  If
it is rational, then (3 a + b)/4 must be irrational,
because

     a = (3 a + b)/2 - (a + b)/2 .

Now, this thought shows that if CONSTRUCTIVELY we
argue by the (correct) Archimedean Principle,
that there is an integer n > 0 with 1/n < (b - a), then

     a < a + 1/n < b,

and clearly a + 1/n is irrational if a is.

So here is the question:  If a < b and both are RATIONAL,
then we see that

     a < a + (b - a) sqrt(2)/2 < b,

and that intermediate point is IRRATIONAL.

So, constructively, we ask: Can there be a CONTINUOUS function f
such that if a < b and both are irrational, then

     a < f(a,b) < b,

and f(a,b) is always irrational as well?  This could be related
to the question as to whether there is a continuous function g
such that for an ARBITRARY pair a < b we would have

     a < g(a,b) < b,

and g(a,b) is always RATIONAL?  Somehow I think not, but I could
not get a proof.

(Surely you cannot map the whole plane into the rationals in a
non-trivial way.  But could you map the irrational plane non-trivially
to the irrationals?  We did map the rational plane nicely to the
irrationals.  OK, by "plane" here I mean the HALF-plane where a < b.)