Disclaimer 2024-12-02

Since this rant is going viral again (again (again)), some disclaimers:

1. I wrote this six years ago to “”“win”“” an ugly Twitter fight. I’m glad I anonymized the inciting tweet and hope I’m the only person still getting grief over this.
2. The core interesting bit— why it’s mathematically valid to define 1/0=0 and why many theorem provers use that definition— is better covered by the Xena project FAQ.
3. “Good for a theorem prover” is not the same as “good for a programming language”.
4. 99+% of mathematicians use the normal, everyday definition of division as “inverse multiplication” to do 99+% of all mathematics. “Defined-everywhere” division is mostly of interest to logicians and some algebraists.
5. More than anything else, I’m fascinated by how defining division by zero seems like it would break everything, but is both a consistent and gives us insight into other math. Mathematics isn’t rote memorization: it’s fluid, playful, and delightful.

---

Have a tweet:

I have no idea if Pony is making the right choice here, I don’t know Pony, and I don’t have any interest in learning Pony.¹ But this tweet raised my hackles for two reasons:

1. It’s pretty smug. I have very strong opinions about programming, but one rule I try to follow is do not mock other programmers.² Programming is too big and I’m too small to understand everything. Disagreeing is fine, laying out why people are wrong is fine, making fun of them is not fine.
2. It’s saying that Pony is mathematically wrong. This is objectively false.

I tweeted a thing about why 1/0 = 0 is mathematically sound. Some people agreed, some people agreed with caveats, and some people called it bunk. A few people said it’s clear I don’t know real mathematics, because a real mathematician would never make such a mistake.

So in this post I’d like to clearly, formally lay out why it’s consistent to say that 1/0 = 0, why some of the common objections don’t apply, and what the real mathematicians say. Fair warning, this post is going to be a little more mathematically dense than my usual stuff. I’ve tried to make it clear but, well, math.

Consistency

First we need to explain what we mean by “consistency”. The formalism is sound if you can only use it to prove true statements. To say 1/0 = 0 is unsound is to either say that we can prove 1/0 ≠ 0 or that, given 1/0 = 0, we can prove something that’s false. These are actually equivalent statements but it’ll be useful to treat them as distinct for teaching purposes.

Next we need to explain what we mean by “division”. But to do that, I need to introduce fields.

Fields

A field is a set of elements (S) along with an addition operator (+) and a multiplication operator (*) that follow some properties:

1. The set is closed under both operations. If x is an element of S and y is an element of S, then both x + y and x * y are elements of S.
2. Both operations are commutative. a + b = b + a, and a * b = b * a.
3. Both operations are associative. a + (b + c) = (a + b) + c, and a * (b * c) = (a * b) * c.
4. Multiplication is distributive. a * (b + c) = a * b + a * c.
5. There is an element that is the additive identity, or 0, such that a + 0 = a.
6. There is an element that is the multiplicative identity, or 1, such that a * 1 = a.
7. The two identities are different elements. 1 ≠ 0.
8. Every element has an additive inverse, -a, such that a + (-a) = 0.
9. Every element EXCEPT 0 has a multiplicative inverse, a⁻, such that a*a⁻ = 1.

