[FOM] 622: Adventures in Formalization 6

[Larry Paulson]

Dear Freek,

This approach is certainly original, but I would be surprised if it appealed to many mathematicians. It seems that the set of complex numbers under this scheme would be the union of five disjoint sets: the natural numbers, the negative integers, the non-integral rationals, the irrational numbers, and the complex numbers with a nonzero imaginary part. Only in the last case would a complex number consist of a pair of real numbers, and this would split into a further 16 cases. No doubt one could restore sanity with the help of a function that undoes this construction, but that surely defeats the point of constructing this set in the first place.

This is why it will not be easy to replace the use of natural language in mathematics. If I choose a natural number N > 0 and later refer to the real number e/N, nobody cares whether N was actually an ordinal or the image of an ordinal as a real number, but in formalised mathematics it does matter. Fortunately, with the right automation, it doesn’t actually make a very big difference.

Larry Paulson


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