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

PREFATORY STATEMENT

xix

The method of definition which we adopt is to replace the formal number
a by another one a-' so related to a- that with the same actual type for both
we can prove a! a-'. a! ar, whenever a- is not equal to A in all types.
If a be functional, we need only consider its argument, or its two arguments,
and can dismiss from consideration the other components; then we replace
these arguments by others so that the a' has the required property. Thus:
(i) The actual types of Nc'a, 2Nc'K, fINc'K, and sm"pa are adequate
when we can logically prove! Nc'to'a, a! Nc'to'K, a! IINc'to'Kc, and t! sm"to',;
(ii) The actual types of L +c v, i- v, p xc v, and pv are adequate when
we can logically prove
a! Noc't'/l +o Noc't'v, [! NoC't1'p - 0 t' v,
a! Noc'tl'p xo Noc't'Cv, and a! Noc't1'pNoc'tl'Y.
It will be noticed that to'a, to',c, and to'p are the greatest classes of the
same type as a, K, and p respectively, and that Noc't'pa and Noc't1'v are the
greatest cardinal numbers of the same type as p and v respectively. These
definitions hold even when any of a, K, j, v are complex symbols.
The remaining formal numbers which are not functional must certainly
be constant. The difficulty which arises here is that if a be such a formal
number and K, occurs in its symbolism, we have no logical method of
deciding as to the truth or falsehood of g! M0 in any type. But we replace
0o by Noc't,'/o which is the greatest existent cardinal of the same type as No
in that occurrence. Thus:
(iii) If a- be a formal number which is not functional, an adequate
actual type of ao is one for which we can logically prove a! a', where a' is
derived from a by replacing any occurrence of No in a by Noc'tl'Ko. Accordingly if N, does not occur in a, an adequate type is any actual type for
which we can logically prove [! a-.
In the case of members of the primary and argumental groups we have
substituted the V of the appropriate type in the place of each variable.
When the actual type is adequate we have
(a). a! Nc'a, (K). g! 2Nc'K, (K).! HINc'K, (p). a!sm"p.
In the case of members of the arithmetical group (except in the case of
- -o vZ), we have substituted for each argument the largest cardinal number
which can be obtained in the type of that argument, namely the N0c'V for
the V of the appropriate type. Accordingly we are sure (except in the case
of p-cv) that for all other values of the arguments which are existent
cardinal numbers the formal number is not null.
It will be noticed that normal adjustment only concerns the subordinate
types. For example *110'03 secures that in Nc'a + p the actual type of

R.&W. II.

b