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.
Comments
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.