These are all of the rules of a field. We can define S, +, and * any way we want, as long as all of the rules are followed. The real numbers, along with our conventional notion of addition and multiplication, form a field. This gives us the building blocks to discover properties of our system. In order to prove a theorem, we need to be able to derive it solely through the definitions of S/+/*, the definition of a field, and any axioms we have.³ For example, we can prove that for all a, a * 0 = 0:

1. By the additive identity, 0 + 0 = 0, so a * 0 = a * (0 + 0)
2. By the distributive property, a * (0 + 0) = a * 0 + a * 0
3. By the additive inverse property, there is some - (a * 0) such that - (a * 0) + (a * 0) = 0.
4. Combining (1) and (2), we get a * 0 = a * 0 + a * 0.
5. Combining (3) and (4), we get - (a * 0) + (a * 0) = - (a * 0) + a * 0 + a * 0.
6. Evaluating (5) gives us 0 = a * 0. QED.

Now that we have this as a theorem, we can use it to prove other theorems. Given this property, we can immediately show that there is no multiplicative inverse of 0:

1. If 0 had a multiplicative inverse 0⁻, then 0 * 0⁻ = 1.
2. For all real numbers, a * 0 = 0.
3. Since 1 ≠ 0, there is no multiplicative inverse of 0⁻.

Okay, now we can talk about division in the reals.

Division

The field definition does not include division, nor do our definitions of addition or multiplication. This means we are free to define division however we want. We want to define it in a way that mostly follows our intuition and is sound. I say mostly because our intuition doesn’t generalize. As an example, we intuitively think of a * b as “a summed up b times”. So what’s -1 * π? How do you sum up something π times? While it would be nice if division didn’t have any “oddness” to it, we can’t guarantee that without kneecapping mathematics.

The intuitive definition of division is multiplying by the inverse. a/2 = a * 2⁻. Under this definition, we can get all of the properties of division we’re used to by proving that they hold. For example,

• Theorem: a/a = 1. Proof: a/a = a * a⁻ = 1.
• Theorem: a * (b/c) = b * (a/c). Proof: a * (b/c) = a * (b * c⁻). Since multiplication is commutative and associative, we can rearrange this to get b * (a * c⁻) = b * (a/c).

This is all great, except for one problem: 0 does not have a multiplicative inverse. Both of those proofs are invalid: if I write 0/0, I get 0 * 0⁻, which is an invalid equation. So we cannot prove that a/a = 1. We can, however, prove something weaker:

• Theorem: IF a ≠ 0, THEN a/a = 1. Proof: same.
• Theorem: IF c ≠ 0, THEN a * (b/c) = b * (a/c). Proof: same.

Note this does not go both ways: it does not follow that 0/0 ≠ 1. All we know is we cannot use this theorem to prove that 0/0 = 1. So we do not have that 0/0 ≠ 1. For any given number, we cannot prove that 0/0 is not that number! Since we’ve defined division as multiplying by the inverse, and zero does not have an inverse, our definition of division does not cover dividing by zero. It does not say anything about it, leaving it “undefined” if you will.

Since this form of division is not defined for 0, it is a partial function over the reals: there is some value in its domain that we have not specified. Practically, this is fine: we’re used to thinking of 1/0 as an impossible operation. But this has some weird consequences: one of our axioms is everything is equal to itself. So does 1/0 = 1/0? If you say that’s silly, we no longer have a = a! And even if you’re fine with that, what about the statement TRUE \/ (1/0 = 1/0)? It shouldn’t matter what the second clause is, because that statement should be true. But by the axiom of the excluded middle, we’d then have to say the second clause is either true or false. When trying to formalize math and logic, we have to find some way to address what happens if you write 1/0. So there’s generally three things mathematicians can do:⁴

• We can say nope, sorry, you can’t even write 1/0, much less give it a value. This is what we do in our day-to-day lives, and the way that Agda and Idris handle division.
• We can choose some value that isn’t a real number, such as “undefined” or infinity, and say x/0 = <whatever>. This is what some mathematicians do with the Riemann sphere.
• We could choose some real number, like 19, and say that x/0 = 19. This is what Isabelle, Lean and Coq do.

All of these have tradeoffs. We already talked about some of the headaches with banning equations like 1/0. With an “undefined” value, division is no longer closed on the reals. In the last case, you explode everybody’s intuitive notion of division. But all of these are sound. Since our original notion of division does not say anything about dividing by zero, it does not rule out anything. None of these extensions lead to a contradiction.

The controversy is over the last case, so let’s focus on that. We’ll define division as follows: IF b = 0 THEN a/b = 1 ELSE a/b = a * b⁻.

Something I need to emphasize here: this does not give us an inverse of 0. 1/0 is not 0⁻. This means that while 0/0 = 1, 0 * 1/0 = 0. Division is only “multiply by the inverse” when the denominator isn’t 0. All we’ve done is special case dividing by zero and nothing else. And doing so is mathematically consistent, because under this definition of division you can’t take 1/0 = 1 and prove something false.

Objections

Here’s where a lot of people objected. They would take the fact 1/0 = 1 and prove something false, usually 1 = 0. None of these proofs, however, are sound. To see why, let’s dig into a couple example proofs and show where they break down.

Here’s a common argument:

1. 1/0 = 1
2. 1/0 * 0 = 1 * 0
3. 1 * 0/0 = 0
4. 1 = 0

The problem is in step (3): our division theorem is only valid for c ≠ 0, so you can’t go from 1/0 * 0 to 1 * 0/0. The “denominator is nonzero” clause prevents us from taking our definition and reaching this contradiction.

Here’s where people got tripped up. They assume we needed the nonzero clause on our division theorems because x/0 is undefined. “If x/0 is a value, then the theorem should extend to c=0, too.” This is wrong. The problem is not that 1/0 was undefined. The problem was that our proof uses the multiplicative inverse, and there is no multiplicative inverse of 0. Under our modified definition of division, we still don’t have 0⁻, which means our proof still does not work for dividing by zero. We still need the condition. So it is not a theorem that a * (b / 0) = b * (a / 0).

To be clear, this does not mean they must be different! All we know is that we cannot use this theorem to argue they are equal. Since the “proof” that 1 = 0 used that theorem, the proof is unsound.

Pretty much every counterargument makes this exact same mistake: it assumes that because 1/0 is now defined, there is now some 0⁻ that generalizes our theorems. But there’s not.

Another common objection is that if 1/0 = 1, then multiplicative inverses are no longer unique: 2/2 = 1, but also 2/0 = 1, so now 2 has two inverses. This, again, confuses cause and effect. 1/2 is the inverse of 2 not because of how we define inverses, but how we defined division. 2/2 = 1 because 2/2 = 2 * 2⁻. But, again, zero does not have an inverse, and 2/0 is not 2 * 0⁻. Since 0⁻ does not exist, it is not an inverse of 2, and every nonzero number still has a unique inverse.

If you want to prove that 1/0 = 1 leads to a contradiction, you must explicitly list every step you take and show that none of them assume that 0⁻ exists.

1/0 = 0

We’ve now established Let’s assume for now that if we choose some constant C, then defining division such that x/0 = C does not lead to any inconsistencies.⁵ It turns out that for certain choices of C, specifically 0, we can make some theorems stronger. We can do this by removing the conditions on (some of) our division theorems, and then add a special case to the proof itself. For example:

• Theorem: a * (b/c) = b * (a/c). Proof: we already proved this for c ≠ 0. Now let c = 0. Then a * (b/0) = a * 0 = 0, and b * (a/0) = b * 0 = 0, and 0 = 0.

Under this definition of division step (3) in the counterargument above is now valid: we can say that 1/0 * 0 = 1 * 0/0. However, in step (4) we say that 0/0 = 1. This theorem does not get stronger:

• “Theorem”: a/a = 1. Proof: we already proved this for a ≠ 0. Now let a = 0. Then a/a = 0/0 = 0, so 1 = 0 and wait shit nevermind

This is why Lean and Isabelle define 1/0 this way. Coq does it too, but as far as I can tell they don’t use it as an optimization.

The Real Mathematicians

A final objection is that I’m a CS person, not a mathmatician, so I don’t understand the math here. But what do the PhDs say?

Lawrence Paulson, professor of computational logic and inventor of Isabelle:

A bit of history: the first logic supported within Isabelle was Martin-Löf’s constructive type theory, and it is still there (CTT). And while developing arithmetic within that formalisation, I came up with a definition (necessarily primitive recursive and executable) of division. It delivered n/0 = 0. Since then a number of people have noticed that defining x/0 = 0 is convenient. This identity holds in quite a few different proof assistants now.

These things are conventions, exactly the same as announcing that x^-n = 1/x^n and that x^0 = 0 [sic].

Leslie Lamport, Math PhD and winner of the 2013 Turing Award:

[In ZF set theory] Since 0 is not in the domain of recip, we know nothing about the value of 1 / 0; it might equal √2, it might equal R, or it might equal anything else.

Matt Noonan, Math PhD and introducer of Ghost Proofs to Haskell:

looks all fine to me!

Arthur Azevedo de Amorim, an author of the introductory Coq textbook, reconstructs the same argument I did here.

I also chatted with a few math graduate student friends and emailed a couple of postdocs I know. So far people nobody’s said that letting 1/0 = 0 is unsound. If any end up getting back to me with that I will include their refutation of this post.

Conclusions

This was originally motivated by how Pony does division. So, is Pony doing the right thing here? No clue. Pony is a programming language, not a formal mathematical system. Consistency is less important than safety, convenience, and context. As a programmer, I don’t like it.⁶

But is Pony doing something unsound? Absolutely not. It is totally fine to define 1/0 = 0. Nothing breaks and you can’t prove something false. Everybody who was making fun of Pony programmers for being ‘bad at math’ doesn’t actually understand the math behind it.

Don’t make fun of other people. The world is big and we are small.

Thanks to Watson Ladd, Matt Noonan, Ron Pressler, Josh Lieber, and Edwin Brady for feedback.

Update 8/12/2018

Some people pointed out I was using some terms ambiguously, which I’ve done my best to fix. A bunch of people also sent in more counterarguments, most of which fell along common themes.

ab = cb => a = c but with division by zero we have 1 * 0 = 2 * 0 => 1 = 2.

This is a common mistake a lot of people made: assuming that some property of division is somehow part of the definition, not something we have to show is true. But division has no “innate” properties: everything manipulation we make involving it is something we have to prove is a valid manipulation. For any contradiction, you must list out, for every manipulation of the equation you make, the theorem that makes that manipulation valid, and show that the proof of that theorem does not use 0⁻.

Letting 1/0 = 0 will lead to hidden errors in your program.

As mentioned before, this is not a post about what’s practically a good idea. All I’m arguing is that mathematically, we can extend division in this way without leading to a contradiction. Programming languages are different from mathematical formalisms, and should be different. I prefer that 1/0 is an error, because I’m not using my program to prove theories.

All languages need to make sacrifices of mathematical soundness in favor of safety, practicality, and predictability. It’s the same reason why, in almost every practically-used language, head has type [a] -> a, not [a] -> Maybe a.

We no longer have that division is the inverse of multiplication over its whole domain.

This is a common argument, and arguably is more about the “aesthetics” of division than what’s formalizable. This happens a lot when we extend functions. For example, over the naturals, a * b is just repeated addition. But if we extend multiplication over the rationals, then we lose that nice definition.

In general, I aesthetically “dislike” definitions and theorems that explicitly include a dependence on a function’s domain, because it leads to “side effects” when we extend them.

If 0/0 = 0 then lim_(x -> 0) sin(x) / x = sin(0) / 0 = 0, but by L’Hospitals’ Rule lim_(x -> 0) sin(x) / x = lim_(x -> 0) cos(x) / 1 = 1. So we have 0 = 1.

This was a really clever one. The issue is that the counterargument assumes that if the limit exists and f(0) is defined, then lim_(x -> 0) f(x) = f(0). This isn’t always true: take a continuous function and add a point discontinuity. The limit of sin(x) / x is not sin(0) / 0, because sin(x) / x is discontinuous at 0. For the unextended division it’s because sin(0) / 0 is undefined, while for our extended division it’s a point discontinuity. Funnily enough if we instead picked x/0 = 1 then sin(x) / x would be continuous everywhere.

A couple of other people brought up limit arguments, but they all are addressed in a similar way.

It’s icky.

Don’t disagree.

Update 10/23/19

I’ve been informed that Pony now supports partial division.