[FOM] Intuitionists and excluded-middle

[Andrej Bauer]

Jesse Alama wrote:
>Can we find a proof that's about as constructive as this one using other
>representations of real numbers, say by Dedekind cuts?

We only need to know that reals form an archimedean ordered field, so
that rationals form a dense set, with at least one irrational number (a
number which is distinct from every rational). Observe that in this case
there is also a positive irrational number.

Proof 1 (abstract):
Let t be a positive irrational. Translation by t is an order-isomorphism
which maps rational numbers Q to the set t+Q of irrational numbers of
the form t+q, with q rational. Thus irrationals are dense as they
contain the dense set t+Q. The latter is dense because
order-isomorphisms map dense subsets to dense subsets. QED.

Proof 2 (concrete):
If x and y are reals such that x < y then there are rational numbers p
and q such that x < p < q < y (see [1] below). Between any two rationals
p < q there is an irrational, for example the convex combination t p +
(1-t) q where t is any irrational between 0 and 1, say t = 1/sqrt(2)
(see [2] below). QED.


[1] Because rationals are dense, if x < y then there is a rational x < s
< y. To see that there are two rationals between x and y, just take a
rational p between x and s, and a rational q between s and y.

[2] If there is an irrational number, then there is one between 0 and 1.
If p and q are distinct and rational and t is irrational then the convex
combination u = t p + (1-t) q is irrational, otherwise t = (u-q)/(p-q)
would be rational.

I hope these proofs are correct. I must be suffering from construvitis,
as I cannot see a much slicker classical proof using LEM, which Dana
Scott hinted at. Is the use of LEM in the supposed slick classical proof
essential or gratuitous?

Andrej Bauer

P.S. What is the best way to prove constructively that sqrt(2) is
distinct from every rational? The usual classical proof only shows that
sqrt(2) is _not_ rational? (Note that x is distinct from y
constructively if there is a rational in between.)