Mathematics and Computation

A blog about mathematics for computers

Five stages of accepting constructive mathematics

In 2013 I gave a talk about constructive mathematics “Five stages of accepting constructive mathematics” (video) at the Institute for Advanced Study. I turned the talk into a paper, polished it up a bit, added things here and there, and finally it has now been published in the Bulletin of the American Mathematical Society. It is not quite a survey paper, but it is not very technical either. I hope you will enjoy reading it.

Free access to the paper:  Five stages of accepting constructive mathematics (PDF)


Mike Shulman

Nice! However, it seems a little contradictory to present sheaves as a model of "constructive mathematics" but also consider a proof using dependent choice to be "constructive".

Paul Fabel

Great paper! Great talk! But I am in stage confusion.

I think I understand the proof of Theorem 1.3 using classical reasoning, but am wondering where the proof of Theorem 1.3 fails to establish LEM in constructive mathematics.

In particular the proof of Theorem 1.3 ( that AC=>LEM) seems to use only a very weak, (and constructively accepted?) form of AC, namely that if we have precisely one or two distinct inhabited subsets of {0,1}, then we may pick an element from each one.

Are the sets A and B `constructively well defined'?

Is the problem that we have' two sets A and B but don't know' if A=B?

You are mistaken about the form of AC needed in the proof of Theorem 1.3. The proof is constructive, of course! And it is not the case that we have "precisely one or two distinct inhabited subsets of ${0,1}$" because for that to be true you would need to know "$A = B$ or $A \neq B$", which would immediately decide $P$. The set ${A, B}$ is one of those funny sets which cannot be shown to be finite.

And what is this idea that a set can be "defined" but not "constructively defined"? The language of set theory and first-order logic is identical in classical and constructive mathematics.

Well, it is only contradictory if you assume that there is just one world of constructive mathematics, or if you presuppose that everything I say in the paper fits into a single world of mathematics. As I specifically speak about three differrent worlds in the Bargaining stage, I would hope it's not such a big problem if later on I do things which are not universally true everywhere. So I think it boils down to warning the reader that dependent choice is not valid in every world, and I decided this was not really necessary at that point.


The paper is very readable and very interesting. But I didn't understand the example on p. 8, of the non-finiteness of subsets of {0, 1}. Are the subsets decidable in your constructive world? If so, what if I represent the subset input as a computation from {0,1} -> {TRUE, FALSE} and test if 0 and/or 1 are present in the subset? If the input programs -- even those denoting decidable sets -- are allowed not to terminate and yet the realizing program must always terminate, then how are any "for all" propositions realized? You write, “In computable mathematics a finite set is represented by a finite list of its elements, and a countable set by a program which enumerates its elements, possibly with repetitions.” Shouldn’t there be a third option: decidable countable subsets of a countable (or finite) set S, are realized by a program S -> {TRUE, FALSE} ?

The subsets are not presumed to be decidable. And you can't just say things like "what if I represent the subset input as a computation from {0,1} -> {TRUE, FALSE} and test if 0 and/or 1 are present in the subset" without first properly setting up an interpretation of logic and set theory (or whatever formalism you have in mind) under which it is even possible to represent subsets as computations. You would probably need to use something like realizaiblity. However, note that general subsets cannot be represented by binary functions because not all subsets are decidable. Regarding your third option: that is just describing countable sets, possibly with decidable equality. And as soon as you say "realized" that means you're at stage three and you're thinking of a particular model. Whatever you discover a particular model may not be applicable to constructive mathematics in general.


Oh, and I guess that an axiom stating that all subsets of finite sets are decidable (and therefore finite) would yield choice for finite sets which would enough to get LEM, right?


... And what if I change selection/specification so that a subset cannot be defined by an arbitrary predicate but only by a decidable one?

Then you cannot do any serious mathematics, as I explained in this MathOverflow answer.


Very interesting talk, and more relevant than ever a decade later as mathematicians keep applying the Platonist standard to our Aristotelian machines. I am still stuck on the anger part.

Few questions, the number $a=1$ if Riemann hypothesis is true, and $a=0$ if it is not, is not a valid number for the lack of effective decision procedure. How then is A or B a set? I realize set theory is still used, but this seems inappropriate. Why not keep logic away from constructions (which sets are) all the way through?

Similarly, why is the notion of finite set defined in the same way as classically? These highly non-constructive meaningless notions is exactly why I was attracted to exploring constructive mathematics. Clearly the correct interpretation is that the set is FINITE (assuming for the moment we accept it even is a set rather than a logical predicate), but there is no bijection to a finite string of natural numbers.

It would be more convincing if constructive mathematicians went "all in" on constructive mathematics, rather than letting classical mathematics hold them back. The anger creeps in from the word games that need not be played.

@Tony: Remember that constructive mathematics makes no explicit assumptions about effective procedures. In particular, it does not require everything to be effective, although it is consistent to assume that everything is constructive.

Regarding your example of the number $a = 1$ if the Riemann hypothesis holds and $a = 0$ if it does not: your definition is not yet complete, as you have not demonstrated that the Riemann hypothesis is decidable, and so you have not yet defined the number $a$. It is not clear what sets $A$ and $B$ you are referring to.

There are several notionf of finite sets. I used a very strong one, because it fit my purposes. In constructive mathematics, and in mathematics in general, picking the correct definition is a matter of getting work done most efficiently and with greatest insight.

You seem to think that constructive mathematics is a political affair laden with philosophical conundrums. Perhaps it was a long time ago, but not anymore. Ideology cannot replace proficiency.

Elif Uskuplu

Thanks for this very interesting talk and paper. I'm very new in HoTT, and I saw the video of the talk in a Youtube playlist related to HoTT. Since I started my pure math education, I've been trained deeply in classical sense. My favorite mathematician was Cantor and my favorite theorem was CSB theorem :) Before I meet with constructive math, I didn't even think that the possibility of omitting LEM, or that Cantor's paradise may not be so. I still appreciate all of works done by "classical" mathematicians, but I belive such a new kind of thoughts is worth to study on it. Today's math is almost lying on the works done in 1900s, and maybe, the future' math will be lying on the works done in 2000s. To rethink everything we took for granted is always a progressive idea. And thank you again for providing new perspective to me.

Post a comment:
Write your comment using Markdown. Use $⋯$ for inline and $$⋯$$ for display LaTeX formulas, and <pre>⋯</pre> for display code. Your E-mail address is only used to compute your Gravatar and is not stored anywhere. Comments are moderated through pull requests.