L. E. J. Brouwer

Intuitionism and
Constructive Mathematics

80-518/818 — Spring 2016

Meeting place and time: Doherty Hall 4303 — Tu 1:30–3:50pm
Instructor: Ulrik Buchholtz (ulrikb[at]andrew.cmu.edu)
Office: Baker Hall 152
Office Hours: by appointment
Course title: Seminar on Topics in Logic

Andrey Markov, Jr.


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


Additional resources