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