[FOM] Intuitionists and excluded-middle

[Lew Gordeew]

Jesse Alama wrote:
> 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?

We should not assume anything, as this block might be empty (by definition n
>= 0). Decimal expansions are not really necessary, either. It would suffice
to take any pair of rationals r, s such that
    r < a < s < b  and  s-r < b-a
and then let c:= a+s-r. This obviously yields the result. The proof can be
formalized in Constructive Analysis with Markov's principle, since x < u and
u < x are both decidable for any rational x and irrational u. Ergo LEM is
not required.

Regards,
LG

-- 
Highspeed-Freiheit. Bei GMX supergünstig, z.B. GMX DSL_Cityflat,
DSL-Flatrate für nur 4,99 Euro/Monat*  http://www.gmx.net/de/go/dsl