Isabelle/HOL is a logic of total functions, so there is no built-in notion of a fraction or any other function application being undefined. That is, a / b is defined for all a and b, and it returns their quotient except when b is zero. But then it still has a value.
In the library, the decision was made to complete the function in such a way that x / 0 = 0. This decision simplifies many proofs, since you have to deal with less side conditions. Unfortunately it also sometimes confuses people who expect something else.
This book has been written primarily to serve as a textbook for a first course in modern logic.
No background in mathematics or philosophy is supposed.
330 ページ
ちょっと見ですが、pp. 166-168 あたりで z/0=0 を述べています。
The most famous figure in human history, according to the ranking of the Massachusetts Institute of Technology, is Aristotle. (MIT) collected and analyzed data on history and culture around the planet from 4,000 BC. until 2010.
There are six people from Greece in the top ten. pic.twitter.com/G8ehuUkpat
The most famous figure in human history, according to the ranking of the Massachusetts Institute of Technology, is Aristotle. (MIT) collected and analyzed data on history and culture around the planet from 4,000 BC. until 2010.
There are six people from Greece in the top ten. pic.twitter.com/G8ehuUkpat
However, it has been denied since Aristotle (384 BC-322 BC), including the mistake of genius Euler, and does not include division by zero, which is said to have been a concern for Einstein's life. A regrettable math. The four arithmetic operations were incomplete. Therefore, the following formula should be the equation following 17.
1/0 = 0/0 = 0,
tan (\ pi / 2) = 0,
log 0 = 0,
(f (x) / x) (0) = f ^ \ prime (0) = f ’(0)
2022.2.8.06:00
The Institute of Reproducing Kernels is dealing with the theory of division by zero calculus and declares that the division by zero was discovered as $0/0=1/0=z/0=0$ in a natural sense on 2014.2.2. The result shows a new basic idea on the universe and space since Aristotele (BC384 - BC322) and Euclid (BC 3 Century - ), and the division by zero is since Brahmagupta (598 - 668 ?).
Announcement 478: Who did derive first 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?
2015/03/26 —The short answer is: yes, it is absolutely safe. When we say that division by zero is not well-defined, what we actually mean is that zero ...
In proof assistants[edit]
Many proof assistants, such as Coq and Lean, define 1/0 = 0. This is due to the requirement that all functions are total. Such a definition does not create contradictions, as further manipulations (such as cancelling out) still require that the divisor is non-zero.[33][34]
Tanter, Éric; Tabareau, Nicolas (2015), "Gradual certified programming in coq", DLS 2015: Proceedings of the 11th Symposium on Dynamic Languages, Association for Computing Machinery, arXiv:1506.04205, doi:10.1145/2816707.2816710, The standard division function on natural numbers in Coq, div, is total and pure, but incorrect: when the divisor is 0, the result is 0.
^ Buzzard, Kevin, "Division by zero in type theory: a FA
