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