Volume 1 — PREFATORY STATEMENT OF SYMBOLIC CONVENTIONS

THE purpose of the following observations is to bring together in one discussion various explanations which are required in applying the theory of types to cardinal arithmetic. It is convenient to collect these observations, since otherwise their dispersion throughout the several numbers of Part III makes it difficult to see what is their total effect. But although we have placed these observations at the beginning, they are to be read concurrently with the text of Part III, at least with so much of the text as consists of explanations of definitions. The earlier portion of what follows is merely a résumé of previous explanations; it is only in the later portions that the application to cardinal arithmetic is made.

I. General Observations on Types.

Three different kinds of typical ambiguity are involved in our propositions, concerning:

(1) the functional hierarchy,

(2) the propositional hierarchy,

(3) the extensional hierarchy.

The relevance of these must be separately considered.

We often speak as though the type represented by small Latin letters were not composed of functions. It is, however, compatible with all we have to say that it should be composed of functions. It is to be observed, further, that, given the number of individuals, there is nothing in our axioms to show how many predicative functions of individuals there are, i.e. their number is not a function of the number of individuals: we only know that their number , where "" stands for the class of individuals.

In practice, we proceed along the extensional hierarchy after the early numbers of the book. If we have started from individuals, the result of this is to exclude functions wholly from our hierarchy; if we have started with functions of a given type, all functions of other types are excluded. Thus a fresh extensional hierarchy, wholly excluding every other, starts from each type of function. When we speak simply of "the extensional hierarchy," we mean the one which starts from individuals.

It is to be observed that when we have the assertion of a propositional function, say "," the must be of some definite type, i.e. we only assert that is true whatever may be within some one type. Thus e.g. "" does not assert more than that this assertion holds for any of a given type. It is true that symbolically the same assertion holds in other types, but other types cannot be included under one assertion-sign, because no variable can travel beyond its type.

The process of rendering the types of variables ambiguous is begun in *9, where we take the first step in regard to the propositional hierarchy. Before *9, our variables are elementary propositions. These are such as contain no apparent variables. Hence the only functions that occur are matrices, and these only occur through their values. The assumption involved in the transition from Section A to Section B (Part I) is that, given "," where is an elementary proposition, we may substitute for "," where is any matrix. Thus instead of "," which contained one variable of a given type, we have "," which contains several variables of several types (any finite number of variables and types is possible). This assumption involves some rather difficult points. It is to be remembered that no value of contains as a constituent, and therefore is not a constituent of even if is a value of . Thus we pass, above, from an assertion containing no function as a constituent to one containing one or more functions as constituents. The assertion "" concerns any elementary proposition, whereas "" concerns any of a certain set of elementary propositions, namely any of those that are values of . Different types of functions give different sorts of ways of picking out elementary propositions.

Having assumed or proved "," where is elementary and therefore involves no ambiguity of type, we thus assert where the types of the arguments and the number of them are wholly arbitrary, except that they must belong to the functional hierarchy including individuals. (The assumption that propositions are incomplete symbols excludes the possibility that the arguments to are propositions.) The noteworthy point is that we thus obtain an assertion in which there may be any finite number of variables and the variables have unlimited typical ambiguity, from an assertion containing one variable of a perfectly definite type. All this is presupposed before we embark on the propositional hierarchy.

It should be observed that all elementary propositions are values of predicative functions of one individual, i.e. of , where is individual. Thus we need not assume that elementary propositions form a type; we may replace by "" in "." In this way, propositions as variables wholly disappear.

In extending statements concerning elementary propositions so as formally to apply to first-order propositions, we have to assume afresh the primitive proposition *1·11 (*1·1 is never used), i.e. given "" and "," we have "" which is practically *9·12. This was asserted in *1·11 for any case in which and are elementary propositions. There was here already an ambiguity of type, owing to the fact that x need not be an individual, but might be a function of any order. E.g. we might use *1·11 to pass from where replaces the of *1·11, and , replace and . Thus *1·11, even before its extension in *9, already states a fresh primitive proposition for each fresh type of functions considered. The novelty in *9 is that we allow and to contain one apparent variable. This may be of any functional type (including Indiv); thus we get another set of symbolically identical primitive propositions. In passing, as indicated at the end of *9, to more than one apparent variable, we introduce a new batch of primitive propositions with each additional apparent variable.

Similar remarks apply to the other primitive propositions of *9.

What makes the above process legitimate is that nothing in the treatment of functions of order presupposes functions of higher order. We can deal with each new type of functions as it arises, without having to take account of the fact that there are later types. From symbolic analogy we "see" that the process can be repeated indefinitely. This possibility rests upon two things:

(1) A fresh interpretation of our constants—, , !, ()., ().—at each fresh stage;

(2) A fresh assumption, symbolically unchanged, of the primitive propositions which we found sufficient at an earlier stage—the possibility of avoiding symbolic change being due to the fresh interpretation of our constants.

