[FOM] Intuitionists and excluded-middle

[Harvey Friedman]

On 10/21/05 1:45 PM, "Dana Scott" <dana.scott at cs.cmu.edu> wrote:

> 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.)

These questions make perfectly good sense both classically and
constructively.

1. Classically. It is well known that the irrational line is homeomorphic to
the Baire Space N^N. In fact, there is a homeomorphism which is an order
isomorphism, where Z x N^N is linearly ordered lexicographically. It is easy
to construct a continuous function f:Z x N^N x Z x N^N into Z x N^N such
that if a,b in Z x N^N and a < b, then a < f(a,b) < b.

Also, Z x N^N x Z x N^N is obviously homeomorphic to Z x N^N by mixing.

Clearly there is a continuous function g:Z x N^N x Z x N^N into Z x N^N such
that for all a < b, we have a < g(a,b) < b.

2. Intuitionistically. One convenient way to treat the real numbers
intuitionistically is by equivalence classes of Cauchy sequences.

A Cauchy sequence is a sequence a1,a2,... of rationals such that there
exists a function f:N into N with the following property. For all n > 0 and
i,j > f(n), 

|ai - aj| < 1/n. 

The equivalence relation on Cauchy sequences is defined as follows. Let
a1,a2,... and b1,b2,... be Cauchy sequences. They are equivalent iff for all
n,m > 0 there exists i > m such that

|ai - bi| < 1/n. 

Everything in 1 works, provided "irrational" is defined properly. We say
that a real number is irrational iff for all representatives a1,a2,... there
exists a function f:N x Q into N such that the following holds. There exists
n > 0 and rational q such that for all i > f(n,q),

|q - ai| > 1/n.

Clearly there is a constructive procedure which, given an irrational real
number, produces the base 2 representation of that real number with the
following property. There exist arbitrarily large positions in the
representation that are 0's and arbitrarily large positions in the
representation that are 1's.

Furthermore, any such base 2 representation with that property corresponds
to a unique real number.

The base 2 representations takes on the form

a.b1b2b3b4...

where a is an integer (in base 2), the b's are 0's or 1's, and where there
are arbitrarily far out 0's and arbitrarily far out 1's.

There is a corresponding element of Z x N^N. The first term is a. The second
term is the length of the first run of 1's. If b1 = 0 then this length is 0.
The third term is the length of the second run of 1's. Etcetera.

Also, Z x N^N x Z x N^N is obviously homeomorphic to Z x N^N by mixing. This
works intuitionistically.

Again there is no problem intuitionistically constructing and verifying the
desired g.

Harvey Friedman