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

xxiv

PREFATORY STATEMENT

The identification of types in argumental and attributive occurrences
by IT is rendered necessary to secure the use of the equivalence
r sm"oa. -.()a). a c-. 7 sm a,
where o is a formal number. Without the convention, this application of
*37'1 would be fallacious. The only one of our examples to which this part
of the convention applies is *101'28 (demonstration), where it secures that
the two occurrences of 1 are in the same type. It is relevant however to the
symbolism in the demonstration of *100'521.
It will be found in practice that this convention relates the types of
occurrences in the same way as would naturally be done by anyone who was
not thinking of the convention at all. To see how the convention works,
we will run through the examples which have already been given above.
In *100'35, IT directs the logical and equational occurrences of Nc'a to
be in the same type, and similarly for Nc',/. Also " meaning" secures that
the equational types of Nc'a and Nc',/ are the same. Thus these four
occurrences are all in one type, which has no necessary relation to the types
of the attributive occurrences of Nc'a and Nc'3,. Thus, using the notation
of *65*04 to secure typical definiteness, *100'35 is to mean:.! Nc (f)'a. v.! Nc ()'/3: ):
Nc ()'a = Nc (y)'.. a e Nc (a)'r,. -.. e Nc (/3)'a.. asm 3.
The types of these attributive occurrences are settled by the necessity
of " meaning."
In *100'42 (demonstration), since all the occurrences of formal numbers
are equational, IT produces no limitation of types.
In *100'44 (demonstration), IT secures that the two occurrences of Nc'a
are in the same type. Also we notice that the first occurrence of Nc',8 is
really (cf. *65'04) Nc (a)',/, since "a e,u" occurs, and thus "meaning" requires
this relation of types, and the second occurrence of Nc',/ is in the type of the
occurrences of Nc'a.
In *100*511, IT directs that the logical and argumental occurrences are
to have the same type. In *100'521, IT directs that the two occurrences
of sm"tL are to have the same type. In *101-28 both occurrences of 1 are
to be in the same type. In *101*38, IT directs that all the occurrences of 2
are to have the same type.
The convention IT in no way limits the types in *110-54, nor in *116-63,
nor in *117'108.
In the first example from *120*53 (in the demonstration) convention IT
has no application.
In the second example from *120'53 (in the demonstration) convention
IT directs that the two occurrences of aP shall be in the same type; and the