Re: [isabelle] 1/0=0
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.
> 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
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and