I apologize for interrupting a productive flow of thought. But I was curious what you guys were talking about. Seems pretty esoteric. — jgill
I can summarize. Short answer is that these days you can do logic via category theory; and when you do that, you get intuitionist logic (denial of the law of the excluded middle (LEM) and all that) in a natural way.
This relates to topology via the idea of fiber bundles from differential geometry if you know what those are. If not just ask). The examples presented so far aren't clear to me and I haven't worked through
@fdrake's promising-looking examples.
@Mephist may or may not have presented coherent examples but there's a gap between his expositions and my understanding that only gets worse over time. The fault may all be mine.
There's a very nice illustration of how this works if you consider any topological space and restrict your attention to the open sets. The "complement" of an open set in a topology, if you only care about open sets, is the interior of the complement of the set. (In other words in general the complement is not an open set, but if we only look at the open sets, it makes sense to define funny complements this way).
So it is in general NOT true that the complement of the (true) complement of an open set is going to give you back the original open set. This corresponds to a failure of the law of the excluded middle.
For a very nice overview of the history and meaning of all this I recommend the prologue of Mac Lane's
Sheaves in Geometry and Logic. One need not understand the details to get the big picture from this very clearly written book.
Intuitionism was developed in the 1930's but didn't get any mindshare in mainstream math. Now with the advent of computers (where the complement of a noncomputable set of natural numbers may also be noncomputable), denial of LEM is back in fashion, especially in computer science and categorical logic. I call this Brouwer's revenge.
Brouwer invented intuitionism in the old days but it didn't catch on. His form of intuitionism had a touch of mysticism to it, but the modern versions are mathematically solid. Fifty years from now (or sooner) they'll be teaching this to undergrads and set theory will be a relic of the past like Euclidean geometry. Set theory of course won't become wrong, just out of fashion.
Another thread of development is that mathematicians want to use computers to check their proofs for accuracy. It turns out that intuitionist type theory (which I know nothing about) is the key. In
homotopy type theory one uses the idea of homotopy from topology (continuously deforming one path into another) to do intuitionist logic in such a way that you can build working computerized proof assistance for professional mathematicians. Also see
intuitionistic type theory.
These are the broad outlines I've picked up, but I haven't spent much if any time on the details. One name you'll hear a lot is
Vladimir Voevodsky, a Fields medal winning mathematician who became frustrated at longstanding errors in published proofs and devoted himself to the project of computerized proof assistants. He died tragically young just recently, in 2017.
Voevodsky's contribution is the Univalent foundations of mathematics. The idea here is that mathematicians routinely conflate equality and equivalence whenever it's convenient. For example there's only one cyclic group of order four, even though there are lots of isomorphic copies of it that are not equal as sets. For example the integers mod 4 and the powers of the imaginary unit
are the "same" group.
I should mention that this kind of thing bothers
@Metaphysician Undercover greatly, and he's right that mathematical equality can sometimes be stretched past what he would consider true equality. The answer to this is that if it quacks like a duck it's a duck, and if it's isomorphic to the cyclic group of order four, it doesn't matter what representation we choose. They're all the "same" in the appropriate technical sense.
In category theory this conflating of equality and equivalence becomes semi-formalized via universal properties. Any two objects that satisfy the same universal property are isomorphic and are regarded as the same thing.
Univalent foundations takes this one step farther by formalizing an axiom that says that equivalent things are equal. My high-level understanding is that the univalence axiom makes mathematically precise the informal practice mathematicians have been accustomed to for decades.
https://en.wikipedia.org/wiki/Univalent_foundations
All of what I've written is of course hopelessly vague and should not be relied on as gospel. But I've hit most of the buzzwords and major concepts in their broad outlines.
ps -- The immediate subject of the thread recently is to see how we can view intuitionist logic as an example of a fiber bundle. Maybe that was the short answer to the question.