House 2, Room 138,

Tel. 018 4713284,

Monday, 15.15 - 17.00, House 2, Room 314.

Friday, 13.15 - 15.00, House 2, Room 315.

First lecture: August 31, 1998.

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.

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

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 on HA^omega, constructive reals and lambda-calculus (They replace Handout2 - Handout7 and will be updated as the course proceeds).
- Handout 1: A sequent version of the natural deduction calculus
- Examples relevant for getting points for this course (in reverse order)
- List of additional Problems

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

- 2.1. Natural deduction and intuitionistic logic (2.1, 2.3.2)
- 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.)

- 1. Introduction (1)
- 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