[FOM] Adventures in Formalization 6

[Paul Blain Levy]

>> > On 8 Oct 2015, at 13:05, Freek Wiedijk <freek at cs.ru.nl> wrote:
>> >
>> > 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]).

It must be stressed that this relies on int' - i[nat] being disjoint 
from nat, which depends on the particular implementation of int' and 
nat.  Evidently an equivalence class of Kuratowski pairs of von Neumann 
naturals can't also be a von Neumann natural, as the former is infinite 
and the latter finite, but it's hardly appealing to have to rely on such 
"accidents".

Paul

>> > 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.