Volume 1 / Part 3 — *118. ARITHMETICAL SUBSTITUTION AND UNIFORM FORMAL NUMBERS.
Reading edition
*118. ARITHMETICAL SUBSTITUTION AND UNIFORM FORMAL NUMBERS.
Summary of *118.
A difficulty arises respecting substitution in arithmetic. For if is a formal number and its occurrence in is arithmetical, then by is always to be taken in an existential type. Hence we can only substitute a real variable for under the hypothesis , and we can only substitute another formal number for provided that the equation , which justifies the substitution, is arithmetical, i.e. provided that in this equation the type of is such that .
The result is that the application of *20·18 is apt to lead to fallacies owing to the different meanings which a formal number may possess in different occurrences. Hitherto we have considered each case in detail, e.g. note on *110·61, and proof of *110·56.
The condition for the safe application of *20·18 is given in *118·01, namely
*118·01.
This question is more fully discussed in the prefatory statement of this volume. The first reference to *118·01 is in *120·222. Another way of evading the difficulty is to work with formal numbers which, together with all their components, are of the same type. This leads to the consideration of Uniform Formal Numbers, which with the exception of *118·01 occupies the rest of the number.
The dominant type of a formal number as used in any context is the type of the formal number itself in that context, and the subordinate types of the formal number are the dominant types of its component formal numbers.
When the dominant types of some of the formal numbers are not expressly indicated by an explicit notation (cf. *65), the rules according to which the dominant types thus left ambiguous are to be related, so far as they are related, including the rules governing the relation of subordinate types, if left ambiguous, to dominant types, are given by conventions , , and of the prefatory statement in this volume.
We have now to consider an important special case which arises when types are explicitly indicated by the use of *65·01·03. A formal number, whose subordinate types are the same as its dominant type, is called uniform; and if some of its subordinate types are the same as its dominant type, it is called partially uniform. A formal number can only be partially uniform, or at least so designated as to be necessarily partially uniform, when the dominant type and those subordinate types identical with it are expressly indicated by *65·01·03. For otherwise the conventions , , and perhaps also , apply; and these do not secure uniformity, and may perhaps in some contexts be inconsistent with it.
Common sense in its consideration of arithmetic habitually disregards the possibility of a formal number representing . In other words, it always applies conventions and . But also, owing to its disregard of types, it assumes that the formal numbers are all uniform. The assumption which is really essential to this common sense reasoning, so far as the form of its arithmetical conclusions are concerned, is the assumption that none of the numerical symbols represent . This assumption is secured here, when no types are expressly indicated, by and . We have now to consider the effect on arithmetical operations of the other assumption, that the formal numbers are uniform, or partially uniform. There is no difficulty arising from any change of convention for symbolism, since, as stated above, partial or complete uniformity is secured by express indication of type. Accordingly conventions , continue, as always, to apply when the types of formal numbers are left ambiguous.
Convention will not be applied either in *118 or *119 or *120: in *118 the fact is entirely unimportant since the dominant types of equational occurrences are always indicated, so that no case arises when it could apply.
Apart from its intrinsic interest and its bearing on substitution, the arithmetic of uniform formal numbers is necessary for *120, where the fundamental arithmetical properties of inductive numbers are investigated.
The propositions of this number are proved by the use of the results of *117. The basis of the reasoning is
*118·13.
In *118·2·3·4 the meaning of the symbolism for dominant types is stated, namely
*118·2.
*118·3.
*118·4.
The important propositions which are finally reached for addition are
*118·23.
*118·24.
*118·241.
*118·25.
The important propositions for multiplication are
*118·33.
*118·34.
*118·341.
*118·35.
*118·351.
The important propositions for exponentiation are
*118·43.
*118·44.
*118·441.
*118·45.
*118·451.
*118·46.
*118·461.
with two analogous propositions *118·462·463,
*118·47.
*118·471.
with two analogous propositions *118·472·473.
It is thus seen that, apart from some exceptional cases connected with 0 and 1, in all arithmetical operations uniform, or partially uniform, formal numbers can replace those constructed in obedience to convention .
*118·01.
As far as the symbolism is concerned, this proposition with the omission of from the hypothesis is a transcript of *20·18. But if or (not excluding both) is a formal number, is required in case the occurrence of in is arithmetical. In fact this proposition embodies the three fundamental propositions of the Principle of Arithmetical Substitution arrived at in the Prefatory Explanations on Types. Its necessity arises from the convention which is explained there.
*118·11.
Dem.
*118·12.
*118·13.
*118·2.
*118·201.
*118·21.
Dem.
Here the reference is to the convention explained in the prefatory statement.
*118·22.
Dem.
*118·23.
Dem.
*118·24.
Dem.
*118·241.
*118·25.
Dem.
*118·3.
*118·301.
*118·31.
Dem.
*118·311.
*118·32.
Dem.
*118·33.
*118·34.
Dem.
*118·341.
*118·35.
*118·351.
*118·352.
*118·4.
*118·401.
*118·402.
Dem.
*118·41.
Dem.
*118·411.
*118·42.
*118·421.
*118·43.
*118·44.
*118·441.
*118·45.
Dem.
*118·451.
Dem.
*118·46.
*118·461.
Dem.
*118·462.
*118·463.
*118·47.
*118·471.
Dem.
*118·472.
*118·473.