Philosophical and Technical Prehistory of Constructive Type Theory (1880–1970)

Abstract

This chapter intends to introduce some of the philosophical logical ideas and preconceptions as well as some of the mathematical logical instruments and techniques which led up to or influenced the development of constructive type theory. The first section discusses the place of constructive type theory w.r.t. two different approaches to or traditions of logic. It is of a more philosophical flavor. The second section presents in a chronological and systematic way some of the important technical prerequisites of constructive type theory. In this chronology are inserted some of Martin-Löf’s works on normalization which can be seen to give rise to the first version of his type theory in 1970. This second section is by its nature more mathematical. Both sections mean to cast some light onto the logical history prior to the establishment of constructive type theory, that is onto the prehistory of this theory.