**Description: **Define the class of
natural numbers, which are all ordinal numbers that
are less than every limit ordinal, i.e., all finite ordinals. Our
definition is a variant of the Definition of N of [BellMachover] p. 471.
See dfom2 7575 for an alternate definition. Later, when we
assume the
Axiom of Infinity, we show ω is a set in
omex 9100, and ω can
then be defined per dfom3 9104 (the smallest inductive set) and dfom4 9106.
*Note*: the natural numbers ω are a
subset of the ordinal numbers
df-on 6194. They are completely different from the
natural numbers ℕ
(df-nn 11633) that are a subset of the complex numbers
defined much later
in our development, although the two sets have analogous properties and
operations defined on them. (Contributed by NM,
15-May-1994.) |