Question:
Who did derive the division by zero 1/0 and the division by zero calculus
$\tan(\pi/2)=0, \log 0=0$ as the outputs of a computer?
Facts:
On February 16, 2019 Professor H. Okumura introduced the surprising news in
Research Gate:
José Manuel Rodríguez Caballero\\
Added an answer\\
In the proof assistant Isabelle/HOL we have $x/0 = 0$ for each number $x$.
This is advantageous in order to simplify the proofs. You can download this
proof assistant here: {\bf https://isabelle.in.tum.de/}.
J.M.R. Caballero kindly showed surprisingly several examples by the system
that
$$
\tan \frac{\pi}{2} =0,
$$
$$
\log 0 =0,
$$
$$
\exp \frac{1}{x} (x=0) =1,
$$
and others. Precisely:
Dear Saitoh,
In Isabelle/HOL, we can define and redefine every function in different
ways. So, logarithm of zero depend upon our definition. The best definition
is the one which simplify the proofs the most. According to the experts,
z/0 = 0 is the best definition for division by zero.
$$
\tan(\pi/2) = 0
$$
$$
\log 0 =
$$
is undefined (but we can redefine it as $0$)
$$
e ^0 = 1
$$
(but we can redefine it as $0$)
$$
0^0= 1
$$
(but we can redefine it as $0$).
In the attached file you will find some versions of logarithms and
exponentials satisfying different properties. This file can be opened with
the software Isabelle/HOL from this webpage: https://isabelle.in.tum.de/
Kind Regards,
José M.
(2017.2.17.11:09).
2019.3.6.6:17
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
