3 ms·

It's a slight tangent, but in the general realm of division being complicated, divide by zero is a longstanding annoyance. Does anyone know (or can refer to) a

It's a slight tangent, but in the general realm of division being complicated, divide by zero is a longstanding annoyance. Does anyone know (or can refer to) a reasonable definition of +,-,*,/,% (in their usual meanings) on rational numbers such that A op B always evaluates to a rational? A/1 divide 0/1 being stored as 1/0 and then propagated around seems reasonable but I keep putting off the bookwork of finding out what arithmetic relations still hold at that point. I think one loses multiply by zero folding to zero, for example A * 0 is now only 0 for A known to have non-zero denominator. Context is a language with arbitrary precision rationals as the number type, and all I'm really looking for is a way to declare that the type of division is a rational for any rational arguments. Searching for this mostly turns up results on the naturals or integers which I'm not particularly interested in. Long shot but worth asking. Thanks

DougMerritt 3y ago
In ordinary arithmetic and algebra, there isn't any reasonable definition of n/0 because if it is allowed, then one can prove contradictory things. Outside of proof systems/pure math, like in software you write, you can define n/0 to be anything you like, you just can't depend on being able to derive mathematically consistent results. There are also more exotic math systems. Infinity is not literally a number (it would lead to contradictions), but mathematicians can happily deal with numbers systems augmented with infinity as an extra member -- one just has to step carefully, since it still isn't a number. The "number system" has one non-number member requiring special handling. Similarly there are modern approaches to infinitesimals where there's a thing "e" which is not zero, but e^2 is zero. That is not normal arithmetic but when handled carefully it can be useful.
jasomill 3y ago
Does anyone know (or can refer to) a reasonable definition of +,-,*,/,% (in their usual meanings) on rational numbers such that A op B always evaluates to a rational? Given the usual definition of multiplication (and division as its inverse), this is not possible: Assume some multiplicative inverse 0⁻¹ of 0 exists. Then, writing · for multiplication, since a·0 = b·0 for all rational a and b, we have a·0·0⁻¹ = b·0·0⁻¹ and therefore a = b for all rational a and b, which is absurd.
- jasomill 3y ago
  As for extending the rationals by 0⁻¹ and giving up properties, a·0 = 0 can still hold for all a ≠ 0⁻¹. To get an idea of what operations do and don't make sense when extending the rationals in the way you propose, define ∞ as our 0⁻¹ and refer to https://en.wikipedia.org/wiki/Projectively_extended_real_line#Arithmetic_operations https://en.wikipedia.org/wiki/Projectively_extended_real_lin... substituting ℚ and ℚ̂ for ℝ and ℝ̂. For a similar construction that maintains ordering properties, see https://en.wikipedia.org/wiki/Extended_real_number_line#Arithmetic_operations https://en.wikipedia.org/wiki/Extended_real_number_line#Arit... Finally, note that the complex number equivalent to your construction is really interesting and useful: https://en.wikipedia.org/wiki/Riemann_sphere https://en.wikipedia.org/wiki/Riemann_sphere https://www-users.cse.umn.edu/~arnold/moebius/ https://www-users.cse.umn.edu/~arnold/moebius/
  - JonChesterfield 3y ago
    The Riemann sphere has always existed beyond my grasp of mathematics. I remember the maths undergraduates being excited about it. Thank you for the references, it looks like I need to learn more before proceeding with certainty.
discarded1023 3y ago
The standard arithmetic classes of Isabelle/HOL show that you can extend division with the equation `x / 0 = 0` and things (seemingly) work out. https://lawrencecpaulson.github.io/2021/12/01/Undefined.html https://lawrencecpaulson.github.io/2021/12/01/Undefined.html https://www.hillelwayne.com/post/divide-by-zero/ https://www.hillelwayne.com/post/divide-by-zero/ https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/ https://xenaproject.wordpress.com/2020/07/05/division-by-zer... You'll need to do some thinking/proof to find out if it works for you.
- JonChesterfield 3y ago
  Huh. That's surprising but quite persuasive, thank you for the references. I like the general view that a non-axiomatic divide can't introduce unsoundness so define it however is useful. It has somewhat kicked the can down the road to defining the multiplicative inverse, but that's still a good step forward. Thank you
