I sympathise with you here, as some mathematicians freak out at any mention of division by zero. It’s not always easy for them to grasp what we are doing with formal logic. You also need to bear in mind that mathematics texts are not proved in any formal system, and in most cases, foundational matters are kept well in the background. Unless the material is specifically axiomatic set theory, it’s a mistake to imagine that mathematics is being done in ZFC.
One can at least mention that the usual paradoxes connected with division by zero do not occur, since we do not have (x*y)/x = y unconditionally. Larry Paulson > On 20 Feb 2019, at 20:40, hol-info-requ...@lists.sourceforge.net wrote: > > Keeping ``0 / 0 = 0`` as before, could be another option, but I have concerns > to convince mathematicians to accept this fact since I aim at precisely > reproduce those pure math proofs under the ?same? formal system with math > books _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