The above remarks apply to the axiom of reducibility as well as to our other primitive propositions. If, at any stage, we wish to deal with a class defined by a function of the 30,000th type, we shall have to repeat our arguments and assumptions 30,000 times. But there is still no necessity to speak of the hierarchy as a whole, or to suppose that statements can be made about "all types."

We come now to the extensional hierarchy. This starts from some one point in the functional hierarchy. We usually suppose it to start from individuals, but any other starting-point is equally legitimate. Whatever type of functions (including 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 . Then if is any predicative function of individuals, . 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 without having .

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[1]. 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 and . 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, , then this proposition is false for any higher type; but this proposition, , 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 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, . Then , are two different functions, which, by the axiom of reducibility, are equivalent to two different predicative functions. Hence there are at least two predicative functions of , and at least two classes , . This argument fails both for classes and functions if either we deny the axiom of reducibility or we suppose that there may be two different individuals which agree in all their predicates, i.e. that the definition of identity is misleading.

The statement that what can be proved for lower types can be proved for higher types requires certain limitations, or rather, a more exact formulation. Taking as a primitive idea, put Then consider the proposition . We can prove Thus can be proved in the lowest type in which it is significant, and disproved in any other. The difficulty, however, is avoided if Indiv is replaced by a variable , and by . Then we have and this holds whatever the type of may be. Thus in order that our principle about lower and higher types may be true, it is necessary that any relation there may be between two types occurring in a proposition should be preserved; in other words, when one constant type is defined in terms of another (as and ), the definition must be restored before the type is varied, so that when one type is varied, so is the other. With this proviso, our principle about higher and lower types holds.

With the above proviso, the truth of our statement is manifest. For we have shown that the same primitive propositions, symbolically, which hold for the lowest type concerned in our reasoning, hold also for subsequent types; and therefore all our proofs can be repeated symbolically unchanged.

The importance of this lies in the fact that, when we have proved a proposition for the lowest significant type, we "see" that it holds in any other assigned significant type. Hence every proposition which is proved without the mention of any type is to be regarded as proved for the lowest significant type, and extended by analogy to any other significant type.

By exactly similar considerations we "see" that a proposition which can be proved for some type other than the lowest significant type must hold for any type in the direct descent from this. E.g. suppose we can prove a proposition (such as ) for the type (where ); then merely writing for , we have a proposition which is proved concerning , namely , and here, by what was said before, ) may be replaced by any higher type.

Thus given a typically ambiguous relation , such that, if is a type, is a type ( or is such a relation), we "see" that, if we can prove , we can also prove , where is any type, and is composed of typically ambiguous symbols. Similarly if we can prove , we can prove , where is any type. But we cannot in general prove or , and these may be in fact untrue. e.g. we have .

Thus more generally, when a proposition containing several ambiguities can be proved for the types , , ..., but not for lower types, it is to be regarded as a function of , and then it becomes true for any type; that is, given we shall also have where is any type. In this way, all demonstrable propositions are in the first instance about , and when so expressed remain true if any other type is substituted for .

When a proposition containing typically ambiguous symbols can be proved to be true in the lowest significant type, and we can "see" that symbolically the same proof holds in any other assigned type, we say that the proposition has "permanent truth." (We may also say, loosely, that it is "true in all types.") When a proposition containing typically ambiguous symbols can be proved to be false in the lowest significant type, and we can "see" that it is false in any other assigned type, we say that it has "permanent falsehood." Any other proposition containing typically ambiguous symbols is said to be "fluctuating," or to have "fluctuating truth-value," as opposed to "permanent truth-value," which belongs to propositions that have either permanent truth or permanent falsehood.

In what follows, ambiguities concerned with the propositional hierarchy will be ignored, since they never lead to fluctuating propositions. Thus disjunction and negation and their derivatives will not receive explicit typical determination, but only such typical determination as results from assigning the types of the other typically ambiguous symbols involved.

It is convenient to call the symbolic form of a propositional function simply a "symbolic form." Thus, if a symbolic form contains symbols of ambiguous type it represents different propositional functions according as the types of its ambiguous symbols are differently adjusted. The adjustment is of course always limited by the necessity for the preservation of meaning. It is evident that the ideas of "permanent truth-value" and "fluctuating truth-value" apply in reality to symbolic forms and not to propositions or propositional functions. Ambiguity of type can only exist in the process of determination of meaning. When the meaning has been assigned to a symbolic form and a propositional function thereby obtained, all ambiguity of type has vanished.

To "assert a symbolic form" is to assert each of the propositional functions arising for the set of possible typical determinations which are somewhere enumerated. We have in fact enumerated a very limited number of types starting from that of individuals, and we "see" that this process can be indefinitely continued by analogy. The form is always asserted so far as the enumeration has arrived; and this is sufficient for all purposes, since it is essentially impossible to use a type which has not been arrived at by successive enumeration from the lower types.

The only difficulties which arise in Cardinal Arithmetic in connection with the ambiguities of type of the symbols are those which enter through the use of the symbol , or of the symbol , which is . For it may happen that a class in one type has no class similar to it in some lower type (cf. *102·72·73). All fallacious reasoning in cardinal or ordinal arithmetic in connection with types, apart from that due to the mere absence of meaning in symbols, is due to this fact—in other words to the fact that in some types is true, and in other types may not be true. The fallacy consists in neglecting this latter possibility of the failure of for a limited number of types, that is, in taking the "fluctuating" form as though it possessed a "permanent" truth-value.

