Wonderfully accessible synopsis. One ever so _minor_ point. Did you really mean to say "The former and the latter are not the same thing" or "The former and the latter are not _formally_ the same thing" ???

Here's a fun fact for you, you might enjoy this. I picked up a copy of a 1943, second edition, hardback copy of Bertrand Russell's An Inquiry into Meaning and Truth. (In an antiquarian bookstore for €25, as one does... the colophon even states BOOK PRODUCTION WAR ECONOMY STANDARD)

Anyway, chapter XX is titled "The Law of The Excluded Middle" and in it Russell states, "[…] As everyone knows, Brouwer has challenged the law, and has done so on epistemological grounds. He, in common with many others, holds that “truth” can only be defined in terms of “verifiability”, which is obviously a concept belonging to the theory of knowledge. If he is right, it follows that the law of the excluded middle, and the law of contradiction also, belong to epistemology, and must be reconsidered in the light of whatever definition of truth and falsehood epistemology permits."

What strikes me about this (apart from the fact that I did not know previously that Russell tackled the question of constructivism/intuitionism so directly) is that he claims that everyone! knows this. If we are being charitable by everyone he means mathematicians, and perhaps logicians, maybe even philosophers, I still think it's quite a broad statement. It shows that the school of the logical positivists springs from Brouwer -- which firstly I was never taught, and which secondly does not appear in, for instance, Language, Truth, and Logic[1] by A.J. Ayer. Finally I can see how the law of double negation becomes an epistemological matter, but not the law of what he calls here contradiction (noncontradiction?).

He goes on to disprove the verifiability claim over many pages, and thus constructivism. There's a swipe at Wittgenstein further on still. It's a fascinating text. Russell grapples with mathematical and logical issues in a clear fashion using everyday language. Kind of like what you might get if you took the intro to HoTT and lengthened it and made it more philosophical.

[1] https://archive.org/stream/AlfredAyer/LanguageTruthAndLogic_...

ps: is there markup for blockquote on HN?

EDIT: clarity, markup, prose style