# Re: [isabelle] [FOM] 820: Sugared ZFC Formalization/2

```> (1::real)/(0::real) = (0::real)" in Isabelle
Isabelle I believe has no opinion about it. It is true in Isabelle/HOL though.
In Isabelle/ZF one can argue that 1/0 is the empty set.  This is because if x is not in the domain of a function f then f(x) is the empty set. There is a short discussion of that at the end of http://isarmathlib.org/Field_ZF.html .The situation is similar in Metamath  (see http://us.metamath.org/mpegif/ndmfv.html) so I would say this is quite standard in ZFC formalizations.

Kind regards
Slawomir Kolodynski
http://savannah.nongnu.org/projects/isarmathlib Library of Formalized Mathematics for Isabelle/Isar (ZF Logic)

On Tuesday, June 19, 2018, 11:02:05 PM GMT+2, José Manuel Rodriguez Caballero <josephcmac at gmail.com> wrote:

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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.