[momentoftop]

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.

[brookst]

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.

[momentoftop]

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.

[hgsgm]

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