Re: "Kantor dust"

[Toby Kenney <tkenney@mathstat.dal.ca>]

On Tue, 10 Feb 2009, Vaughan Pratt wrote:

> As a (surely constructive!) witness to the surjectivity, indeed
> bijectivity, of R,  define the inverse S: [0,oo) --> N^N  of R as
> follows.  (R converts sequences to Reals, which S turns back into
> Sequences.)
>
>   S(x)(0) = floor(x)
>   S(x)(n+1) = S(g(x mod 1))(n)
>
> where x mod 1 = x - floor(x) and g(x) = x/(1-x) : [0,1) --> [0,oo) is
> the inverse of f(x) = x/(1+x) : [0,oo) --> [0,1) used in the definition
> of R.
>

The trouble with this is that the floor function isn't constructive - the
question "is x<2" is undecidable in the reals, but decidable in the
natural numbers.

The problem with the obvious definition:
"Take the set of natural numbers below x, and take the join of this set."
is that the natural numbers don't have K~-finite joins, only K-finite
ones.

Incidentally, has anyone looked at semilattices with K~-finite joins? (Or
whatever your favourite notion of finiteness is.) Is there any use for
something like the completion of N under K~-finite joins, other than
allowing us to define the floor function?

Toby