Course on Constructive Logic and Lambda Calculus
D, 6 points
Lecturer
Anton Setzer,
House 2, Room 138,
Tel. 018 4713284,
Schedule
Weekly (with some exceptions to be announced),
Monday, 15.15 - 17.00, House 2, Room 314.
Friday, 13.15 - 15.00, House 2, Room 315.
First lecture: August 31, 1998.
Continuation after Christmas: from January 8 till (at the latest) January 18, 1999.
Topics covered
Intuitionistic Logic. Brouwerian counterexamples. Elementary constructive
analysis and algebra. Relationship between classical and constructive
logic: double-negation translation. Properties of disjunction and
existence. Realizability. Kripke-models and completeness theorem.
Proof theory for intuitionistic logic. Normalization.
Lambda calculus and logic of combinators. Church-Rosser theorem.
Fixed point theorem. Representability of recursive functions.
Undecidability Results. Models of the lambda calculus:
D^{\infinity} models, reflexive domains. Typed
lambda calculus.
Gödel's dialectica translation, Curry-Howard Isomorphism. Martin-Löf's
type theory.
Literature
Troelstra, A. S., van Dalen, D.: Constructivism in mathematics, vol. 1.
North Holland, 1988.
Hindley, J. R., Seldin, J. P.: Introduction to combinators and lambda
calculus. Cambridge University Press, 1986. (This book is not available
any longer, but we are allowed to copy parts of it for this course).
Reference Literature
Troelstra, A. S., van Dalen, D.: Constructivism in mathematics, vol. 2.
North Holland, 1988.
Barendregt, H. P.: The lambda calculus - its syntax and semantics. North-Holland,
1984.
Martin-Löf, P.: Intuitionistic type theory. Bibliopolis, 1984.
Additional material on type theory and proof theory.
Erik Palmgren's course notes
on Constructive Mathematics give a nice brief introduction into the subject.
Lecture Notes, Handouts
Plan
Numbers after an item indicate chapters in the relevant books.
Numbers after an E: mean exercises recommended for this section.
Following numbers refer again to the relevant books,
expressions of the form P n, where n is a natural number,
refer to Problem n in the List of Problems
- 0. Overview and introduction
- Part A: Constructive mathematics
In this part all numbers, unless stated differently,
refer to the book of Troelstra, van Dalen vol. 1
- 1. Introduction (1)
- 1.1. Examples of non-constructive proofs (1.2.)
- 1.2. Directions in the foundations of mathematics (1.1, 1.4)
- 1.3. The Brouwer-Heyting-Kolmogorov (BHK) interpretation of the logical
connectives (1.3.1)
E: 1.3.1
- 1.4. Brouwerian counter examples (1.3.2 - 1.3.7)
E: 1.3.3., P 1
- 2. Predicate logic and constructivism (2)
- 2.1. Natural deduction and intuitionistic logic (2.1, 2.3.2)
E: 2.1.1., 2.1.2., 2.1.9
- 2.2. Logic with existence predicate (2.2.1. - 2.2.4)
E: 2.2.1., 2.2.2.
- 2.3. The double negation translation (2.3.1. - 2.3.8)
E: 2.3.1., 2.3.3.
- 2.4. Kripke Semantics (2.5.1 - 2.5.9, 2.5.11, 2.5.13)
E: 2.5.1., 2.5.2., 2.5.4., 2.5.6
- 2.5. Soundness and completeness for Kripke Semantics (2.6.)
- 3. Arithmetic (3)
- 3.1. Primitive recursive arithmetic (PRA) (3.2.)
- 3.2. Heyting Arithmetic (HA) (3.3.)
- 3.3. Friedman's A-translation (3.5.1 - 4)
- 3.4. Disjunction property and explicit definability for
numbers in HA (3.5.6 - 3.5.12, 3.5.14 - 3.5.17)
- 3.5. Kleene-realizability (4.4)
- 3.6. HA^\omega (Troelstra, van Dalen, vol. 2, 9.1)
- 4. The real numbers (5.1. - 5.4, 6.1. - 6.2.)
- Part B: Lambda Calculus
In this part all numbers, unless stated differently, refer to the book
of Hindley and Seldin
- The lambda calculus (1)
- Combinatory logic (2)
- The fixed point theorem (3A, 3B; some remarks on 3D)
- Representing the recursive functions (4)
- The undecidablity theorem (5)
- The formal theories lambda beta and CLw (6A, 6B)
- Extensionality in lambda-calculus (7)
- Models of CLw (10)
- Models of lambda beta (11)
- D_infinity and other models (12)
- Typed lambda calculus and combinatory logic (13)
- Strong normalization of the typed lambda calculus (Appendix 2)
- Part C: Martin-Löf's type theory