Announcements

• There is a YouTube channel for the course.
• The first meeting is Tuesday, January 12!
• The course is now over, thanks to everyone who participated!

Lecture Plan

Date	Topics	Readings
1/12	Introduction and overview: Brouwerian Intuitionism, Markov's Russian Constructivism, Bishop's Constructivism, subtleties of the Proof Interpretation	The SEP articles listed below; Troelstra's History of Constructivism in the Twentieth Century
1/19	Brouwer's rejection of LEM; Heyting arithmetic: MR, IPR, DP, EDN	Brouwer's Unreliability of the logical principles; sections 3.1–3.5 of TvD vol. 1
1/26	Brouwerian analysis: Bar induction, the Fan theorem and their consequences	Brouwer's 1927 On the domains of definition of functions; sections 4.2, 4.6–4.8 of TvD vol. 1
2/2	Markov's constructivism; Church's thesis, Specker sequences	Beeson sections 4.1–4.7, Kushner's review of Markov's constructive mathematical analysis.
2/9	Guest lecture by Frank Pfenning	Per Martin-Löf, On the Meanings of the Logical Constants and the Justifications of the Logical Laws and Pfenning, Lecture Notes on Judgments and Propositions.
2/16	CANCELLED
2/23	Introduction to Realizability	Beeson VI.1–2 and VII.
3/1	Topological, Kripke and Beth semantics	Dummett Ch. 5; van Dalen's 2001 Intuitionistic Logic.
3/8	SPRING BREAK
3/15	Kevin Kelly: Theory choice (slides); Egbert Rijke: Elementary toposes
3/22	More sheaf semantics and Ryan on Formal topology	Palmgren, Constructive Sheaf Semantics; Vickers, Topology via Logic (1989)
3/29	Evan on the effective topos; Jacob on synthetic differential geometry
4/5	Kevin Kelly; computability aspects of learning; Patrick on “Brouwer and the formalists”
4/12	Sam on intuitionistic modal logic; Marc on constructive notions of finite subsets
4/19	Andrew on constructive nonstandard arithmetic; some comments on formal topology and classifying toposes
4/26	Colin on Dummett's anti-realism argument; Sam on constructive set theory

Course Description

In this seminar we shall read primary and secondary sources on the origins and developments of intuitionism and constructive mathematics from Brouwer and the Russian constructivists, Bishop, Martin-Löf, up to and including modern developments such as homotopy type theory. We shall focus both on philosophical and metamathematical aspects. Topics could include the Brouwer-Heyting-Kolmogorov (BHK) interpretation, Kripke semantics, topological semantics, the Curry-Howard correspondence with constructive type theories, constructive set theory, realizability, relations to topos theory, formal topology, meaning explanations, homotopy type theory, and/or additional topics according to the interests of participants.

Texts

• Jean van Heijenoort (1967), From Frege to Gödel: A Source Book in Mathematical Logic 1879–1931, Cambridge, MA: Harvard University Press.
• Michael Dummett (1977/2000), Elements of Intuitionism (Oxford Logic Guides, 39), Oxford: Clarendon Press, 1977; 2nd edition, 2000.
• Michael Beeson (1985), Foundations of Constructive Mathematics, Heidelberg: Springer Verlag.
• Anne Sjerp Troelstra and Dirk van Dalen (1988), Constructivism in Mathematics: An Introduction (two volumes), Amsterdam: North Holland.

Additional resources

• Constructivists' Hymn by S. Y. Maslov.
• Constructive Mathematics by Douglas Bridges and Erik Palmgren in the Stanford Encyclopedia of Philosophy (SEP).
• Intuitionism in the Philosophy of Mathematics by Rosalie Iemhoff (SEP).
• Intuitionistic Logic by Joan Moschovakis (SEP).
• The Development of Intuitionistic Logic by Mark van Atten (SEP).
• Luitzen Egbertus Jan Brouwer by Mark van Atten (SEP).
• The nLab: a wiki-lab on Mathematics, Physics and Philosophy from the point of view of (higher) category theory.