[chriswarbo]

> in constructivism Cantor's "proof" isn't a proof at all!

Are you sure about that, and could you point me to a reference if so? It was my understanding that Cantor's proof works perfectly well in a constructive setting.

For example, we can represent real numbers in a constructive way as functions from a natural number to a digit, where we interpret f(N) as giving us the Nth decimal place. We can represent an infinite list in the same way: taking a natural number and giving the value at that list position (a real number is hence an infinite list of digits).

Hence we can construct a function F which takes in a list of real numbers (a function mapping natural numbers to functions-mapping-natural-numbers-to-digits) and gives out a real number (a function mapping natural numbers to digits). Given a number N, this function looks up the Nth digit of the Nth number in the list, and returns a different digit (e.g. one more, modulo 10). Formally, in some Agda-like notation, it would be something like:

    Digit = Member of {0, 1, 2, 3, 4, 5, 6, 7, 8, 9}

    inc : Digit -> Digit
    inc(0) = 1
    ...
    inc(9) = 0

    List(t) = Natural -> t

    Real = List(Digit)
    Real = Natural -> Digit

    F : List(Real) -> Real
    F : (Natural -> Real) -> Real
    F : (Natural -> (Natural -> Digit)) -> (Natural -> Digit)

    F(list)(n) = inc(list(n)(n))

Cantor's proof is then a function which takes a list L and returns a proof that F(L) doesn't occur in L. We can represent non-occurrence using a function taking a natural number N and returning a proof that the Nth element of L differs from F(L) (this is a list of proofs!). We can represent proofs that two numbers differ by using a natural number, which gives (one of) the decimal places at which those numbers have different digits. We know from the definition of F that F(L) will differ from the Nth value in the list, and more specifically that it will differ at the Nth decimal place. It's easy to prove that distinct digits are different, since the set of digits is finite (although the exact encoding depends on the logical system being used). Hence we just need to show that `inc(N) != N`, and use that as proof that `F(L)(N) != L(N)(N)`, and hence `F(L)` doesn't occur in `L`:

    -- Proof that x != y, however you want to represent that (e.g. 'Equal x y -> Empty')
    Differ(t) : (x : t) -> (y : t) -> Set of proofs that x != y

    incDiffers : (d : Digit) -> Differ(Digit)(d, inc(d))
    incDiffers(0) = 0 != 1
    ...
    incDiffers(9) = 9 != 0

    -- Proof that two reals differ, which is a natural and a proof that they differ
    -- at that digit
    RealsDiffer(x, y) = {n : Natural | Differ(Digit)(x(n), y(n))}

    -- Proof that F(L) differs from everything in L. This is because the Nth element of L
    -- differs from F(L) at (at least) the Nth decimal place.
    cantor : (L : List(Real)) -> (n : Natural) -> RealsDiffer(L(n), F(L))
    cantor(L)(n) = (n, incDiffers(L(n)(n)))

[btilly]

The diagonalization argument is constructive, but with an asterisk. However the classic understanding of cardinality also requires Cantor's bijection theorem. If there is a one-to-one function from A into B and from B into A, then there is a bijection between them. This proof is non-constructive. And without it, the entire tower of cardinalities falls apart.

The asterisk with the diagonalization argument can be seen best with an example. Suppose that we define "reals" as programs which have been proven to construct Cauchy sequences that converge at a given rate from some set of axioms. Suppose that we construct a program that will enumerate all possible proofs from that set of axioms. This is doable. We search those proofs for proofs of statements of the form "this computer program computes a Cauchy sequence". That gives us a purported listing of all possible real numbers according to this definition. (Any given real will show up many times.)

Now apply Cantor's proof. It can construct a program which we believe produces a Cauchy sequence which converts at the given rate which is not in the list of all possible real numbers. The construction is concrete and we can write down the resulting program with only modest difficulty. BUT is the program that we found a real number under the definition that we chose?

It cannot be if the set of axioms is consistent. Because if there was a proof that it was, then it would be on the list and we'd be looking for a number that we don't want. Indeed, a proof that it actually produces a Cauchy sequence would follow immediately from the assertion that the axiom system we were using is consistent. But Gödel's theorem says that the axiom system, if it is consistent, can't ever prove that. The program that we have produced is some sort of "meta-real" - but it is not a "real" by the definition chosen since there is no proof from the chosen axiom system that it actually produces a Cauchy sequence.

And now Cantor's argument is not showing up as "there are more reals than integers". It is showing up as some sort of, "Our definition of reals is complex and recurses in on itself in a way that tangles up the division between true, false, and unknown."

See https://mathoverflow.net/questions/30643/are-real-numbers-co... for more variations on the complexity of constructivism and Cantor's diagonalization argument.

[jwatte]

I don't think this construction works, for the same reason that rationals are lower cardinality than reals. I e, I think your program proves the rationals, not the reals.

[chriswarbo]

They would be rationals if the "lists" were finite (i.e. if their input were finite, like "natural numbers less than 100"). Infinite lists of digits (i.e. where the input can be any natural number) are reals.

One subtlety is that we're talking about arbitrary functions, e.g. they aren't necessarily computable, or even representable (e.g. as programs, or otherwise).