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