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)

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”.

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.

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

notthe 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

identicalin classical and constructive mathematics.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

generalsubsets 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.