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

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

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