Course on Constructive Logic and Lambda Calculus

D, 6 points


Anton Setzer,
House 2, Room 138,
Tel. 018 4713284,
Replace '_dot_' by '.' and '_at_' by '@' in 'a_dot_g_dot_setzer_at_swan_dot_ac_dot_uk'


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.


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


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