Re: Uncountable sets in CZF?

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

Date: 08 Sep 2004 06:48:45 GMT

In article <3c6b9c1e.0409071724.6b1f0716@posting.google.com>,
raf@tiki-lounge.com (Ross A. Finlayson) writes:
|kramsay@aol.com (KRamsay) wrote in message
|news:<20040907121638.22164.00000614@mb-m05.aol.com>...
|> In article <3c6b9c1e.0409030813.584832fe@posting.google.com>,
|> raf@tiki-lounge.com (Ross A. Finlayson) writes:
|> |Keith presented a statement that he could map a proper subset of the
|> |naturals bijectively to the reals. What's the deal with that?
|>
|> Do you think you're quoting me at all accurately here? You do agree
|> that you should attempt to, don't you?
|
|Yes, I think you claimed there was a surjection from some proper
|subset of N onto R, and through Cantor-Schroeder-Bernstein as there is
|a trivial surjection from R onto any subset of N there is a bijection.

Well I didn't, and it doesn't.

In <20040830045814.04815.00000438@mb-m17.aol.com> I wrote:
|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.

Do not quote people as claiming things that they expressly inform
you that they are not saying, just because you think the thing they
refused to say follows from what they did say. Even if the person is
simply confused, it's not accurate to describe them as having said
they agree with your conclusion.

There's no reason why you can't say in these cases, "X says that Y
holds. From Y, we can deduce Z, although X doesn't think so".

In this case, I specifically asked you not to try again to quote this
result without getting the details straight.

1. I didn't say these consequences of the assumption that each
function from N to N is computable were *true*. All I've ever said
is that it is *consistent with IZF* that they are true. There's a
big difference between claiming something is true and claiming that
it's consistent to assume it.

2. I didn't say it was consistent for there to be a bijection,
just a surjection from the subset of N.

3. Cantor-Bernstein doesn't say that if there are surjections from
A to B and from B to A, then there's a bijection between A and B.
It says it for injections. (Cantor-Bernstein isn't a theorem of IZF.
It doesn't require the axiom of choice, but it does require the law
of excluded middle, which we had to drop in order to work with the
assumption that each function from N to N is recursive.)

4. After a bit of searching, I found a paper on the web about the
dual Cantor-Bernstein theorem, which is the statement that if there
are surjections from A to B and from B to A, then there's a bijection
between A and B. This is the result you're trying to apply in the
context of IZF. It can't be proven without the axiom of choice, let
alone without using the law of excluded middle, so it's very far from
being a theorem of IZF. The assumption that each function from N to N
is computable is of course contradictory with it.

5. The existence of a surjection from R to Z isn't a theorem of IZF!
The existence of non-constant functions from R to Z isn't a theorem
of IZF! You probably are thinking of some function like the greatest
integer function [x] = max {n in Z: n<=x}. But this is only defined
for all reals if we are able to say that for each real x, either x<1
or x>=1 (and likewise x<n or x>=n for each integer n). That's not a
constructive result. If you are given a real number x, in the form of
a sequence of rational approximations, there's nothing to guarantee
that you can tell whether x<1 or not. (If x is not <1, then x>=1.)

|You say specifically that "it doesn't follow that there is a
|bijection." Yet, it necessarily does, until you present some disproof
|or negation of the Cantor-Schroeder-Bernstein theorem in that context.

No, even if you were right, you're not entitled to pretend I agree
with you until I show you what's wrong with it. It's up to you to
make sure that you're right, not up to other people to correct you
when you're mistaken.

|I don't base my arguments (that the reals and naturals are equivalent)
|upon what you said, I haven't seen your explanation of a surjection
|from some proper subset of the naturals to the reals,

I said it was a consequence, in IZF, of assuming that all functions
from N to N are computable. If each function from N to N is computable,
then each real is computable.

Each computable real can be represented by a machine that computes
a sequence of approximations to it. So the mapping from those integers
that represent machines that compute reals, to the reals that they
compute, is from a subset of the natural numbers onto the computable
reals. It's not one-to-one, because many different machines compute
the same real number.

Even when I'm thinking in constructive terms, I don't regard the
statement that each function from N to N is computable as a fact.
(And nonconstructively, it's false, of course.) It's just something
that can be consistently assumed, much like the continuum hypothesis.
In the Bishop tradition of constructive mathematics, such statements
are used to help us know what to try to prove, and what not to bother
trying to prove.

|and I have my
|own explanations for why the naturals can biject with some proper
|subset of the reals.

Well that they can do! But I think you mean the reverse, which is
a different story.

If there were a bijection between the reals and a subset of the
natural numbers, then equality between reals would be decidable,
i.e. either r=s or r<>s for each r and s. That's perfectly natural
for classical mathematics, following from the law of excluded middle,
but isn't appropriate constructively. Classically, then this bijection
is plainly impossible; constructively it's at least not appropriate.

|Apparently, so do you. I think that's good, and progress.

You're mistaken.

Keith Ramsay

P.S. Cantor's theorem is a fact of mathematics!

Relevant Pages

  • Re: Uncountable sets in CZF?
    ... an element of R not in the image is a theorem of IZF. ... It doesn't follow that there's a bijection. ... naturals to the reals. ...
    (sci.math)
  • Re: Zenkins paper on Cantor
    ... validate that EF is a bijection from N to R. ... different representation, then used to generate another, leads to the ... of the integers to reals if the mapping would lead to a contradiction. ... A bijection between the naturals and reals is not accepted by ...
    (comp.theory)
  • Re: Zenkins paper on Cantor
    ... validate that EF is a bijection from N to R. ... different representation, then used to generate another, leads to the ... of the integers to reals if the mapping would lead to a contradiction. ... A bijection between the naturals and reals is not accepted by ...
    (sci.math)
  • Re: Cantor Confusion
    ... >> So you can not show a bijection, ... Why isn't it sufficient to collect the shares of two edegs for every ... Paths can be bijected with the reals. ... Bis the set of all paths to which edge e belongs. ...
    (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)