[isabelle] 1/0 = 0

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

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

as the limit case of

 (a*b)/(c*d) = (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
+ (y-2)^2 = 1, (x+1)^2 + (y-2)^2 = 1 (the topological lemniscate) to the
x-axis if and only if we assume that 1/0 = 0. Otherwise, g(f(p,q)) will
have a singularity at (0,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
José M.

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