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

[no_identd]

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