[FOM] 622: Adventures in Formalization 6
Adam Naumowicz
adamn at math.uwb.edu.pl
Tue Oct 13 03:11:59 EDT 2015
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
More information about the FOM
mailing list