A fluctuating form however often possesses what is here termed a "stable" truth-value, which is as important as the permanent truth-value of other forms. For example, anticipating our definitions of elementary arithmetic, consider . There is no abstract logical proof that there are two individuals; so suppose 2 and 3 refer to classes of individuals, but 5 refers to classes of a high enough type, then with these determinations cannot be proved. But has a stable truth-value, since it can always be proved when all the types are high enough. In this case the fact that our empirical census of individuals (at least of the "relative" individuals of ordinary life) has outrun the capacity of logical proof, makes the fluctuation in the truth-value of the form to be entirely unimportant.

In order to make this idea precise, it is necessary to have a convention as to the order in which the types of symbols in a symbolic form are assigned. The rule we adopt is that the types of the real variables are to be first assigned, and then those of the constant symbols. The types of the apparent variables, if any, will then be completely determinate.

A symbolic form has a stable truth-value if, after any assignment of types to the real variables, types can be assigned to the constant symbols so that the truth-value of the proposition thus obtained is the same as the truth-value of any proposition obtained by modifying it by the assignment of higher types to some or all of the constant symbols. This truth-value is the stable truth-value.

II. Formal Numbers.

The conventions, which we shall give below as to the assignment of types, practically restrict our interpretation of fluctuating symbolic forms to types in which the forms possess their stable truth-value. The assumption that these truth-values are stable never enters into the reasoning. But we judge a truth-value to be stable when any method of raising the types of the constant symbols by one step leaves it unaltered.

In practice the fluctuation of truth-values only enters into our consideration through a limited number of symbols called "formal numbers."

Formal numbers may be "constant" or "functional."

A constant formal number is any constant symbol for which there is a constant such that, in whatever type the constant symbol is determined, it is, in that type, identical with . In other words if be a constant symbol, then is a formal number provided that "truth" is the permanent truth-value of , for some constant .

The functional formal numbers are defined by enumeration; they are where in each formal number the symbols , , , occurring in it are called the arguments of the functional form even when they are complex symbols. The argument of is , and those of are and , and those of are 1 and 2.

Thus among the constant formal numbers are The references which support this statement are

*101·11·21·32.*123·36.*110·42.*113·23.*116·23.

Among the functional formal numbers are It will be observed that e.g. is both a constant and a functional formal number, so that the two classes are not mutually exclusive. In fact they possess an indefinite number of members in common.

All the formal numbers, with the exception of and , are members of without any hypothesis [cf. *100·41·01.*110·42.*112·101.*113·23.*114·1.*116·23, note to *119·12, and *120·411].

