Volume 1 / Part 3 — *119. SUBTRACTION.
Reading edition
*119. SUBTRACTION.
Summary of *119.
The treatment of subtraction follows the same general lines as that of addition, and is simplified by the results in *110. A difficulty arises from the fact that subtraction (in any ordinary sense of the term) is not always possible; and also from the fact that the result, when possible, is not always a cardinal number.
We put
*119·01.
Thus when subtraction (in the ordinary sense of the term) is not possible,
The question of existential adjustment of types is dealt with by of the prefatory statement combined with the following definitions:
*119·02.
*119·03.
We then proceed to deduce the elementary properties derivable from these definitions.
*119·11.
*119·12
*119·14.
*119·25.
*119·26.
The next group of propositions is concerned with some simple results of subtraction.
*119·32.
*119·34.
*119·35.
Associative laws are then considered.
*119·44.
*119·45.
The question of types is then dealt with:
*119·52.
A difficulty arises from the fact that if and are two complete types whose members are classes, we cannot prove that, either or . We put
*119·54.
Then we obtain
*119·541.
Finally we show that any existential adjustment of types will suffice for the components:
*119·61.
*119·62.
Also *119·25·26 are now extended to
*119·64.
The only applications of the propositions of this number are in connection with Inductive Cardinals (cf. *120).
*119·01.
Here the suffix to the sign of subtraction is introduced to show that we are concerned with cardinal subtraction. It will be found that is not an except under hypotheses for and .
*119·02.
*119·03.
*119·04.
Note that the occurrence of a formal number in the place of or in is an arithmetic occurrence, and accordingly applies to it.
*119·1.
*119·101.
*119·102.
*119·103.
*119·11.
*119·12.
Dem.
Thus is an when is an .
*119·13.
Dem.
*119·14.
*119·21.
The notation is defined in *65·01.
Dem.
*119·22.
Dem.
*119·23.
Dem.
*119·24.
*119·25.
Dem.
*119·26.
Dem.
*119·27.
For the extension of this theorem cf. *119·64.
*119·31.
Dem.
The penultimate step in the proof employs the principle, explained in the prefatory statement, that, since in the previous line the equation has its sides undetermined in type by the conventions and , any convenient type can be chosen for them. The type chosen in this line is such that , and the references indicate the existence of at least one such type.
*119·32.
*119·33.
Dem.
*119·34.
*119·35.
Dem.
*119·41.
Dem.
*119·42.
Dem.
Note that if be an infinite class, it does not follow from that . This will be proved, however, when is an inductive class (cf. *120·41).
*119·43.
Dem.
*119·44.
Dem.
*119·45.
*119·51.
Dem.
*119·52.
The difficulty in respect to types, which arises from the fact that and have not been proved to be identical, does not exist when is an "inductive number"; cf. *120·413.
*119·53.
*119·531.
Dem.
*119·532.
Dem.
*119·54.
*119·541.
*119·61.
Dem.
*119·62.
Dem.
*119·63.
Dem.
*119·64.
Dem.