The Present Version of Constructive Type Theory (1995)

Abstract

What is here being called the present version of constructive type theory is a synthesis and elaboration of the versions (7) and (8) of constructive type theory. This chapter sets out with preliminaries which are philosophical methodological guidelines underlying the organization and presentation of the present version of constructive type theory. The following two sections discuss the non-dependent types and objects as well as the dependent types and objects resp. The third section moreover explains, how to construct new types and objects from given ones, where the former will be called function types and the latter function objects. These sections define a whole type structure, but nothing has been said so far about what types there are. The sixth and seventh sections introduce two ground types, namely the ground type of sets and the ground type of propositions resp. And the ‘application’ of the just mentioned type structure to the ground type of sets yields in the ninth section constructive set theory, while the ‘application’ of the same type structure to the ground type of propositions yields in the tenth section constructive logic. The eleventh section reveals that the theories of these two ground types, i.e. constructive set theory and constructive logic, not only share the same (type-) structural features, but they also have other essential features in common which allow to establish a precise correspondence (often called isomorphism) between sets and propositions. The twelfth and last section introduces the sequents and shows that there is a precise correspondence (that can also be called isomorphism) between types and sequents.