*To*: Cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] [FOM] 820: Sugared ZFC Formalization/2*From*: Slawomir Kolodynski via Cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*Date*: Wed, 20 Jun 2018 07:15:34 +0000 (UTC)*In-reply-to*: <CAA8xVUjf5p3HszMP+AYecwTPwy9fddd_w0shZVbWVQOQYTyi6A@mail.gmail.com>*References*: <CAA8xVUjf5p3HszMP+AYecwTPwy9fddd_w0shZVbWVQOQYTyi6A@mail.gmail.com>*Reply-to*: Slawomir Kolodynski <skokodyn at yahoo.com>

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

**References**:**Re: [isabelle] [FOM] 820: Sugared ZFC Formalization/2***From:*José Manuel Rodriguez Caballero

- Previous by Date: Re: [isabelle] [FOM] 820: Sugared ZFC Formalization/2
- Next by Date: Re: [isabelle] make_string
- Previous by Thread: Re: [isabelle] [FOM] 820: Sugared ZFC Formalization/2
- Next by Thread: [isabelle] datatype_compat in Isabelle2018-RC0
- Cl-isabelle-users June 2018 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list