Re: "Kantor dust"

[Greg Meredith <lgreg.meredith@biosimilarity.com>]

Categorically minded,

Many thanks for an interesting thread! Just out of curiousity, is the Conway
construction clearly identified with the Dedekind reals? How does the
construction fit into the constructivist debate?

Best wishes,

--greg

On Mon, Feb 9, 2009 at 2:47 PM, Prof. Peter Johnstone <
P.T.Johnstone@dpmms.cam.ac.uk> wrote:

> On Mon, 9 Feb 2009, Dusko Pavlovic wrote:
>
>  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.)
>>
>>  That's actually a quote from Toby Bartels, not from me.
> It's a statement about a topos built over the classical topos of sets;
> the argument is a rather ad hoc one, and I'm not sure to what extent
> it's possible to make it constructive. However, as I said elsewhere, I
> prefer to work with the gros topos of spaces (i.e. sheaves on a suitable
> full subcategory of spaces for the coverage consisting of jointly-
> surjective families of open inclusions) and there it's quite clear
> what you need: namely, Heine--Borel (equivalently, exponentiability
> of R in your category of spaces). That's not true in all toposes;
> you could try to get round it by basing your gros topos on locales
> rather than spaces (the locale of formal reals being constructively
> locally compact), but it's not clear (to me, at least) what the
> result would actually mean if you based yourself on a topos where
> the formal reals aren't spatial.
>
>  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?
>>
>>  I don't think there is any doubt that the map exists. The problem is
> that,
> for most if not all schools of constructivism, it's wildly non-surjective.
>
> Peter Johnstone
>
>
>
>


-- 
L.G. Meredith
Managing Partner
Biosimilarity LLC
806 55th St NE
Seattle, WA 98105

+1 206.650.3740

http://biosimilarity.blogspot.com