[FOM] 622: Adventures in Formalization 6

Freek Wiedijk freek at cs.ru.nl
Thu Oct 8 08:05:26 EDT 2015

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.


More information about the FOM mailing list