Principia mathematica, vol. 1 (of 3)

The notations introduced in this and the two following numbers serve to express the type of one variable in terms of the type of another. They are very useful in arithmetic, where it is necessary to take account of types in order to avoid contradictions. The two chief notations are "," for the type in which is contained, and "," for the type of which is a member. We put

This defines "the type of members of ," or "the type which is of the same type as ." The characteristic of a type is that if is a type, we have and conversely, if , then is a type. For in that case, "" is true whenever it is significant, i.e. whenever belongs to the type which is the range of significance of in "." Consequently is this range of significance, i.e. is a type.

Since we have (, it follows that is a type. It is not "the type of ," but "the type of the members of ." (In case is null, "the type of the members of " may be interpreted as meaning "the type to which belongs when '' is significant.") "The type of ," i.e. the type of which is a member, is defined as follows:

In short, consists of everything either identical or not identical with , that is, every for which there is such a proposition, whether true or false, as "." We put "" here instead of "," because need not be a class, and is in fact subject to no limitation whatever, whereas "" is not significant unless is a class, and therefore we write "" rather than "."

In virtue of *20·8, we have i.e. if "" is significant, then the range of significance of the function is the type of . It follows that two ranges of significance which overlap are identical, and two different ranges of significance have no member in common.

Thus given any two objects which are members of any one of the following: the type of , the type of the classes to which belongs, the type of the classes to which these classes belong, and so on, we can express the type of either of our two objects by means of its relation to the other object.

The propositions of this and the two following numbers will hardly ever be used until we come to cardinal arithmetic. They are used constantly in the first section on cardinal arithmetic, and they are constantly relevant in the first section on relation-arithmetic. Moreover they are usually required for cardinal and ordinal existence-theorems.

I.e. if there is any function satisfied by both and , then is of the type of . It is necessary to the use of this proposition that, if is a typically ambiguous function, it should receive the same typical determination for and for . For example, we have always and ; but we must not regard these as values of one function , because such a function is typically ambiguous. On the other hand, and are values of one function , because here the presence of a renders the function typically determinate.