[FOM] Adventures in Formalization 6
Paul Blain Levy
P.B.Levy at cs.bham.ac.uk
Wed Oct 14 18:15:27 EDT 2015
>> > 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.
More information about the FOM
mailing list