*To*: José Manuel Rodriguez Caballero <josephcmac at gmail.com>*Subject*: Re: [isabelle] 1/0=0*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Thu, 21 Jun 2018 12:35:59 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAA8xVUgbV1+ApLVZEQSwEQbhLeJhwCZB879z6sTzhR53nJf=Nw@mail.gmail.com>*References*: <CAA8xVUgbV1+ApLVZEQSwEQbhLeJhwCZB879z6sTzhR53nJf=Nw@mail.gmail.com>

Extending the domain of division with x/0 = 0 (and also for integers) is a common choice in a great many systems, not just Isabelle/HOL but HOL Light, HOL4, MetiTarski and doubtless many other systems. They do it simply for convenience and not for any deep reason. The point is that many laws involving division will then hold unconditionally, an example being (a*b)/(c*d) = (a/c)*(b/d). Another example of domain extension is that the finite sum operator yields 0 if given an infinite index set. (This has nothing to do with the sum of an infinite series, which is a limit.) Again there is no deep reason, it is simply that some simple identities involving finite summation can be proved without requiring the index set to be finite. The technique of extending the domains of functions to simplify theorem proving goes back at least to the 1970s and the Boyer/Moore prover. Larry Paulson > On 20 Jun 2018, at 22:52, José Manuel Rodriguez Caballero <josephcmac at gmail.com> wrote: > >> >> Slawomir said >>> (1::real)/(0::real) = (0::real)" in Isabelle >> Isabelle I believe has no opinion about it. It is true in Isabelle/HOL >> though. > > > If this is true in some sense, I guess that it can be claimed that the > "natural" topology of the "real numbers" in Isabelle/HOL is the lemniscate > of Bernoulli in place of the traditional straight line. Of course, with > this lemniscate of Bernoulli you can simulate the real line, just ignoring > the issue with 1/0, but as Voevodsky pointed out, there are several > connections between topology and type theory. Sometimes the "defects" of a > type system are just indicators of a deep topological meaning, but more > research is needed before to reach a conclusion. For a traditional > mathematician, continuity is the best criterion to justify a definition: > "nature doesn't jump"as Leibniz said. If 1/0 = 0, then a mathematician > could imagine that as a result the limit of a continuous process. > José M.

**References**:**[isabelle] 1/0=0***From:*José Manuel Rodriguez Caballero

- Previous by Date: Re: [isabelle] Isabelle2018-RC0: missing documentation for ISABELLE_TOOL_JAVA_OPTIONS
- Next by Date: Re: [isabelle] Coinduction on predicate defined wrt other coinductive predicates
- Previous by Thread: [isabelle] 1/0=0
- Next by Thread: [isabelle] On random variables, dependencies and their expectations
- 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