A functional formal number consists of two parts, namely, its argument or arguments, and the constant "form." An argument of a functional formal number may be a complex symbol, and may be constant or variable. Thus is an argument of , and of ( and of (; also is an argument of (. The constant form is constituted by the other symbols which are constants. Two occurrences of functional formal numbers are only occurrences of the same formal number if the arguments and also the constant forms are identical in symbolism. Thus two occurrences of are occurrences of the same formal number, even if they are determined to be in different types; but and are different formal numbers. Also and are different formal numbers because their "forms" are different, though the arguments and 1 are the same and (in the same type) the entity denoted is the same. Thus the distinction between formal numbers depends on the symbolism and not on the entity denoted, and in considering them it is symbolic analogy and not denotation which is to be taken into account. For example two different occurrences of the same formal number will not denote the same entity, if in the two occurrences the ambiguity of type is determined differently.

The functional formal numbers are divided into three sets: (i) the primary set consisting of the forms , , , (ii) the argumental set consisting only of , (iii) the arithmetical set consisting of , , , and .

A functional formal number has at most two arguments. But an argument of a functional formal number may itself be a functional formal number, and will accordingly possess either one or two arguments, which in their turn may be functional formal numbers, and so on. The whole set of arguments and of arguments of arguments, thus obtained, is called the set of components of the original formal number. Thus , , , and are components of (; and , and are components of ; and , and are components of . The two arguments of ( are and , and those of are and , and those of are and .

Addition, multiplication, exponentiation, and subtraction will be called the arithmetical operations; and in , , , , and will each be said to be subjected to these respective operations. The arithmetical components of an arithmetical formal number (i.e. one belonging to the arithmetical set) consist of those of its components which do not appear in the capacity of components of a component which does not belong to the arithmetical set. Thus , , , are arithmetical components of ; and and are arithmetical components of , but is not one; and and are arithmetical components of , but is not one; and and are arithmetical components of , but and and are components of and are therefore not arithmetical components of . Only arithmetical formal numbers possess arithmetical components.

A formal number of the arithmetical set having no components which are formal numbers of the argumental set is called a pure arithmetical formal number. For example and are pure, but and are not pure.

There are many types involved in the consideration of a formal number. For example, in there is the type of and of ; in there is the type of , the type of , and the type of ; and so on for more complex formal numbers. The type of a formal number as a whole in any occurrence is called its actual type. This is the type of the entity which it then represents.

The other types involved in a formal number in any occurrence are called its subordinate types.

The actual types are not indicated in the symbolism for the various formal numbers as stated above. They can be indicated relatively to the type of the variable by writing , , (, (, (, by the notation of *65. Even when the actual type of a complex formal number, such as , is settled—so for instance that we have —the meaning of the symbol is not completely determined, for the type of remains ambiguous. It follows, however, from

*100·511.*110·23.*113·26.·62,

that the subordinate types make no difference to the value of a formal number, so long as the components are not null.

We can therefore make a formal number definite as soon as its actual type is definite by securing that its components are not null. This is done by the convention II T (below) combined with the definitions

*110·03·04.*113·04·05.*116·03·04.

When the subordinate types are adjusted in accordance with these definitions and conventions, they will be said to be normally adjusted.

But in order to state this convention we require a definition of what is here called the adequacy of the actual type of a formal number. The general idea of adequacy is simple enough, namely that, given the subordinate types of , the actual type of should be high enough to enable us logically to prove when such a proof is possible for types which are not too low. For example, all types except the lowest for which it has meaning are adequate for the constant formal number 2. It is rather difficult however to state the meaning of adequacy with precision in a manner adapted to all formal numbers. Fortunately the definition of the lowest type which corresponds to this general idea of adequacy is not important for our purposes. It will be sufficient to define as adequate some types which certainly do have the property in question.

The method of definition which we adopt is to replace the formal number by another one so related to that with the same actual type for both we can prove , whenever is not equal to in all types. If 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 has the required property. Thus:

(i) The actual types of , , , and are adequate when we can logically prove

(ii) The actual types of , , , and are adequate when we can logically prove

It will be noticed that , , and are the greatest classes of the same type as , , and respectively, and that and are the greatest cardinal numbers of the same type as and respectively. These definitions hold even when any of , , , are complex symbols.

The remaining formal numbers which are not functional must certainly be constant. The difficulty which arises here is that if be such a formal number and occurs in its symbolism, we have no logical method of deciding as to the truth or falsehood of in any type. But we replace by which is the greatest existent cardinal of the same type as in that occurrence. Thus:

(iii) If be a formal number which is not functional, an adequate actual type of is one for which we can logically prove , where is derived from by replacing any occurrence of in by . Accordingly if does not occur in , an adequate type is any actual type for which we can logically prove .

In the case of members of the primary and argumental groups we have substituted the of the appropriate type in the place of each variable. When the actual type is adequate we have

In the case of members of the arithmetical group (except in the case of , we have substituted for each argument the largest cardinal number which can be obtained in the type of that argument, namely the for the of the appropriate type. Accordingly we are sure (except in the case of 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 the actual type of is adequate, and *110·23 shows that any adequate actual type of will do. But nothing is said about the actual type of . We make the following definition: When the subordinate types of a formal number are normally adjusted, and the actual type is adequate, the types of the formal number are said to be arithmetically adjusted.

We notice that for the primary set, the arithmetical adjustment of types means the same thing as the adequate adjustment of the actual type. Also if the arguments of a formal number of the arithmetical set are simple symbols, the two ideas come to the same thing.

In the case of variable formal numbers of the primary set, it follows from *117·22·32 that when their types are arithmetically adjusted they are not equal to for any values of their variables.

Also in the case of those variable formal numbers which are of the pure arithmetical set (excluding ) it follows from *100·4·52·42.*113·23.*116·23 that, working from the ultimate components reached by successive analysis upwards, for all values of such ultimate components which are members of they can be reduced to the case of the formal numbers of the primary group; and that therefore they are not equal to when their types are arithmetically adjusted. For example in , , , , are these ultimate components; let them be existent cardinal numbers. Hence when the types are arithmetically adjusted, the actual type of is adequate and is an existent cardinal; we can therefore substitute for it. By the same reasoning we can substitute for , and again for .

A definite standard arithmetical adjustment of types for any formal number can always be found by making every use of , whether explicit or concealed in or in some other symbol, to be homogeneous. Proofs which apply to any arithmetical adjustment of types start by dealing with this standard type, and then by the use of *104·21.*106·21·211·212·213 the extension is made to the adjacent higher classical and relational types. We then "see" that by the analogy of symbolism this extension can always be formally proved at each stage, so that we are dealing with the stable truth-value. For some constant formal numbers a lower existential type can be found than that indicated by this method.

III. Classification of Occurrences of Formal Numbers.

A symbolic form of any of the kinds [cf. *117·01·04·05·06] is called an arithmetical inequality.

These forms only arise when we are comparing cardinal numbers in respect to the relation of being "greater than" or "less than." It might seem natural to include equations among these arithmetical inequalities. Their use however, even as between cardinal numbers, is not so exclusively arithmetical, and it is convenient to consider them separately under another heading during our preliminary investigations.

In the arithmetical inequalities as above written, and , or any symbols replacing and , are called the opposed sides of the inequality, and either of or is called a side of the inequality.

Symbolic forms of the kinds and , where either or is a formal number, will be called equations and inequations respectively; and and are called the opposed sides of the equation or inequation, and either of them is simply a side of the equation or inequation.

When we reach the exclusively arithmetical point of view, it will be convenient to put together equations, inequations and arithmetical inequalities as one sort of symbolic form. Their separation here is for the sake of investigations into the exceptions due to the failure of existence theorems in low types. It is unnecessary to consider arithmetical inequalities in this connection.

The ways in which a symbol can occur in a symbolic form are named as follows:

The occurrence of in is called an argumental occurrence,

The occurrence of as an argument of an arithmetical formal number (which may be a component of another formal number) or as one side of an arithmetical inequality is called an arithmetical occurrence,

The occurrence of as one side of an equation is called an equational occurrence,

The occurrence of in "" is called an attributive occurrence,

Any other occurrence of is called a logical occurrence, so also is .

It is obvious that a pair of opposed sides of an equation or inequation must be of the same type. Furthermore, if be a formal number, and *20·18 is applied so as to give the equational occurrence of must be of the same type as its occurrence in ), otherwise the inference is fallacious. Accordingly substitution in arithmetical formulae can only be undertaken when the conventions as to the relations of ambiguous types secure this identity. This question is considered later in this prefatory statement, and the result appears in the text as *118·01.

At this point some examples will be useful; they will also be referred to subsequently in connection with the conventions limiting ambiguities of type.

*100·35.

Here the formal numbers are and , each of which has three occurrences. The first occurrence of is logical, its second is equational, and its third is attributive.

*100·42 (in the demonstration).

Here and are the only formal numbers, and all their occurrences are equational.

*100·44 (in the demonstration).

Here and are the only formal numbers; the first occurrence of is logical, its second is equational; both the occurrences of are equational.

*100·511.

Here the formal numbers are and . The first occurrence of is logical, the second is argumental, the third is equational; the only occurrence of is equational.

*100·521.

Here and are the only formal numbers; has two occurrences, the first logical, the second argumental; has one occurrence, which is equational.

*101·28 (in the demonstration).

Here the formal numbers are 1 and . The first occurrence of 1 is argumental, the second is attributive; the occurrence of is attributive.

*101·38.

Here the formal numbers are 0, 1, and 2, and their occurrences are all logical.

*110·54.

Here the formal numbers are The occurrence of ) and that of ( are both equational, and they must be of the same type since they are opposed sides of the same equation. The occurrences of the other formal numbers are as arithmetical components of a more complex arithmetical formal number and are therefore arithmetical.

*116·63.

The formal numbers are , , , and (. Each formal number occurs once only. The occurrences of and are arithmetical, and those of the other two are equational.

*117·108.

The formal numbers are and , each with three occurrences. The first two occurrences of each formal number are arithmetical, the last occurrence of each is equational.

*120·53 (in the demonstration).

Here the formal numbers are , , , , . Each formal number has one occurrence. Those of , and are equational, and those of and are arithmetical.

*120·53 (in the demonstration).

Here the formal numbers are , , , , . The first occurrence of is equational, its second occurrence is logical; the first two occurrences of are equational, its third occurrence is arithmetical; the only occurrence of is arithmetical; the only occurrences of and of are equational.

IV. The Conventions and .

Two occurrences of a formal number with the same actual type are said to be bound to each other.

The choice of types for formal numbers, when they are not made definite in terms of variables by the notation of *65, is limited by the following conventions, which enable us to dispense largely with the elaboration produced by the definition of types.

. All logical occurrences of the same formal number are in the same type; argumental occurrences are bound to logical and attributive occurrences; and, if there are no argumental occurrences, equational occurrences are bound to logical occurrences.

This rule only applies, so far as meaning permits, to those types which remain ambiguous after the assignment of types to the real variables.

It will be noticed that if there are no argumental or logical occurrences of a formal number, does not in any way apply to the assignment of types to the occurrences in the form of that formal number.

The identification of types in argumental and attributive occurrences by is rendered necessary to secure the use of the equivalence where 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, directs the logical and equational occurrences of to be in the same type, and similarly for . Also "meaning" secures that the equational types of and 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 and . Thus, using the notation of *65·04 to secure typical definiteness, *100·35 is to mean

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, produces no limitation of types.

In *100·44 (demonstration), secures that the two occurrences of are in the same type. Also we notice that the first occurrence of is really (cf. *65·04) , since "" occurs, and thus "meaning" requires this relation of types, and the second occurrence of is in the type of the occurrences of .

In *100·511, directs that the logical and argumental occurrences are to have the same type. In *100·521, directs that the two occurrences of are to have the same type. In *101·28 both occurrences of 1 are to be in the same type. In *101·38, directs that all the occurrences of 2 are to have the same type.

The convention 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 has no application.

In the second example from *120·53 (in the demonstration) convention directs that the two occurrences of shall be in the same type; and the necessity of "meaning" secures that the first occurrence of shall also be in this type. The same necessity secures that shall be in the same type as ; and it also secures that in "" the first occurrence of and that of shall have a common type, which is otherwise unfettered; also nothing has been decided as to the types of and in .

We now come to conventions embodying the outcome of arithmetical ideas. The term "arithmetical" is here used to denote investigations in which the interest lies in the comparison of formal numbers in respect to equality or inequality, excluding the exceptional cases—whenever the cases are exceptional—due to the failure of existence in low types. The thorough-going arithmetical point of view, which we adopt later in the investigation on Ratio and Quantity and also in this volume in *117 and *126 and some earlier propositions, would sweep aside as uninteresting all investigation of the exact ways in which the failure of existence theorems is relevant to the truth of propositions, thus concentrating attention exclusively on stable truth-values. But the logical investigation has its own intrinsic interest among the principles of the subject. It is obvious however that it should be restrained to a consideration of the theorems of purely logical interest. In practice this extrusion of uninteresting cases of the failure of arithmetical theorems, even amid the logical investigations of the first part of this volume, is effected by securing that all arithmetical occurrences of formal numbers have their actual types adequate.

As far as formal numbers of the primary group, i.e. , , , are concerned, the arithmetical adjustment of types is secured formally in the symbolism by the definitions *110·03·04 for addition, and *113·04·05 for multiplication, and *116·03·04 for exponentiation, and *117·02·03 for arithmetical inequalities, and *119·02·03 for subtraction.

We save the symbolic elaboration which would arise from the extension of similar definitions to other formal numbers by the following convention:

. Whenever a formal number occurs, so that, if it were replaced by , the actual type of would by definition have to be adequate, then the actual type of is also to be adequate.

For example in , if were replaced by , then by *110·04 the actual type of is adequate. Hence by the actual type of is to be adequate: accordingly so long as and are simple variables and members of , we can always assume for the type of the occurrence of .

It is essential to notice that so long as the argument of an argumental formal number, or the arguments of an arithmetical formal number, are adjusted arithmetically, the exact types chosen make no difference. This follows for argumental formal numbers from *102·862·87·88, for addition from *110·25, for multiplication from *113·26, for exponentiation from *116·26, for subtraction from *119·61·62. Thus (remembering also *100·511) in any definite type a formal number has one definite meaning provided that any subordinate formal number which occurs in its symbolism is determined existentially. The convention directs us always to take this definite meaning for any pure arithmetical formal number.

The convention does not determine completely the meaning of an arithmetical formal number which is not pure. For example, is a pure arithmetical formal number when , , are determined in type; and convention directs that the type of is to be adequate. But is an arithmetical formal number which is not pure, and convention directs that the type of the domain of is to be adequate, but does not affect the type of . Thus it is easy to see that secures the adequacy of the actual types of all arithmetical components of any arithmetical formal numbers which occur, but does not affect the actual type of a formal number which occurs as the argument of an argumental formal number. But in this case convention will bind the actual type of this occurrence of the argument to any logical or attributive occurrence of the same formal number. For example, if and occur in the same form, then these two occurrences of must have the same actual type. In practice argumental formal numbers are useful as components of arithmetical formal numbers for the very purpose of avoiding the automatic adjustment of types directed by .

The meaning of is best explained by examples. Among our previous examples we need only consider those in which arithmetical formal numbers occur.

In *110·54 the convention or definitions direct us to determine the types of and adequately when forming , also to determine and adequately when forming . The convention does not apply to the types of and . These types must be identical in order to secure meaning.

In *116·63 the convention directs us to adjust the types of and adequately; it does not affect the types of and , which must be identical to secure meaning. If we replace , , by formal numbers, by 2, , and 1 for example, we get "." The convention now directs that 1 is to be determined adequately. It so happens that any type is adequate for it, since can be proved in any type. Then adequate types for and are types for which we can prove and . Thus if is the type of in both cases, an adequate type for is , and for is .

In *117·108 we find arithmetical occurrences in arithmetical inequalities. Thus directs us to take the first two occurrences of and the first two of with adequate actual types. The type of and in is not affected by it. It is evident that the conventions , 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 needs a consideration of the whole question of arithmetical substitution. Consider the first of the two examples. We have

It is obvious that unless we can pass with practical immediateness from "" to "" by *20·18, arithmetic is made practically impossible by the theory of types. But a difficulty arises from the application of . Suppose we assign the types of our real variables first. Then the types of , , , 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 . Assume that this is the case. But the equational use of is in the same type as , and by the arithmetical use of in 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 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 "," where and are formal numbers and occurs arithmetically in , we cannot infer unless the equation is arithmetical. For otherwise the in the equation cannot be identified with the in .

When we have "," where is a formal number and is a number in a definite type, and wish to pass to "," or "" and wish to pass to "," the occurrence of in being arithmetical, the type of may not be an adequate type for . Accordingly the in "" cannot be identified with the in . The type of the in the equation ought to be freed from dependence on that of . Accordingly the transition is only legitimate when we can write instead where in both cases the equation is arithmetical. For now all the symbols are subject to the same rules.

If this modification can be made without altering the truth-value of the asserted propositions, the substitution is legitimate, otherwise it is not.

It is obvious that in the above our immediate passage is to or from . But is easy to see that, the occurrence of being arithmetical, we always have In order to prove this, we have only to prove

The demonstration of the first of these propositions runs as follows:

In the above demonstration the step to (3) is legitimate since by the hypothesis is a determination of in an adequate type.

Similar proofs hold for the other propositions, using *113·204 and *116·204 and *117·12 and *103·13.

We must also consider the circumstances under which we can pass from "" to "," where the latter equation is arithmetical. In other words, using *65·01 we require the hypothesis necessary for

We have

Now in (4) the occurrences of and , which are in the same type, may be chosen to be in any type we like. Hence we deduce

Hence is the requisite condition. Now since can be in any type, we can also choose it in any existential type for . Thus with applying to the arithmetical occurrence of in , we have, where is a formal number and is a number in a definite type,

In the last proposition by the equation is arithmetical. These equations are summed up in *118·01.

These three fundamental theorems embody the principle of arithmetical substitution. The hypothesis is really less than is assumed in ordinary life, the usual tacit assumption being . In fact unless , is necessarily false.

Principle of Identification of Types. Suppose we have proved "" and "," where is a formal number whose occurrence in "" is in an entirely ambiguous type, and is the same formal number with its type related to that of by *65·01. Then since the type of the in "" is ambiguous, we can write "" and thence infer "."

The principle is: An entirely undetermined type in an asserted symbolic form can be identified with any type ambiguous or otherwise in any other asserted symbolic form or in the same symbolic form.

For example in *100·42 (demonstration) considered above, since occurs, the first occurrences of and are of the same type, and so are their second occurrences in . But the two types are not determined by our conventions to have any necessary connection. In fact the type in is entirely arbitrary. Accordingly it can be identified with the other type, and thus the inference to the next line, viz. to "," is justified.

In the case of arithmetical equations, it is important to notice that we have Hence if and are formal numbers, Thus if we have "" and "," we can infer from the former proposition "" and from this and the latter proposition, we infer "," so the general principle of identification can be employed when the in the first proposition is an arithmetical equation.

For example, in an example given above, *100·44 (demonstration), viz. the equation is arithmetical. Accordingly we are justified in asserting the propositional function where in "" has all along been presupposed by the necessity of meaning. Thus the inference follows,

This proof loses its point when is looked on as a variable with necessarily the same type throughout. For then the proposition collapses into

But if be a formal number necessarily a member of , the proposition is really

With this presupposition we should have in the first line of the demonstration though with "" a single variable, the line is formally correct as it stands in the text.

Recognition of Particular Cases. It is important to notice the conditions under which can be recognized as a particular case of , where is a real variable and is a formal number. In the first place obviously we must substitute for , wherever it occurs in , and thus obtain . Then we may find that by the application of our conventions, we can replace this by . For example we have

*100·42.

Now put for , we obtain

Now by , even when is a formal number, the identity of types of the two occurrences of is equally secured in

Thus this is a particular case of *100·42. Such deductions can be made in general without any explicit formal statement.

Ambiguity of . It follows (cf. *100·02 and *103·02) from the typical ambiguity of that is also typically ambiguous. Hence "" according to our methods of interpretation would not necessitate that and should be of the same type. We shall always interpret "" as standing for "" and therefore as not necessarily identifying the types of and . Similarly for , , and . For example

*110·402.

Here the and need not be of the same type. Again

*110·41.

Here the identification of the types of and requires the hypothesis "."

VI. Conventions and .

General Arithmetical Convention. Conventions and are always applied, but the following convention is not used at first. This convention limits the remaining ambiguity of type by sweeping away the exceptional cases in low types, due to the failure of existence theorems. The convention will be cited as .

. All equations involving pure arithmetical formal numbers are to be arithmetical.

We have seen that from an arithmetical equation the analogous equation in any other type can be deduced. Thus with all equations between formal numbers are so determined in type that their truth in "any type" is deducible. Thus in the few early propositions where is introduced, the fact is noted by stating that the equations hold "in any type." These propositions are *103·16, *110·71·72.

The effect of applying to other propositions in *100 is to render some of the hypotheses (usually logical forms affirming existence) unnecessary, but also materially to limit the scope of the propositions. Take for example

*100·35.

If we apply to this, we can write

For the equational occurrences of and are by and to be with adequate actual types. But if is a small class in a high type, an adequate actual type for will be a high type, whereas may hold in a low type. Thus with , for the sake of simplicity we abandon the statement of the minimum of hypothesis necessary for our propositions. The enunciation of no other proposition in *100 is affected.

The enunciation of no proposition in *101 is affected by , though it would unduly limit the scope of *101·34. In *110, would unduly limit the scope of such propositions as

*110·22·23·24·25·251·252·3·31·32·331·34·35·351·44·51·54

and of many others, without altering their enunciations. There is no proposition in *110 whose enunciation it would alter. is already applied to *110·71·72; if is removed from these propositions, then must be added as an hypothesis to both of them. The effect of on *113 and *116 is entirely analogous to that on *110; in neither of these two numbers is there any proposition to which is applied in the text.

As regards *117, is applied throughout, so that the propositions are all in the form suitable for subsequent investigations in which the interest is purely arithmetical. It is important however to analyse the effect of AT on the enunciations for the sake of logical investigations, especially in connection with *120. First, can only affect propositions in which equations or inequations occur, and among such propositions it does not affect the enunciations of those in which both sides of the equations are not formal numbers, so that the equations are not arithmetical after the application of AT. These propositions are *117·104·14·24·241·243·31·551. These propositions, which are characterized by the presence of a single letter on one side of any equation involved, can be recognized at a glance. The propositions involving arithmetical equations whose enunciations are unaltered by the removal of are *117·21·54·592. Propositions involving inequations whose enunciations are unaltered by the removal of are *117·26·27. Finally the only propositions of *117 whose enunciations are altered by the removal of are *117·108·211·23·25.

In *118 and *119 is not used.

In *120, which is devoted to those properties of inductive cardinals which are of logical interest, is never used. None of the propositions *117·108·211·23·25·3 are cited in it, except *117·25 in the demonstration of *120·435 for a use where is not relevant. The application of AT to *120 would simplify the hypotheses of *120·31·41·451·53·55, and limit the scopes of the propositions.

One other convention, which we will call "," is required in certain propositions where the hypothesis implies that there are types in which every inductive cardinal exists, i.e. in which is not an inductive class. Among such hypotheses are , , (or typically definite forms of these hypotheses), or or . When such hypotheses occur, we shall assume that induct is, whenever significance permits, to be determined in a type in which every inductive cardinal exists, i.e. in which the axiom of infinity holds (cf. *120·03·04). The statement of this convention is as follows:

. When the hypothesis of a proposition implies that there is a type in which every inductive cardinal exists, every occurrence of "" in this proposition is to be taken (if conditions of significance permit) in a sufficiently high type to insure the existence of every inductive cardinal.

It is to be observed that this convention would be unnecessary if we confined ourselves to one extensional hierarchy, for in any one such hierarchy all types are inductive or all are non-inductive, so that if every inductive cardinal exists in one type in the hierarchy, the same holds for any other type in the hierarchy. But when we no longer confine ourselves to one extensional hierarchy, this result may not follow. For example, it may be the case that the number of individuals is inductive, but the number of predicative functions of individuals is not inductive; at any rate, no logical reason can be given against this possibility, which can only be rejected on empirical grounds, if at all.

The way in which this convention is used may be illustrated by the demonstration of *122·33. In the second line of this demonstration, we show that the hypothesis implies It will be seen that these definitions do not suffice to determine the type of . Hence in (1), the on the left may not be of the same type as the on the right. Now the use of *122·473, which occurs in the next line of the demonstration of *122·33, requires that the on the left and the on the right should be of the same type. This requires that the should not be taken in a type in which we have . Hence in order to apply *120·473, we must choose a type in which all inductive cardinals exist. Since "" occurs in the hypothesis, we know that all inductive cardinals exist in the type of . But it is unnecessary to restrict ourselves to the type of , since any other type in which all inductive cardinals exist will equally secure the validity of the demonstration. Thus the convention secures the restriction required, and no more.

The convention is often relevant when "" without any typical determination occurs in the hypothesis. Whenever this is the case, if "" occurs in the proposition in a way which leaves its type undetermined so far as conditions of significance are concerned, it is to be taken in a type in which all its members exist.

VII. Final Working Rule in Arithmetic.

It is now (whenever is used, together with when necessary) possible finally to sweep aside all consideration of types in connection with inductive numbers. For by combining *126·121 *126·122 and *120·4232·4622, we see that it is always possible to take the type high enough so that no definitely determined inductive number shall be null (, and that all the inductive reasoning can take place within this type. Furthermore we have already seen that the arithmetical operations are independent of the types of the components, so long as they are existential. Thus, as far as the ordinary arithmetic of finite numbers is concerned, all the conventions (including AT), and the necessity for hypotheses as to the existence of inductive numbers, are finally superseded by the following single rule:

Rule of Indefinite Numbers. The type assigned to any symbol which represents an inductive number is such that the symbol is not equal to .

We make the definition

*126·01.

Wherever this symbol "" for the class of "indefinite inductive cardinal numbers" is used, the above rule is adhered to. In other words, "" can always be replaced by "," where is a homogeneous or ascending cardinal, and is the appropriate constant, or is a variable, as the case may be. In the latter case, a symbolic form such as can be replaced by

Furthermore by *120·4622 it follows that with this rule the result of proceeding by induction in one type and then transforming to another type is the same as that of proceeding by induction in the latter type. Thus for example there is no advantage to be gained by discriminating between and ; for , , , , , , and , and so on.

Hence all discrimination of the types of indefinite inductive numbers may be dropped; and the types are entirely indefinite and irrelevant.

FOOTNOTES: