Email Gateway (Aug 22 2022 at 17:40): Email Gateway (Aug 22 2022 at 17:40):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
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.
Last updated: Apr 27 2024 at 01:05 UTC