[FOM] Intuitionists and excluded-middle

[Lew Gordeew]

Dana Scott wrote: 
> Here is another puzzle asking for a very quick proof using LEM (first
> pointed out to me by Paul Halmos): From the construction of the reals
> we know that between any two irrationals there is a rational.  Show that
> there is also an irrational.  (Hint:  If the irrationals are a < b, then
> the average (a+b)/2 is a bad answer because it might be rational.)
> Second question: What is a more constructive proof?

PROOF. Without loss of generality suppose 0 < a < b < 1. Consider decimal
expansions:

a = (0.)x_1,...,x_k,y,y_1,...,y_n,z,z_1,z_2,...
b = (0.)x_1,...,x_k,u,u_1,u_2,...

where y < u , y_1 =...= y_n = 9 and z < 9 (k, n >= 0).

Let c:= (0.)x_1,...,x_k,y,y_1,...,y_n,z+1,z_1,z_2,...

Clearly a < c < b. Moreover c is irrational, since so is a.
Q.E.D.

This proof is very quick and fairly constructive. 

Regards,
LG

-- 
Lust, ein paar Euro nebenbei zu verdienen? Ohne Kosten, ohne Risiko!
Satte Provisionen für GMX Partner: http://www.gmx.net/de/go/partner