Principia mathematica, by Alfred North Whitehead ... and Bertrand Russell.

*63. RELATIVE TYPES OF CLASSES.

Summary of *63.
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 "to'a," for the
type in which a is contained, and " tx," for the type of which x is a member.
We put
*63'02. t'a = a v -a Df
This defines " the type of members of a," or " the type which is of the
same type as a." The characteristic of a type is that if r is a type, we have
(x). x e T,
and conversely, if (x). x e T, then T is a type. For in that case, "x e " is true
whenever it is significant, i.e. whenever x belongs to the type which is the
range of significance of x in " x e T." Consequently T is this range of significance, i.e. is a type.
Since we have (x). xe(a u - a), it follows that a v - a is a type. It is
not " the type of a," but " the type of the members of a." (In case a is null,
" the type of the members of a" may be interpreted as meaning " the type to
which x belongs when ' x e a' is significant.") "The type of x," i.e. the type
of which x is a member, is defined as follows:
*63 01. t'x = t'x u - t'x Df
By what was said above, " to'x " is the type of the members of t'x, i.e. the
type of x. By combining the definitions of t'x and to'a, we obtain
F. t'x = tot'x.
Thus F. x et'x and F: y x. D. y e t'x.
In short, t'x consists of everything either identical or not identical with x,
that is, every y for which there is such a proposition, whether true or false,
as " y = x." We put " tx " here instead of " t'a," because x need not be a
class, and is in fact subject to no limitation whatever, whereas "t0x" is
not significant unless x is a class, and therefore we write "to'a" rather
than "to'x."
27-2