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

PREFATORY STATEMENT

xxvii

two of Nc',/ with adequate actual types. The type of Nc'a and Nc',8 in
Nc'a = Nc'/3 is not affected by it. It is evident that the conventions IT, IIT
are not sufficient to secure the truth of this proposition as thus symbolized.
It is essential that in the equation the type be adjusted adequately for
both formal numbers. In fact the general arithmetical convention, that
types of equational as well as of arithmetical occurrences are adjusted
arithmetically, is here used.
V. Some Important Principles.
Principle of Arithmetical Substitution. In *120'53, the application of IIT
needs a consideration of the whole question of arithmetical substitution.
Consider the first of the two examples. We have
I-: /3=7+c 8.! /. )~ = av x ca.
It is obvious that unless we can pass with practical immediateness from
" / = 7 +0 8. a = a " to " as = ar+c " by *20-18, arithmetic is made practically
impossible by the theory of types. But a difficulty arises from the application
of IIT. Suppose we assign the types of our real variables first. Then the
types of a, /, y, 8 can be arbitrarily assigned, and there is no necessary
connection between them which arises from the preservation of meaning.
Thus / may be in a type which is not an adequate type for 7 +c 8. Assume
that this is the case. But the equational use of 7 +c is in the same type
as /9, and by IIT the arithmetical use of 7+0 8 in xay+c is in an adequate
type. Thus, on the face of it, the reasoning, appealing to *20'18, by which
the substitution was justified, is fallacious; for the two occurrences of 7 +o 8
in fact mean different things.
In order to generalize our solution of this difficulty it is convenient to
define the term "arithmetical equation." An arithmetical equation is an
equation between purely arithmetical formal numbers whose actual types
are both determined adequately. Then it is evident that from "a = T. f(v),"
where a and T are formal numbers and T occurs arithmetically in f(T), we
cannot infer f(o) unless the equation a = is arithmetical. For otherwise
the T in the equation cannot be identified with the T in f(r).
When we have ",/ =.f (r)," where T is a formal number and 3 is a
number in a definite type, and wish to pass to "f(/3)," or "3 =.f(/)" and
wish to pass to "f(r)," the occurrence of Tin f(r) being arithmetical, the
type of / may not be an adequate type for r. Accordingly the r in " =T "
cannot be identified with the T in f(T). The type of the T in the equation
ought to be freed from dependence on that of /3. Accordingly the transition
is only legitimate when we can write instead
",8+0=T-.f (T)" or " 3+c0=T.f(/3),"