Re: "Kantor dust"

[Dusko Pavlovic <Dusko.Pavlovic@comlab.ox.ac.uk>]

hi.

i missed most of this thread, but even this one message that i did catch
raises several questions that i would like to share.

QUESTION 1: re peter johnstone's

>>>  In the topos of sheaves on the real line,
>>>  every function from [0,1) to N is constant,
>>>  yet there are obviously many other functions from N^N to N.
>>>  Thus N^N and [0,1) are not constructively isomorphic as sets,
>>>  so there is no way to give N^N the order type of [0,1) constructively.

are you claiming that this statement is true with respect to every base
topos and every real line in it? (the discussion seems to have touched
upon the various constructions of the various real lines. it would be nice
to know where is the one, over which you build the topos, is coming from.)

QUESTION 2: is there a branch of constructivism that would reject as
non-constructive the map N^N-->[0,1) obtained by interpreting the N^N as
the coefficients of continued fractions?

COMMENT: IF the answer to either of the above questions is NO, then
maybe the tacit

   SLOGAN that "constructively valid" = "true in every topos"

needs to be taken *very carefully*. when we build toposes over classical
universes, then we may be able to force away more than any constructivist
would ever reject. the strict constructivist logics have already been
marginalized as too restrictive; lets not completely bury them just for
the joy of constructing counterexamples.

moreover, EVEN IF the answer to both of the above questions is YES, the
above SLOGAN still does not tell the whole story, IMHO.

the constructivists wanted to make our computations effective. that goal
led to some great philosophical debates in the first half of XX century.

later people built computers and paid lots of programmers to make
computations effective. besides brouwer, and heyting and kolmogorov, maybe
we should admit that people like gosper, and knuth, and dijkstra, and our
own vaughan pratt, also have an idea about what is effectively computable.

peter johnstone points out that the comparison test for the binary reals
(i presume the reals in base 2; there are many other representations, of
course) is undecidable. this actually applies to every base, and even to
the continued fraction representation (because it is irredundant). but in
the practice of effective computations, this is no showstopper. there are
many things that need to be computed with the reals, and no one
representation fits for all purposes. so the statement

> nobody uses the binary reals

probably has more counterexamples than, say, the statement "nobody
uses toposes". even if "the" binary reals were completely wrong.

the study of the various effective algebraic operations on the reals,
always reduced to one binary form or another, goes back at least to gosper
and schroepel, the original "hackers" from the 70s. they were, of course,
aware that the comparison test was undecidable. buyt people prefer to run
a program that may not terminate, or will terminate fast, over a program
guaranteed to terminate between tomorrow and 2 years from now.

gosper's continued fraction representation was improved by jean
vuillemin, who proposed in 1990s a redundant representation, where the
comparison test is decidable. this is what at least some people have
really been using in their real projects, sensitive enough to bring
the chaotic effects of the floating point arithmetic to the surface.

it would be interesting to understand whether the notion of computability
as embodied in toposes is related in some rational way with the notion of
computability as embodied in computers.

-- dusko