[isabelle] 1/0=0

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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.