Volume 1 / Part 3 — *125. THE AXIOM OF INFINITY.
Reading edition
*125. THE AXIOM OF INFINITY.
Summary of *125.
The present number is merely concerned to give a few equivalent forms of the axiom of infinity, and of the kindred assumption of the existence of .
In virtue of *125·24·25 below, if the axiom of infinity holds in any one type, then it holds in any other type which can be derived from this one, or from any type from which this one can be derived. Hence if we assume, as it seems natural to do, that all extensional types are derived from a first type, namely that of individuals, then the axiom of infinity in any such type is equivalent to the assumption that the number of individuals is not inductive.
We deal, in this number, first with equivalent forms of , then with equivalent forms of , then with equivalent forms of or . When "" or "" occurs in this number without typical definition, it and all other typically ambiguous symbols are to be taken in the lowest logically possible types, or with the same relative types as if this had been done. The propositions of this number are often not referred to in the sequel, but are here collected together on account of their intrinsic interest.
*125·1.
*125·11.
*125·12.
Dem.
*125·13.
*125·14.
Dem.
*125·15.
Dem.
*125·16.
Dem.
*125·2.
*125·21.
Dem.
*125·22.
*125·23.
*125·24.
Dem.
*125·25.
*125·3.
Dem.
*125·31.
*125·32.
Dem.
*125·33.
Dem.
*125·34.
Dem.
*125·35.
Dem.
*125·36.
Dem.