Isabelle/HOL and Division by zero:
Dear the related persons: Professor Larry Paulson kindly stated in his e-mail to me that: The idea that x/0 = 0 is only a convention. It does not change mathematics in any significant way and it does not lead to contradictions either. On 2017/07/04 0:2 Jose kindly introduced the relation of Isabelle/HOL and Division by zero, in details: Thank you for the book. Attached to this email you will find the discussion between Prof. Lawrence Paulson (*https://www.cl.cam.ac.uk/~lp15/* <#m_-7616739960837325088_search/isabelle/_blank>) and Prof. Harvey Friedman (*https://math.osu.edu/people/friedman.8* <#m_-7616739960837325088_search/isabelle/_blank>) concerning the division by zero. I understand Isabelle/HOL derived the result 1/0=0 about 40 years ago, however, nobody did not understand its importance over the system, for this essence, please look the survey draft: *viXra:1908.0100* <http://vixra.org/abs/1908.0100> submitted on 2019-08-06 20:03:01, (922 unique-IP downloads) Fundamental of Mathematics; Division by Zero Calculus and a New Axiom I have the general questions: 1) The definition and motievation of 1/0=0 by Isabelle. 2) Why is it conventional? I think for the division by zero, the definition is very essential and important, because in the usual definition we have a contradiction, immediately. I feel that Isabelle/HOL creates many new worlds. With best regards, Sincerely yours, Saburou Saitoh 2019.12.05.10:36
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
