Title: Combinatory Logic, Predicate Logic, Type Theory 
       and The Foundation of Mathematics

Abstract:

Combinatory Logic(and lambda calculus) were first invented as very
simple bases from which to develop logic, arithmetic and mathematics
as a whole. Both Church's and Curry's systems, dating back to the
1930s, however, were proved inconsistent by Kleene and Rosser.
Systems of illative combinatory logic (and lambda calculus) have since
been developed that avoid the known paradoxes and still allow the
development of logic, arithmetic, set theory etc. Only limited
consistency has been proved.
Modern type theory, which stems from early work of Church and Curry,
has developed quite independently and has become much used in Computer
Science. Surprisingly the valid statements of the form 
  x_1:A_1,...,x_n:A_n |- M:B
of very general type systems, can be translated into valid statements
of illative combinatory logic of the form
X_1,...,X_n |- Z.
The reverse also holds for appropriate  X_1,...,X_n.
The seminar will introduce illative combinatory logic. It will show
how this avoids the Curry paradox and indicate how it is used for the
building up of logic, arithemetic and set theory. An idea of the
relations between illative combinatory logics and type systems will
also be given.