Initiation to constructive mathematics

I have a soft spot for Constructivism in Mathematics: An Introduction (2 volumes) by Troelstra and van Dalen as an overview. And for what one loses compared to classical mathematics (as well as its historical importance), it's probably worth going straight to Bishop's Foundations of constructive analysis.

However, an important thing to be aware of when reading older and historical works is that they may give a misleading impression of constructivism as currently practiced. Historical overviews such as Troelstra-van Dalen or Bridges-Richman will often spend time contrasting schools of constructivism such as Brouwer's intuitionism, Markov's constructive recursive mathematics, and Bishop's constructive mathematics. This is certainly interesting and historically important, but in my (humble) opinion, the trend of the future in constructivism is towards "neutral" constructive mathematics, which historically was a bit of a latecomer.

The three historical "big schools" all assume various principles that deviate from neutral constructivism, some of which are even classically contradictory. While some of those principles (notably ones like Markov's principle and countable choice, which are weak "computable" forms of LEM and AC and in particular are consistent with classical mathematics) are still in wide use today, it's become more fashionable to at least notice when they are used and attempt to avoid them if possible.

One important reason for this is that neutral constructivism is valid internal to any elementary topos, whereas these additional principles are not. Topos theory has also led to important insights into the best way to do mathematics constructively, such as the use of locales as a good notion of "space".

Thus, I would recommend supplementing your historical reading with some more modern work. Bauer's Five stages of accepting constructive mathematics cited in the comments is an excellent start. But unfortunately, I don't know of a good book-length work to follow it.

One of my own early introductions to constructivism was a course on constructive locale theory given by Peter Johnstone, much of which became Part C of Sketches of an Elephant; but that may be a bit difficult to follow without some background in category theory and topos theory (such as obtained from Parts A and B). The HoTT Book also includes some explanation of modern approaches to doing mathematics constructively, particularly chapters 10 and 11 (plus a few remarks in the introduction); but, again, it may be hard to get there without slogging through chapters 1-9. And of course there is Taylor's Practical foundations of mathematics, which has many nice features but which Peter Johnstone famously called "the book of which Mathematics Made Difficult was a parody". So overall I think there is room here for someone to write a good book.


I'm personally a fan of the book Varieties of constructive mathematics by Bridges and Richman. It begins with a general overview and then devotes a separate chapter to each of a number of standard constructivist approaches, and I found it overall very accessible.


MR0485251 Per Martin-Löf, Notes on constructive mathematics. Almqvist & Wiksell, Stockholm, 1970.