[FOM] 622: Adventures in Formalization 6

[Freek Wiedijk]

Dear Larry,

>And then what is the status of the “real” natural
>numbers, which are surely present somewhere unless they are
>actually constructed to be a subset of the complex numbers,
>which would be even stranger?

It's different.  When defining, say, the integers from the
natural numbers nat, then one first defines the integers as
a set int' (for instance as a quotient of nat x nat), with
an embedding i: nat -> int'.  And then the integers int that
the rest of the library actually uses everywhere are then
defined as int := nat U (int' - i[nat]).  And similarly for
the other number types.  So, yes, the "real" natural numbers
(the finite Von Neumann ordinals, of course!) are a subset
of the complex numbers.  And a subset of the ordinal numbers.
And a subset of the extended reals.

Henk Barendregt once told me that Van der Waerden describes
exactly this same construction in one of his books.

Freek