[FOM] 622: Adventures in Formalization 6

[Adam Naumowicz]

On Mon, 12 Oct 2015, Larry Paulson wrote:

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

I would also be surprised if the "gory details" of the construction 
appealed that much to mathematicians. However, I really doubt if 
mathematicians are indeed interested in treating a complex number as an 
actual pair of reals, but rather to be able to consider its real and 
imaginary part that enjoy all the natural properties. The definition of an 
ordered pair is an even simpler example here: we know that it can be 
constructed in a number of ways (using the definition of Kuratowski, 
Wiener, Hausdorff or some other variants), but this is of interest to 
those working in set-theory only, while the rest of mathematicians use the 
pairs a lot, but hardly ever have the need to bother themselves with how 
the pairs are constructed.

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

Andrzej Trybuec used to call this construction as "encapsulation", to 
resemble the technique that works well in objective programming. In the 
Mizar library this works very well, there are hardly any further 
developments that actually require the 'low level' structure of complex 
numbers once the formalizer is given access to all their expected 
properties.

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

As Freek has pointed out, the right type system could take care of that, 
so even in formalized mathematics it can make a very little difference 
and still eliminate the ambiguity of the natural language.

Adam Naumowicz

===========================================================================
Dept. of Programming and Formal Methods      Fax: +48(85)738-83-33
Institute of Informatics                     Tel: +48(85)738-83-06 (office)
University of Bialystok                      E-mail: adamn at mizar.org
Ciolkowskiego 1M, 15-245 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
===========================================================================


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

_______________________________________________
FOM mailing list
FOM at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/fom