Re: Uncountable sets in CZF?

From: KRamsay (kramsay_at_aol.com)
Date: 08/30/04 

Date: 30 Aug 2004 08:58:14 GMT

raf@tiki-lounge.com (Ross A. Finlayson) writes:
|Now we've seen in other threads that in IZF it is not inconsistent for
|there to be bijections between N and R. Is that not so?

No, Cantor's theorem that for any function from N to R there exists
an element of R not in the image is a theorem of IZF. Please just
think of this as a mathematical fact, won't you?

I've seen proofs that it's consistent with various constructive formal
systems to assume that each function from N to N is computable.
If I'm not mistaken the same sort of proof works for IZF.

Assuming that each function from N to N is computable has a
number of consequences that are liable to be unfamiliar. Since it's
contradictory with the law of excluded middle, you have to be ready
to work with intuitionist logic.

Here, though, the relevant consequence is that the function mapping
those Turing machines that compute real numbers to the real numbers
they compute would be a SURJECTION from a SUBSET of the natural
numbers to the real numbers. Please, now that we've gone through this
more than once, either don't try to quote the result, or remember these
key details. It doesn't follow that there's a bijection. I don't happen to
know whether it's consistent to assume there exists a bijection between
R and a subset of N. I suspect not, but I didn't succeed in working it
out.

But most especially, there can't be a surjection from the whole of the
naturals to the reals.

Keith Ramsay

Relevant Pages

  • Re: Uncountable sets in CZF?
    ... a trivial surjection from R onto any subset of N there is a bijection. ... I don't base my arguments (that the reals and naturals are equivalent) ... from some proper subset of the naturals to the reals, ...
    (sci.math)
  • Re: Uncountable sets in CZF?
    ... It doesn't follow that there's a bijection. ... > naturals to the reals. ... What that means is that one of the reasons that people call the reals ... That implies it is not a mathematical fact and to promote the other ...
    (sci.math)
  • Re: Uncountable sets in CZF?
    ... |a trivial surjection from R onto any subset of N there is a bijection. ... It doesn't follow that there's a bijection. ... is that it is *consistent with IZF* that they are true. ... for all reals if we are able to say that for each real x, ...
    (sci.math)
  • Re: Zenkins paper on Cantor (reply of Dr. Zenkin)
    ... What is "a function which is a bijection"? ... exists another function (algorithm), f^-1, with the property for all b ... well-defined (exists for all naturals n, m) and S is a bijection - ... of reals, S". ...
    (sci.math)
  • Re: Cardinality of Real Numbers
    ... Cantor's first assumes the existance of a bijection between the ... >> natural numbers and the reals. ... From this, a contradiction is reached ... >naturals to the reals, and shows that there is some real not in the ...
    (sci.math)