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.

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.

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.

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.

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.

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"...

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

>Though choice is more commonly used in an alternate form such as Zorn's lemma

Speaking of choice & constructivism, did you know that there exists a constructive version of the axiom of choice? See here:

http://web.archive.org/web/20170222112602/http://www.jonmste...

[Historical side note of somewhat fleeting importance on something which, besides me, nobody so far seems to have really noticed:

It seems that van Heijenoort 'overtranslated' Hilbert's infamous boxing gloves paragraph. Here's the original German, from Die Grundlagen der Mathematik, Abhandlungen aus dem mathematischen Seminar der Hamburgischen Universität 6 (1928), 65-85:

"Dieses Tertium non datur dem Mathematiker zu nehmen, wäre etwa, wie wenn man dem Astronomen das Fernrohr oder dem Boxer den Gebrauch der Fäuste untersagen wollte."

Here, van Heijenoort's translation:

"Taking the principle of excluded middle from the mathematician would be the same, say, as proscribing the telescope to the astronomer or to the boxer the use of his fists."

Here, a more literal translation:

"To take this Tertium non datur from the mathematician, would be about how when would want to proscribe the Astronomer the telescope or the boxer the usage of the fists."

Now, the point of this doesn't consist of the sentence now sounding rather different (and somewhat badly phrased) - in fact, that seems rather typical of intentionally more literal translations, as usually, translation also involves fitting the translated version of the text into the common use of the target language. No, the point consists of the fact that van Heijenoort should have left the latin expression "Tertium non datur" in place, see the following reddit comments thread about TND 🆚 LEM for why:

https://www.reddit.com/r/dependent_types/comments/33tc28/jon... ]

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.

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."

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

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.

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.

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

Presumably drvd is referring to the independence of the Continuum Hypothesis: we don't know |R| in the sense that we don't know for which ordinal alpha is |R| the alpha'th infinite cardinal. The Continuum Hypothesis is the claim that |R| is the first cardinal after |N|. It's well known the Continuum Hypothesis is independent of ZFC. That means for the question of "how many reals there are" (at least if that question is read in the formal sense), the answer is "it depends: for different models of ZFC, there are different answers".

What is the cardinality of the powerset of the naturals?

It's usually referred to as "c". I'm not sure what you're asking? It's like saying "3 is the number that follows 2", and then asking "yeah, but what really IS the number 3, man?". The answer is: it's the cardinality of the sets which can be in a bijection with the power set of the natural numbers.

If you're referring to the continuum hypothesis, that is a distinct question from "what is the cardinality of the real numbers". Also: a solved one, the contiuum hypothesis is independent of ZFC, so saying "we don't even know what the cardinality is" is still wrong.

This is an extremely unusual conception of epistemology, even for mathematics. This knowledge that is contingent on axioms isn't at all convincing. At the beginning of the 20th century, this was a raging debate. It wasn't quite resolved, it just didn't quite matter to practicing mathematicians so it kind of faded into the background.

There is a massive gap between 3 and the cardinality of the continuum. 3 is directly examinable. If I count some collection of objects, my fingers say, I will immediately grasp 3.

On the other hand, the set of real numbers is a highly pathological, abstract concept. Everything we know about the reals suffers from two severe deficiencies: One, it depends on infinitary axioms which presuppose facts about the phenomenon we would like to investigate. Two, even what we can infer from such axioms is always indirect evidence. That's not surprising: All reasoning about infinity is indirect.

In certain mathematical settings it is even true that the Cauchy sequence definition of real numbers and the Dedekind cut definition do not agree. At the very least, the reals isn't even a thing: there are many reals. That you say that "we know the cardinality of the reals" because we know CH is independent of ZFC is... preposterous to say the least. "If you assume you know the cardinality of the reals, then you know the cardinality of the reals; therefore we know the cardinality of the reals" is basically what such axiomatic acrobatics boils down to. Axioms are not knowledge.

Here, another interesting construction of the real numbers:

https://arxiv.org/abs/math/0405454 - The Eudoxus Real Numbers

https://ncatlab.org/nlab/show/Eudoxus+real+number

https://en.wikipedia.org/wiki/Construction_of_the_real_numbe...

(Surprisingly enough, ncat & Wikipedia complement each other here in their explanations of it.)

Getting back to the OP: in a very real sense, the set of Real numbers does not exist. Therefore, it is impossible to know its size via experience. The only possible way is to derive it from chosen axioms.

Note that even your conception of 3 is reliant on axioms. How do you "know" that 3 ducks is the same 3 as 3 fingers? Only via axioms.

That's sounds a little absurd. A five year old child knows that 3 fingers is the same 3 as 3 ducks. Certainly 5000 years ago people understood 3 without ever knowing what an axiom is. The peano axioms didn't create arithmetic, arithmetic created the peano axioms. S(S(S(0))) follows | | |, not the other way around.

The cardinality of the continuum is a cardinal number. It’s one of the alephs. It is not known which aleph it is. So it’s not known what the cardinality of the powerset of the naturals is. It’s just known that it is the same cardinal number of the reals. Basically, we have two jars of marbles that contain the same number of marbles but it’s not known how many marbles that is.

The continuum hypothesis being independent just means that it's an additional rule you can add or remove from the game you are trying to play. It doesn't mean we are lacking in knowledge and that if we were to work harder we would solve this problem. We do know which aleph c is: it's aleph_1 with CH and some other aleph without CH. Just take your pick which version you like better.

It's not like we don't know which one is the true model of military combat: chess or checkers. They're just two different games with two different rule sets, and you get to pick which one you like to play more.

The set theory that most working mathematicians deal with is ZFC. In ZFC it is not known what cardinal the continuum is. Hence the statement that I was responding to is incorrect. The person I responded to said that they do know how many reals there are.

The cardinality of the reals is called c. It is known to the be the same as the cardinality of the power set of the naturals. It is not known, in ZFC, which aleph this is. We just know that it is the same as the size of another set.

If you want to add an axiom and say that c is aleph1 then you are free to do so. But if you don't have this axiom then you don't know which aleph it is. So in what sense can you say that you know how many reals there are? You only know it if you add an axiom that says, "It is aleph1."

If I have a jar of pennies and I know it has the same number of pennies as the number of quarters in another jar that I have, does this mean I know how many pennies are in the jar?

Exactly right.

I think the issue is with the implicit claim that we don't "know" a cardinal until we know which aleph it corresponds to.

> What is the cardinality of the powerset of the naturals?

That question is better than almost every other question!