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

xii

PREFATORY STATEMENT

individuals, but any other starting-point is equally legitimate. Whatever type
of functions (including Indiv) we start from, all higher types of functions are
excluded from the extensional hierarchy, and also all lower types (if any).
Some complications arise here. Suppose we start from Indiv. Then if 0!
is any predicative function of individuals, z (4! z) = O! z. But identity
between a function and a class does not have the usual properties of identity;
in fact, though every function is identical with some class, and vice versa, the
number of functions is likely to be greater than the number of classes. This
is due to the fact that we may have ^ (! z) =!. z (! z) =x! z without
having *! 2 = X! z.
In the extensional hierarchy, we prove the extension from classes to
classes of classes, and so on, without fresh primitive propositions (*20, *21).
The primitive propositions involved are those concerning the functional
hierarchy.
From all these various modes of extension we "see" that whatever can
be proved for lower types, whether functional or extensional, can also be
proved for higher types*. Hence we assume that it is unnecessary to know
the types of our variables, though they must always be confined within some
one definite type.
Now although everything that can be proved for lower types can be
proved for higher types, the converse does not hold. In Vol. I. only two
propositions occur which can be proved for higher but not for lower types.
These are a! 2 and [! 2r. These can be proved for any type except that of
individuals. It is to be observed that we do not state that whatever is true
for lower types is true for higher types, but only that whatever can be proved
for lower types can be proved for higher types. If, for example, Nc'Indiv = y,
then this proposition is false for any higher type; but this proposition,
Nc'Indiv = v, is one which cannot be proved logically; in fact, it is only
ascertainable by a census, not by logic. Thus among the propositions which
can be proved by logic, there are some which can only be proved for higher
types, but none which can only be proved for lower types.
The propositions which can be proved in some types but not in others all
are or depend upon existence-theorems for cardinals. We can prove
a! 0, a! 1, universally,
g! 2, except for Indiv,
a! 3, a! 4, except for Indiv, Cl'Indiv, Rl'Iadiv; and so on.
Exactly similar remarks would apply to the functional hierarchy. In both
cases, the possibility of proving these propositions depends upon the axiom
of reducibility and the definition of identity. Suppose there is only one
individual, x. Then - = x,: x are two different functions, which, by the
* But cf. next page for a more exact statement of this principle.