Email Gateway (Aug 22 2022 at 17:39): Email Gateway (Aug 22 2022 at 17:39):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
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.
Email Gateway (Aug 22 2022 at 17:40):From: Slawomir Kolodynski via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
(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)
Last updated: Apr 24 2024 at 12:33 UTC