[FOM] Intuitionists and excluded-middle

[Hendrik Boom]

On Sun, Oct 16, 2005 at 11:42:15AM -0700, 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?

Take the rational c that Paul Halmos provides us between a and b.
Then (c+b)/2 is irrational, and between a and b.

-- hendrik