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 .The situation is similar in Metamath  (see so I would say this is quite standard in ZFC formalizations.

Kind regards
Slawomir Kolodynski 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> 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.