amenhotep 3y ago
Not a very satisfying answer (feels like if a satisfying answer to this question was possible, maths would look very different) but I think the trick to not getting annoyed by it is to shift your perspective rather than try and redefine maths. It's not that division is a badly behaved operator; it's that division isn't an operator. It's a shorthand for multiplication by the reciprocal. Since the reciprocal of 0 doesn't exist, we can no more multiply by it than we can compute 5 + the sound of one hand clapping. And we don't fret over how the addition operator's inadequacy there is unsatisfying!

DougMerritt 3y ago

In ordinary arithmetic and algebra, there isn't any reasonable definition of n/0 because if it is allowed, then one can prove contradictory things. Outside of proof systems/pure math, like in software you write, you can define n/0 to be anything you like, you just can't depend on being able to derive mathematically consistent results. There are also more exotic math systems. Infinity is not literally a number (it would lead to contradictions), but mathematicians can happily deal with numbers systems augmented with infinity as an extra member -- one just has to step carefully, since it still isn't a number. The "number system" has one non-number member requiring special handling. Similarly there are modern approaches to infinitesimals where there's a thing "e" which is not zero, but e^2 is zero. That is not normal arithmetic but when handled carefully it can be useful.

jasomill 3y ago

Does anyone know (or can refer to) a reasonable definition of +,-,*,/,% (in their usual meanings) on rational numbers such that A op B always evaluates to a rational? Given the usual definition of multiplication (and division as its inverse), this is not possible: Assume some multiplicative inverse 0⁻¹ of 0 exists. Then, writing · for multiplication, since a·0 = b·0 for all rational a and b, we have a·0·0⁻¹ = b·0·0⁻¹ and therefore a = b for all rational a and b, which is absurd.

jasomill 3y ago
As for extending the rationals by 0⁻¹ and giving up properties, a·0 = 0 can still hold for all a ≠ 0⁻¹. To get an idea of what operations do and don't make sense when extending the rationals in the way you propose, define ∞ as our 0⁻¹ and refer to https://en.wikipedia.org/wiki/Projectively_extended_real_line#Arithmetic_operations https://en.wikipedia.org/wiki/Projectively_extended_real_lin... substituting ℚ and ℚ̂ for ℝ and ℝ̂. For a similar construction that maintains ordering properties, see https://en.wikipedia.org/wiki/Extended_real_number_line#Arithmetic_operations https://en.wikipedia.org/wiki/Extended_real_number_line#Arit... Finally, note that the complex number equivalent to your construction is really interesting and useful: https://en.wikipedia.org/wiki/Riemann_sphere https://en.wikipedia.org/wiki/Riemann_sphere https://www-users.cse.umn.edu/~arnold/moebius/ https://www-users.cse.umn.edu/~arnold/moebius/
- JonChesterfield 3y ago
  The Riemann sphere has always existed beyond my grasp of mathematics. I remember the maths undergraduates being excited about it. Thank you for the references, it looks like I need to learn more before proceeding with certainty.

discarded1023 3y ago

The standard arithmetic classes of Isabelle/HOL show that you can extend division with the equation `x / 0 = 0` and things (seemingly) work out. https://lawrencecpaulson.github.io/2021/12/01/Undefined.html https://lawrencecpaulson.github.io/2021/12/01/Undefined.html https://www.hillelwayne.com/post/divide-by-zero/ https://www.hillelwayne.com/post/divide-by-zero/ https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/ https://xenaproject.wordpress.com/2020/07/05/division-by-zer... You'll need to do some thinking/proof to find out if it works for you.

JonChesterfield 3y ago
Huh. That's surprising but quite persuasive, thank you for the references. I like the general view that a non-axiomatic divide can't introduce unsoundness so define it however is useful. It has somewhat kicked the can down the road to defining the multiplicative inverse, but that's still a good step forward. Thank you

amenhotep 3y ago

Not a very satisfying answer (feels like if a satisfying answer to this question was possible, maths would look very different) but I think the trick to not getting annoyed by it is to shift your perspective rather than try and redefine maths. It's not that division is a badly behaved operator; it's that division isn't an operator. It's a shorthand for multiplication by the reciprocal. Since the reciprocal of 0 doesn't exist, we can no more multiply by it than we can compute 5 + the sound of one hand clapping. And we don't fret over how the addition operator's inadequacy there is unsatisfying!