[FOM] 820: Sugared ZFC Formalization/2

[José Manuel Rodriguez Caballero]

As a kind of ordinary mathematician, I have no problem accepting that 1
divided by 0 is 0, i.e., value "(1::real)/(0::real) = (0::real)" in
Isabelle. Indeed, everything depends upon the topological interpretation of
the "real numbers" that we are using:

   - 1/0 is undefined if we are conceiving the real numbers as a line;
   - 1/0 is infinity if we are conceiving the real numbers as a circle;
   - 1/0 is 0 if we are conceiving the real numbers as the lemniscate of
   Bernoulli (identifying zero and infinity).

>From a local point of view, real numbers are like a segment (with the
exception of the singularity at zero in the case of the lemniscate of
Bernoulli), but from a global point of view "only God knows", because no
human being has never seen the real numbers as a whole. So, I'm open to the
three above-mentioned possibilities. I think that to consider that the
"real numbers" are by definition a line is a kind of Cartesian dogmatism.
In the case 1/0 = 0, a small neighbourhood of zero includes both very small
numbers and very large numbers, e.g., ice-cream has a bad taste either when
it has almost no sugar or it has too much sugar. A similar idea holds in
hight dimension, e.g., complex numbers, quaternions, octonions, etc.

Kind Regards,
José M.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180619/93b63d9d/attachment.html>