[FOM] Intuitionists and excluded-middle

[Neil Tennant]

On Wed, 19 Oct 2005, Jesse Alama wrote:

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

First, a and b differ in their expansions from the (k+1)-th place (since
y<u). Secondly, Lew Gordeew explicitly allowed the possibility that n
might be 0 (hence that there be no 9s).