Volume 1 / Part 3 — *126. ON TYPICALLY INDEFINITE INDUCTIVE CARDINALS.

*126. ON TYPICALLY INDEFINITE INDUCTIVE CARDINALS.

Recapitulation of Conventions and Summary of *126.

We have now arrived at the stage where we can adopt the standpoint of ordinary arithmetic, and can for the future in arithmetical operations with cardinals ignore differences of type. In order to understand how this is so, it will be necessary briefly to recall the line of thought of some of the previous numbers and the conventions upon which the symbolism is based.

The symbolism of *102, though perfectly precise as to the typical relations of the various symbols, is in fact too complex for use, except in cases of absolute necessity. It is better to use the typically ambiguous symbols and , combined with some simple rules of interpretation of the symbolism, so as to secure that the various occurrences of the same symbols are in their proper relationships of type. This is the course followed in *100, *101, and in every number from *110 onwards.

The important symbols which involve an explicit or implicit use of or are called 'formal numbers,' and it is only necessary to make the rules of interpretation apply to them.

A constant formal number is any symbol representing a typically ambiguous constant such that there is a constant such that, however the ambiguities of type may be determined, the former constant is identical with . The variable formal numbers are defined by enumeration. They are divided into three Sets, the Primary Set, the Argumental Set, and the Arithmetical Set.

The Primary Set consists of , , , where is a variable of any type and is a variable of any type. Also and may themselves be complex symbols which in some way involve variables.

The Argumental Set has only one member , where is a variable of any type. In its capacity of a formal number is only interesting when is an ; then gives the corresponding in another type, provided that is not . Also may be a complex symbol which in some way involves a variable, e.g. is a formal number of the Argumental Set: is called the argument of .

The Arithmetical Set consists of , , , . These formal numbers are only interesting when and are also members of . Also and may be complex symbols, so long as one of them at least involves a variable. For example is a formal number, and so is .

The Primary and Argumental and Arithmetical Sets of Formal Numbers are derived from the corresponding sets of variable formal numbers, by adding to them the constant formal numbers obtained by substituting constants for the variables occurring in the expressions for the members of the variable set in question.

In the formal numbers of the arithmetical set as written above, and are called the first components. Thus every formal number of this set has two first components. The first components (if any) of the first components are also called components of the original formal number, and so on; so that components of components are components of the original symbol.

A formal number of the arithmetical set, whose components are all formal numbers, either constant or variable but not belonging to the argumental set, is called a pure arithmetical formal number. These are the formal numbers which it is important in arithmetic to secure from assuming the value owing to lowness of type.

The logical investigation of *100 and *101, where typically ambiguous formal numbers are used, is directly concerned in investigating the premisses necessary to secure various propositions from fluctuating truth-values owing to the intrusion of null-values among the cardinals. The convention, necessary to avoid determinations of type which we never wish to consider, is as follows, where the terms used are explained fully in the prefatory statement:

. 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 after the assignment of types to the real variables.

In *110, *113, *116, *119 we consider the arithmetical operations of addition, multiplication, exponentiation, and subtraction. Also in *117 we consider the comparison of cardinal numbers in respect to the relation of greater and less.

There is no interest in complicating our theorems by allowing for the cases when a pure arithmetical formal number, whose components are ambiguous as to type, becomes equal to owing to the low type of one of its components. Also in the theory of greater and less the possibility of null-values in low types has no real interest. Accordingly these are excluded from any consideration by the definitions

*110·03·04, *113·04·05, *116·03*116·04, *117·02·03,

as far as members of the primary set of formal numbers are concerned; and for other formal numbers by the following convention:

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

When is a pure arithmetical formal number, this convention secures that the type of every component is adequate.

But in arithmetic we also wish to avoid the intrusion of null-values into the consideration of equations, so far as this avoidance can be attained by the use of high types. Accordingly when we are concerned with the purely arithmetical point of view, we add also the following definition and convention ().

Definition. An arithmetical equation is an equation between pure arithmetical formal numbers whose dominant types are both determined adequately.

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

This convention is used in *117 and in some earlier propositions which are noted in the prefatory statement.

Its effect is to render the statement of hypotheses often unnecessary. Examples of its application to the numbers where it is not used in the symbolism are also considered in the prefatory statement.

In the case of the inductive numbers we cannot logically prove, apart from , that one type exists which is adequate for all the formal numbers 0, 1, 2, 3, etc. But we can prove that for any particular inductive number, say 521, a type exists for which 521 is not equal to . Accordingly for a given symbolic form, in which the symbolism necessarily has only finite complexity, when the types of variables which by hypothesis represent inductive classes or inductive numbers, not , have been settled, it is always possible to fix on a type which will be adequate for all the pure arithmetical formal numbers produced by the symbolism of the form, and also at the same time (and here the peculiar properties of inductive numbers come in) to have chosen the original types of the variables so that any of the variables can assume the value of any assigned constant inductive number, say 521, without being null.

The result is that we may assume that the symbols representing inductive numbers are never null, and thereby obtain the stable truth-values of propositions about them.

Accordingly we proceed as follows: we put

*126·01. .

We make the rule that when appears, convention is always applied. The result is that when a formal number is an we need never think about its type, and accordingly all the conventions vanish from the mind, as far as pure arithmetical indefinite inductive cardinals are concerned. We supersede all other conventions by the single one that, if it has been proved or assumed that a formal number represents an inductive cardinal, the types are so arranged that that formal number is not equal to . The proofs of propositions in this number consist largely of the production of a definite type in which this result is attained.

The important propositions are

*126·12.

*126·121.

*126·13·14·15.

*126·141.

*126·151.

Also *126·4·42·43 give the fundamental propositions for subtraction, division, and "inverse exponentiation"; and *126·5·51·52·53 the fundamental propositions for the relations of greater and less.

*126·01.

Whenever the symbol is used the Rule of Indefinite Numbers is adhered to, so that all consideration of distinctions in type among inductive cardinals can be laid aside (cf. Prefatory Statement and also the Summary of this number).

*126·011.

*126·1.

Dem.

*126·101.

*126·11.

*126·12.

Dem.

*126·121.

This proposition, taken in connection with *120·4232, embodies the convention named the Rule of Indefinite Numbers and its justification. The convention is that 1, 2, 3, ... are always in future to be used in existential types. In other words whenever any particular inductive number is employed, it is determined in a type in which it is not . The justification is that by *126·11·12 such a type can always be found for each particular inductive number.

The convention is also applied to arithmetical formal numbers in *126·13·14·15.

For all arithmetical and equational occurrences this convention is really the outcome of , , and .

*126·13.

*126·14.

*126·141.

*126·15.

*126·151.

*126·23.

Dem.

*126·31.

Note that the specification of the type of is omitted in accordance with the convention. The reference to *126·12 shows that it is always possible to apply the convention.

*126·32.

*126·33.

*126·4.

*126·41.

*126·42.

*126·43.

*126·5.

Dem.

*126·51.

The proof proceeds as in *126·5.

*126·52.

*126·53.