[FOM] Intuitionists and excluded-middle

[Jesse Alama]

Lew Gordeew <legor at gmx.de> writes:

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

This is a nice argument.  Two comments:

1.  The proof makes use of the representation of real numbers by
    decimal expansions.  Can we find a proof that's about as
    constructive as this one using other representations of real
    numbers, say by Dedekind cuts?

2. This proof might not go through for all representations of real
   numbers, especially an important one in this connection, namely
   representation by choice sequences.  You conclude from the
   assumption that a and b are irrational numbers between 0 and 1 that
   we can represent them as

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 the sequence of y_i's is the first (and longest) block of 9's in
the decimal expansion of a after which a and b "disagree" in their
decimal expansions.  Why should we assume that every irrational number
between 0 and 1 (or any irrational number for that matter), regarded
as a choice sequence, has such a block of 9's?

Jesse

-- 
Jesse Alama (alama at stanford.edu)