[FOM] Intuitionists and excluded-middle

[Jesse Alama]

Neil Tennant <neilt at mercutio.cohums.ohio-state.edu> writes:

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

That's true; I didn't want to imply that the proof would be
intuitionistically unacceptable because it implies that every decimal
expansion has a non-trivial block of 9's.  (Of course that's not even
classically acceptable, consider 0.1111... .)  I should have asked:
why are we entitled to believe that if two distinct irrational
numbers, regarded as choice sequences, disagree, then there is an
initial (possibly empty) subsequence where they agree, followed by a
block (possibly empty) of 9's, and so on?

I ask this only because I wonder whether Lew's proof goes through in a
theory of real numbers based on Brouwer's notion of choice sequence.
Does Lew's proof violate one of the basic features of choice sequences
as generated by an act of our free will?

For the Brouwer scholars: would Lew's proof be acceptable?

Jesse

-- 
Jesse Alama (alama at stanford.edu)