I believe you but that’s kind of mind blowing. How do they avoid the seemingly-obvious corollary that 0*0 = X, for all values of X? That is, just multiplying both sides of “x/0 = 0” by zero.

By specifying that x/y*y is only equal to x if y≠0, I guess?

Exactly.

Functions in these logics are total, so if you want division to be a function (and you probably do), it has to assign something to division by 0.

It would be acceptable to assign an unspecified object from the domain, for which you have no non-trivial theorems, and so all your real theorems must have a precondition about the denominator being non-zero. But if you specify a candidate like 0, you can get some theorems which don't have the precondition. Consider:

a/b * c/d = ac/bd.

This now holds even if one of b or d is 0.

I appreciate the explanation and I’m in no position to disagree, but ugh. Seems like it would work just as well to define x/0 as 6, or e, or -15. I’m sure that’s not the case. But as a long time tech person who’s always considered underflow/overflow to be a hack to get around limitations of hardware, it offends be a bit to find conditionals in abstract math. Undefined seems cleaner, like null, since it implicitly says “don’t treat this as a normal value that you can operate on”.

I suspect the real math people know what they’re doing more than I do, though.

The theorem a/b * c/d = ac/bd doesn't hold if x/0 = 6, though.

The theorem prover HOL Light is a close cousin of Isabelle/HOL and doesn't adopt this, and just says that x/0 is some unspecified number. You can't prove much interesting about it. You can prove, say, that x/0 * 0 = 0, but you can't prove whether or not x/0 is, say, positive or not.

If you prefer null, there was a logic that allowed for undefined terms and partial functions that became the basis of the IMPS theorem prover. I found it most notable for the fact that it doesn't have reflexivity of equality: 1/0 = 1/0 is false in IMPS.

Division is already defined conditionally in regular old elementary school field theory.

It's not making a multiplicative inverse of 0 exist though, it just defines a '/' operator that is slightly different from our usual one (i.e. a/b = a*b^(-1))

Thanks - I was not aware that theorem provers often allow "division" by zero.

Looking at https://xenaproject.wordpress.com/2020/07/05/division-by-zer... I see that they don't use mathematical division, but define a slightly different operator with an additional condition for handling zero. This appears to be far more convenient for theorem provers.

The trade-off would be that "division" is no longer the inverse of multiplication.

Ah, thanks for the link. I suggested the reason that Isabelle/HOL does this is because it requires total functions and you don't have a convenient way to do refinement types. But that's not an adequate explanation, because Lean does allow such refinements, but it still turns out to be inconvenient for division.

I will note that setting a - b = 0 for a <= b is pretty standard, and is often called "partial subtraction."