Search

The purpose of the present paper is to give a formulation of the simple theory of types which incorporates certain features of the calculus of λ-conversion. A complete incorporation of the calculus of λ-conversion into the theory of types is impossible if we require that λx and juxtaposition shall retain their respective meanings as an abstraction operator and as denoting the application of function to argument. But the present partial incorporation has certain advantages from the point of view of type theory and is offered as being of interest on this basis (whatever may be thought of the finally satisfactory character of the theory of types as a foundation for logic and mathematics).For features of the formulation which are not immediately connected with the incorporation of λ-conversion, we are heavily indebted to Whitehead and Russell, Hilbert and Ackermann, Hilbert and Bernays, and to forerunners of these, as the reader familiar with the works in question will recognize.The class of type symbols is described by the rules that ı and o are each type symbols and that if α and β are type symbols then (αβ) is a type symbol: it is the least class of symbols which contains the symbols ı and o and is closed under the operation of forming the symbol (αβ) from the symbols α and β.

The attempt to exclude the well-known pardoxes of set theory from a system of formal logic, without at the same time rendering the system so weak as to be inadequate for the purposes of mathematics, may be made in various ways. Currently the most favored methods are the Zermelo axiomatic set theory and the simple theory of types. As is well known, the simple theory of types may be described in the following terms. A particular domain, to be called the domain of individuals is selected; this may be any domain within very wide limits, but in any particular system must be treated as fixed. Classes and relations (and functions, if the system provides for such) are then classified into a hierarchy of types. For simplicity in the description of this hierarchy it is convenient to think of relations (and functions) as defined in terms of classes following a suggestion first made by Wiener in 1914. On this basis, the first type is composed of the individuals, the second type of classes of individuals, the third type of classes of classes of individuals, and so on. The restriction imposed by the simple theory of types is that the members of a class which belongs to the type n +1 must all belong to the type n. There is no provision for classes which do not belong to a type: classes not obeying the restriction just stated are regarded as non? existent, and names for such classes are excluded from the system. And even to say or write a e b (that a is member of the class b) is excluded as not well-formed unless the variables or constants a, b show by their syntactical form that, for some n, they refer to types n and n + 1 respectively. (Of course, the foregoing statement cannot be made within the system based on the simple theory of types which is being described, but only within some stronger system, e.g., one employing transfinite types. For the purpose of the formal construction of the system it is not