Five Stages of Accepting Constructive Mathematics - Andrej Bauer

Andrej Bauer
University of Ljubljana, Slovenia; Member, School of Mathematics
March 18, 2013
Discussions about constructive mathematics are usually derailed by philosophical opinions and meta-mathematics. But how does it actually feel to do constructive mathematics? A famous mathematician wrote that "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." Was he right? In this talk we shall visit the astounding worlds of constructive mathematics. As tourists from the classical world we will at first be shocked by the bizarre and unfamiliar phenomena, but hopefully also left curious about the new possibilities and dimensions of mathematics that the classical dogma declares heretical or even non-existent.
For more videos, visit video.ias.edu

[@jakecarlo9950]

You will be angry and depressed to learn that this presentation has won a philosopher to your cause. (You had me at “excluding the law of excluded middle.” ) I promise not to tell the other mathematicians if you promise never to be discouraged in your pursuits. Thank you for the work you’re doing.

[@j9dz2sf]

For once, I understand what a logician says! And it is very interesting!

[@foo_tube]

Why is it that the videographer spaces out/loses focus at at the precise moment when the main part of the proof is being elucidated. The professor is writing on a chalkboard offscreen, so unless you already know what he's saying, you are left behind. Then, it happens again later, but this time the chalkboard is illegible because the camera is too far away. Stuff like this is maddening to me and always seems to happen in math instruction.

[@Jooolse]

Very clear and interesting (Science4All brought me here)!

[@JernejBarbic]

Very insightful, even though I could not understand everything. [Also, good entertainment with the psychology.] What is clear to me is that the speaker is onto something fundamentally new. It's a new way of doing mathematics. Perhaps one day what is today "mainstream" mathematics, will become "classical", and constructive mathematics will be the new "proper" way of doing mathematics. Just like in physics, there is classical physics which was one day mainstream, and there is relativistic physics after Einstein. The fact that these ideas are already naturally embraced by other sciences (physics and CS), also tells me that there is something to this. I think we need to keep an open mind to such new ideas, as radical as they may seem.

[@lfossati80]

Like someone said, it takes time to build…

[@GeorgWilde]

Hi! How do i learn constructive topology without learning classical first?

[@Honortofinuka]

Much of modern scientific theory, in my case taxonomy, is crippled by excluded middle arguments. Axiomist versus constructutivists. See recent papesr of Grisin, Geneva, on plain old arithmatic and its limits.

[@annaclarafenyo8185]

Nonsense. Excluded middle is still okay for double-negated statements in intuitionistic logic. The theory is precise, it isn't a bunch of wishy washy nonsense.

[@Honortofinuka]

@@annaclarafenyo8185 Either split the universe of discourse into two such that there is no middle to exclude, or exclude an unconstructed middle.

[@annaclarafenyo8185]

@@Honortofinuka You don't understand any of these terms you are using.

[@Honortofinuka]

@@annaclarafenyo8185 Oh, I understand the terms I am using. I guess I don't understand the terms you are using. I'm coming from N. Gisin's take on constructivism as avoiding terms in maths, that are placeholders, that are not definable as real things.

[@tgenov]

​@@Honortofinuka Well, that's a really high bar.... Definability is not definable as a real thing. Impredicativity is a bottomless cave if "define" and "undefine" are seen as functions.

[@beback_]

So why are we rejecting the law of excluded middle again?

[@anti-hermes2541]

Why not? It's just a different paradigm, which may produce potentially insightful results.

[@annaclarafenyo8185]

It's not 'rejecting the law of excluded middle', that's a superficial way of understanding intuitionism. Intuitionism is a method of reformulating logical deduction so that it is a computer program, so that a proof turns into a witness of some sort of function or mathematical object. The law of excluded middle is still there in the Godel/Gentzen double-negation formulation, which says that if you consider instead of proposition A, proposition "not not A", then THIS double-negated thing obeys excluded middle. Classical logic is NOT a strengthening of intuitionistic logic, it is a weakening of intuitionistic logic by focusing only on doubly-negated statements. This is a very important step in the process of acceptance of intuitionism. The reason law-of-excluded middle needs to be pushed up is because when A or not A doesn't give you a function which proves either A or not A, rather it gives you a function which accepts a proof of A AND a proof of not A, and produces a contradiction (very easily). So considering the proof as a computable function (all proofs have a computable interpretation), it is a different type of function than a function which proves one of A or not A. This distinction is important regardless of any philosophy.

[@BosonCollider]

Because it allows you to handle more general propositions and predicates than the ones that are either true or false. Most of the propositions that show up in our daily life are neither obviously true or obviously false, so there is no reason why math should be treated differently.

[@annaclarafenyo8185]

@@BosonCollider That's not what intuitionistic logic is like. For the proposition in our daily life, for example, "too much salt contributes to diabetes", the double-negation "It is not true that too much salt does not contribute to diabetes" is uncertain in the exact same way. But in intuitionistic logic, the analog second statement DOES obey excluded middle, while the first does not. This is why classical logic is a truncation of intuitionistic logic, it's less information. Every classical statement should be viewed as shorthand for the double-negated intuitionistic statement, so that the law of excluded middle holds. The existence of double-negation embedding shows that intuitionistic logic is not weaker than classical logic, despite superficial appearances. It is just making more distinctions between the different types of proofs. These distinctions are real, and this is demonstrated by the easy conversion of intuitionistic logic into a computer programming language. Classical logic fails to be a computer programming language naturally, simply because it doesn't distinguish carefully enough between proofs of a statement and a proof of the double negation.