Re: Cauchy completeness of Cauchy reals

[Dusko Pavlovic <dusko@kestrel.edu>]

(not sure whether i shouldn't let this thread die, since i didn't read
mail for a week, and we all have things to do. but it's not like this
list is filling anyone's mailbox with megabytes of usolicited research
problems, and it seems a couple more dekabytes on cauchy reals might be
useful.)

Alex Simpson wrote:

>>      |cb(x)i - cb(y)i| <= [... calculation omitted ...]
>>                       <=   1/2^i
>>
>>means that cb(x)i and cb(y)i have the first i digits equal.
>>
>I don't see that cb(x)i and cb(y)i have the first i digits equal.
>
i stand corrected (as they say).

>>now, as everyone has been pointing out, the dyadic representation
>>depends on markov's principle.
>>
>
>This is *not* what has been pointed out (whatever you mean
>by dyadic representation).
>
>What I previously pointed out was that the existence of
>ordinary binary representations may fail even in the presence
>of Markov's principle.
>
dyadic numbers are rationals in the form p/2^n. (google helps with such
things.)

the intuition that dyadic approximation has to do with markov's
principle is supported by the fact that markov's principle is equivalent
with the statement

>>that 1/2 + 1/4 +...+ 1/2^k > 1-e. in other words, that there is k
>>s.t. 1/2^k < e. this is *equivalent* to markov's principle.
>>
>
>The property quoted is in fact a trivial consequence of intuitionistic
>arithmetic alone. It has nothing to do with Markov's principle.
>
for a real number e, i am pretty sure that the above is equivalent with
markov's principle. it must be in books, but i think you can't miss the
proof if you try.

*however* you are right that in my "construction", it is used in a wrong
place, for a rational number, and k exists trivially.

>Such an f is tantamount to giving a splitting to the epi
>
>  r: {x: Q^N | x a Cauchy sequence} --> I_C
>
>where I_C is the Cauchy interval. There are many toposes
>in which Q^N is basically Baire space and I_C is basically
>the closed unit interval in Euclidean space
>Furthermore,
>in many such toposes (e.g. Johnstone's), countable
>choice and Markov's principle both hold.
>
splitting r is only the strongest sense of finding the canonical
representatives, not the only one. r may not split by a topos morphism,
but the canonical representatives can be found externally, and suffice
for a completeness proof.

after all, if i remember correctly, such is the situation with markov's
principle itself: for a decidable P,

* heyting arithmetic does not validate |- ~forall x. P(x) -> exists x.~ P(x)
* but if |-~foral x. P(x) can be derived, then |- exists x.~P(x) can be
derived.

in particular, if i can prove that not all numbers in a binary stream
are 0, then i can extract the first 1 from that proof, although that
proof transformation cannot be internalized as a recursive function, to
realize the implication.

all this is, of course, just more intuitive support for the idea that i
have been trying out, that *dyadic approximations might yield
representatives of cauchy sequences, and since they are a coalgebra,
help with their completeness*. i know that it is probably a wrong idea,
but it also feels wrong to me to settle with incomplete cauchy reals.
i'd like to understand why in the world would toposes deviate from
cantor's idea of continuum, so pervasive in everyday math?

-- dusko