Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] 1/0 = 0


view this post on Zulip Email Gateway (Aug 22 2022 at 17:24):

From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
My interpretation of 1/0=0 as the conception of real numbers as a lemniscate
is just a topological (alternative) explanation of the logical fact that many
laws involving division hold unconditionally, e.g., adding infinity to the
real line (Alexandroff compactification) and gluing 0 with infinity, we can
deduce the law

(ab)/(0d) = (a/0)(b/d) (i.e. 0 = 0(b/d) and infinity = infinity * (b/d))

as the limit case of

(ab)/(cd) = (a/c)*(b/d).

when c goes to zero (= infinity). Indeed, to any point (p,q), except (0,2),
on the union of the following two tangent circles (from a topological point
of view this is a lemniscate)

(x-1)^2 + (y-2)^2 = 1, (x+1)^2 + (y-2)^2 = 1

we can associate a unique point f(p,q) defined as the intersection between
the circle x^2 + (y-2)^2 = 4 and the ray from (0,2) to (p,q). Let g(u,v) be
the stereographic projection projection from x^2 + (y-2)^2 = 4 to the
x-axis, considering (0, 4) as its north pole. Then, the composition
g(f(p,q)) is a homeomorphism from the union of the two small circles (x-1)^2

Even if 1/0 = 0 was introduced in some proof assistants without deep
reasons, a posteriori it could be useful when considering mathematical
models where large numbers are like small numbers in some sense (large and
small with respect to absolute value). So, it induces a genuine
mathematical intuition motivated despite its origin as just a formal
simplification.
José M.


Last updated: Mar 28 2024 at 08:18 UTC