[btilly]

You overstate "knowledge".

We project back currently accepted axioms, and find that Cantor's proof works. And therefore it was known, because the proof was known.

However Cantor's proof is not so cut and dry, nor was it so unarguable at the time.

It was based on set theory, and it was not clear to people at the time that set theory actually worked. Indeed, in 1901 Bertrand Russell came up with "the set of all sets that do not contain themselves" and came to a contradiction.

One of the proposed resolutions was to find a better set of axioms, which lead us to ZF and later to ZFC. This is the path that mathematics took.

Another was to question what words like "exists" and "truth" mean. In particular, does it make sense to talk about the existence of something we cannot construct? To talk about the truth of a statement that we have neither proof nor disproof of? This path leads to constructivism, and in constructivism Cantor's "proof" isn't a proof at all!

As it turns out, there are philosophical reasons to prefer constructivism, but mathematics is easier to do within formalism. After mathematicians gained enough experience with and trust for ZF, they went with convenience. But there are plenty of mathematicians historically, and even a few remaining today, who think that the entire tower of cardinalities from classical set theory is formal nonsense meaning nothing. And there is no logical flaw in their views.

[xamuel]

Cantor's proofs (he gave multiple) are un-controversial. There's absolutely zero question about them from any reputable mathematician.

One COULD take issue with the wording: what Cantor demonstrated is that there is no injection from the reals to the naturals (i.e., no way to assign a natural number to every real with no repeats). Anyone who disputes this is a quack. The layman controversy comes from our choice to describe this situation in English as, "There are more reals than naturals". That's merely a shorthand for the more precise statement. People get bent out of shape because they mistake the shorthand itself as some deep philosophical claim, rather than looking at what it actually means.

[btilly]

You overstate your case.

The proof that there is a bijection between the reals and the power set of the natural numbers depends on Cantor's bijection theorem. As you can verify from https://en.wikipedia.org/wiki/Constructivism_(mathematics) or many other sources, that proof and theorem has been rejected by many reputable mathematicians over time. Most notably including Brouwer.

[xamuel]

Constructivism is subtler than that (the wikipedia intro is misleading).

When an intuitionist says that we can't use the principle of excluded middle, they mean it more like in a functional programming sense: if we have two recipes for a cake, one of which requires a proof of X, and one of which requires a disproof of X, we cannot combine those recipes with a proof of "X or not X" and bake a cake.

Intuitionists noticed that (in a sense that can be formalized), if you do mathematics while "pretending" that the law of excluded middle is doubtful, then all your proofs become constructive. There is a misconception among laymen, who see these mathematicians who are so pretending for a pragmatic purpose, and mistakenly think these mathematicians are so pretending out of philosophical principles. That's never or almost never the case.

I can't speak for Brouwer's "religious" beliefs but what I can say is: if he attempted to teach students "It isn't always true that (P or not P)", without appropriate disclaimers that by saying that he's actually saying something very subtle and precise--then his math department would be obligated to stop him from misleading those students.

[btilly]

I have no idea what your background is, but my understanding is exactly opposite of yours. You are shoehorning people who think something very different from what you think into the framework of how you think people should think about it.

The first "pure existence proof" by contradiction was due to David Hilbert in 1888. The now-named Hilbert Basis Theorem resolved a famous problem introduced by Paul Gordan. Paul Gordan's famous response was, "Das ist nicht Mathematik. Das ist Theologie." (That is not Mathematics. That is Theology.)

In the debates that followed in subsequent decades, the question was whether or not we could sensibly talk about the existence of something we have no way to find or verify. Brouwer wasn't just making a subtle point in the 1920s that is palatable to modern mathematicians. He was rejecting the symbol game that was Hilbert's Formalism as meaningless nonsense.

Brouwer's school lost. So it is true that any Constructivist today does have to present a weakened form in public that fits your description. But historically they meant exactly what they said. And what they said is that proving that there is an unfindable contradiction in an infinite set is not an acceptable proof of existence. And what they believed was that allowing such unsound reasoning methods would lead to contradictions. (This belief has since been disproven, but in the 1920s nobody can be faulted for having been genuinely concerned about it.)

To gain a better understanding of the times, I would recommend two books. The first is Hilbert! by Constance Reid. It is a biography of David Hilbert, and does a surprisingly good job of describing the fundamental epistemological issues that lead him to Formalism. The other is The Mathematical Experience by Davis and Hersch.

[xamuel]

I'm not a math historian, so I'll take your word for it about the math history. I should have qualified that my statements apply to contemporary mathematics.

Paradox: Cantor's theorem is uncontroversial in mathematics. But the controversialness of Cantor's theorem is uncontroversial in history of mathematics. :)

I, for one, am glad Brouwer's school was defeated: I wouldn't want to choose a mathematical denomination like people choose their church denomination.

EDIT: Thinking about it deeper, it does make me wonder if we haven't all already chosen a mathematics denomination, and just not realized it. It's fun to imagine an alternate reality where Brouwer won and Hilbertists are forced to couch their theorems with elaborate contortions about "when I say X exists I really mean that a Hilbert-style proof that X exists exists"...

[btilly]

We have indeed all already chosen a mathematics denomination. And people like me who don't think that it makes actual sense to talk about the "existence" of things that cannot be in any useful way described have lost.

That said it is worth understanding very clearly, no matter what your preferences, that the deciding factors in any debate between the two sides did NOT center on logic. Logically both positions are internally consistent. In the end it comes down to asking whether or not you wish mathematics to be convenient, or about something real. Convenience won.

Which is the same reason that ZFC beat out ZF. (Though choice is more commonly used in an alternate form such as Zorn's lemma.)

[thraway180306]

I noticed you consistently misspell Reuben Hersh's surname. Sorry I haven't corrected you when I first saw you doing that on HN close to a decade ago, assuming you might soon self-correct if only by glancing over the book you hold so dear.

As for the book by Constance Reid, Gian-Carlo Rota's review entitled Misreading the History of Mathematics is all that should be said of it.

[leephillips]

I second the recommendation of Reid's biography (although the title does not have an exclamation point): great book about a truly great man. Eventually Gordan came around, to some extent, and said that maybe "even theology has its uses."

[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).