> Trying to remediate that by refuting the "proof" that it's undefined
He does not refute any proofs by citing that division by 0 is undefined. He refutes them by asserting that the multiplicative inverse doesn't exist. These are very different statements.
Neither the standard field nor his modified field use the zero inverse, 0⁻. The proofs he's criticizing do erroneously use 0⁻. That's what he's calling out, I believe.
> He refutes them by asserting that the multiplicative inverse doesn't exist.
Yes - but in algebraic fields division by x is equivalent to multiplication by 1/x. This is precisely why you cannot have a field that admits division by 0: because 0 has no multiplicative inverse.
Maybe all this talk about fields is a distraction? Integer arithmetic isn't a field anyway. Other than 1 and -1, no integer has a multiplicative inverse that's an integer.
Integer division just isn't the same operation as division on rationals or reals. The same laws don't apply.
(For floats, division by zero can return Inf, -Inf or NaN and there's no reason to define it differently.)
It looks like the theorem-proving languages that define 1/0 to be 0 tend to be using natural numbers as a fundamental type. Not only do they define division differently, they also don't have negative numbers, and so define 2-3 to be 0.
Yes! Exactly, it's a distraction. There are reasonable, well-intentioned reasons to argue that division by 0 should be an acceptable operation in a computational setting. Computational settings need not admit all the rigor of theoretical math. I wish the author had not tried to involve field theory and programming like this because it detracts from the point :)
He does not refute any proofs by citing that division by 0 is undefined. He refutes them by asserting that the multiplicative inverse doesn't exist. These are very different statements.
Neither the standard field nor his modified field use the zero inverse, 0⁻. The proofs he's criticizing do erroneously use 0⁻. That's what he's calling out, I believe.