[FOM] 622: Adventures in Formalization 6

[Arnon Avron]

Dear Larry,

Without entering the question what is the best approach, 
I would like to point out that the approach described by Freek 
is anything but original. In fact, this is how I was taught
when I was a first-year student, and how the real
numbers are defined in e.g. the first chapter of the classic 
book of FIKHTENGOL'TS "The fundamentals of Mathematical Analysis", 
which at least  at that time (45 years ago...)
was considered to be the best textbook on Analysis (it is 
a two-volumes shortened English translation of the original
3-volumes Russian textbook).

Arnon Avron


On Mon, Oct 12, 2015 at 03:31:41PM +0100, Larry Paulson wrote:
> 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.
> 
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom