Hacker News Reader

> The whole point is that the proof shows you any way you define division by 0 is going to compromise your definition of a field, or it's going to make fields with nonzero elements impossible.

But it does neither. All field theorems pertaining to inverses/division take the form `x ≠ 0 ⇒ ... x⁻¹ ...` None of them is compromised.

> In fact, the modern, axiomatic definition of a field explicitly excludes the unit 0 from the otherwise sane rules of multiplicative inverses.

Exactly, which is why defining 1/0 = 0 (or 42) poses no problem to fields (BTW, the Lean proof assistant defines 0⁻¹ = 0 for fields, even though it's not the inverse and 0*0 = 0).

The whole problem is one of formalization. "Undefined", as it's used in mathematics, is very much informal. It is used to say that a certain expression, 1/0, while "grammatically" correct, is meaningless. Formal systems simply cannot do that: the expression 1/0 must either be ill-formed (can be done with dependent types but is often inconvenient) or it must mean something in the semantic domain of the language. Different formal system define what that something is, but whatever it is, it is no longer "undefined" in the informal sense.

> The whole problem is one of formalization. "Undefined", as it's used in mathematics, is very much informal. It is used to say that a certain expression, 1/0, while "grammatically" correct, is meaningless. Formal systems simply cannot do that: the expression 1/0 must either be ill-formed (can be done with dependent types but is often inconvenient) or it must mean something in the semantic domain of the language. Different formal system define what that something is, but whatever it is, it is no longer "undefined" in the informal sense.

We're substantially in agreement here. This circles back to my core thesis - there is no point in defending the implementation of something mathematically undefined in a programming language by retreating to the formal axioms of fields (or any other algebraic structure, for that matter).

Your other point about 1/0 = x for whatever you'd like x to be is something I mentioned in my comment. The extended real number system does something similar by defining arithmetic of positive and negative infinities. But the extended real number system is not a field. It's a fine and useful system, but you insert pathologies into the real field by trying to accept infinity as a real number. Likewise if you want 1/0 to be equal 42, that's fine. But you're going to "infect" everything that 42 touches in the process. You won't compromise arithmetic, but you will compromise the definition of a field.

What I'm getting at is that 1) mathematically speaking, the author's entire preamble about division by 0 is both incorrect and irrelevant, 2) we should not be trying to justify implementation behavior in systems which cannot use real numbers through the wizardry of field theorems.

> But you're going to "infect" everything that 42 touches in the process

How so? Remember that, e.g. ∀x . 0x ≠ 1 still holds, and it is not true that 0((1/0)(1/42)) = 1 because associativity doesn't apply, because associativity for division stems from the existence of a multiplicative inverse exists, and none does even though 1/0 = 42.

> You won't compromise arithmetic, but you will compromise the definition of a field.

Not at all. Formal systems of mathematics define fields (in general, not just in arithmetic) specifically with 1/0 = 0. Can you show a single field axiom or theorem that would be affected by this?

Perhaps you could if you insisted on stating a theorem by using an informal term such as "wherever foo is defined," but 1/ those theorems can always be stated in more precise terms that don't make use of the informal notion of definedness, and 2/ very few formal systems formalize definedness in a way that means an undefined value must not be 42 (i.e. where you can actually prove 1/0 ≠ 42 or where 1/0 is ill-formed) -- see Feferman https://math.stanford.edu/~feferman/papers/definedness.pdf -- and AFAIK, such systems are very, very rarely used in practice.

At this point I've written a number of comments throughout this thread which explain why division by zero is not possible in a field - specifically, a field which contains nonzero elements. You are asking me to show you an axiom or theorem proving this, but I don't know how else to explain this to you since I've already explained it in a number of different ways. In a sibling comment I even write out the formal proof, and in others I've explained why the author's refutation is incorrect.

I'm not sure what else to say. The author is wrong - it is not at all controversial among mathematicians that the algebraic structure of a field cannot support division by zero. Perhaps I'm simply a poor teacher - in that case I would refer you to [1], [2] and [3] for a better explanation. As I've said elsewhere, you can make a coherent algebra by extending a field - then division by 0 or infinity is possible. But it stops being a field - just as it cannot be many other algebraic structures. Therefore I feel very confident stating that 1) the author is wrong, 2) I've sufficiently explained why in these comments and 3) the burden isn't really on anyone to disprove that division by 0 works at this point.

In any case, this entire discourse is ridiculous because the author should not be trying to defend programming language decisions using abstract mathematics. This kind of nuance and ambiguity is neither necessary nor relevant for justifying an implementation of defined behavior for division by zero. The whole exercise is a farcical distraction, to put it bluntly. Mathematics is pedantic by design, but this sort of definitional rigor is laughably unneeded and for defining integer and float-based arithmetic. The author does a disservice to what is an otherwise reasonable point by (incorrectly) justifying it with axiomatic field theory.

It's self-indulgent over-engineering to try to prove division by zero in fields "works, no really!" from first principles for a programming language blog post; especially when mathematics is essentially united in saying, "no actually, it doesn't."

__________________

1. https://www.reddit.com/r/math/comments/3b5i6p/can_you_divide.... 2. http://mathworld.wolfram.com/DivisionbyZero.html

3. https://en.m.wikipedia.org/wiki/Division_by_zero

If you mean this, https://news.ycombinator.com/item?id=17737661, then it contains a mistake, which I pointed out in a reply.

The references you linked to are irrelevant as they refer to informal mathematics. Of course you can't meaningfully divide by zero (in the sense that the value of division corresponds with our intuitive understanding of what division is). But when it comes to formalization you must assign some meaning to 1/0 or work out a complex system where it becomes ill-formed (i.e. a "syntax error"). The only question is whether that meaning -- that must exist in formal mathematics even though it should not in informal mathematics -- causes an actual contradiction or not, even though it doesn't "make (an informal) sense" either way.

I don't know what to tell you. You're continuing to argue but you seem to not be following my point. I've already long since told you we're in agreement that you need to account for syntactically possible but theoretically impossible algebras for computation. In so doing I have gone further and repeatedly stated that because division by zero is not actually possible in fields, the author should not have tried to use such a rigorous system to justify the practical, syntactical requirements of a programming language. It doesn't make sense to try and refute mathematical theory as the preamble of a programming language manifesto.

What exactly are you looking for me to say here?

> What exactly are you looking for me to say here?

Very simple. Here is a theory of a field in FOL:

    ∀ x . x + 0 = x
    ∀ x . ∃ -x . x + (-x) = 0
    ∀ x, y . x + y = y + x
    ∀ x, y, z . (x + y) + z = x + (y + z)
    ∀ x, y . x – y = x + (-y)
    ∀ x . 1x = x
    ∀ x . x ≠ 0 ⇒ ∃ x⁻¹ . xx⁻¹ = 1
    ∀ x, y . xy = yx
    ∀ x, y, z . (xy)z = x(yz)
    ∀ x, y . y ≠ 0 ⇒ x/y = xy⁻¹
    ∀ x, y, z . x(y + z) = xy + xz

Do you claim that this formalization is unacceptable (i.e. it does not precisely and fully define what a field is)? If so, why? If not, can you write a single theorem in this theory that would be falsified if I added the axiom, ∀ x . x/0 = 0 ?

If your answer to both questions is no, then your only point may be that the extended definition of the symbol / does not deserve the name "division" because it does not conform to our intuitive, informal notion. That's fine but is a long way from claiming that there is no acceptable formalization of fields or that division by zero introduces a mathematical contradiction or breaks equational laws. Note that you cannot say that the original theory defines a field while the extended one doesn't, because the latter's models are a subset of the former's.

This then leaves open the matter of whether such a philosophical, aesthetic consideration trumps pragmatic ones or vice-versa, to which I don't think anyone has a universal answer, and it is not the issue, anyway.

In the definition of a field ∀ x . x/0 = undefined, not 0 or any other value you might prefer.

A field is exactly defined by the field axioms: adding or removing any other axiom makes it no longer a field.

> A field is exactly defined by the field axioms: adding or removing any other axiom makes it no longer a field.

This is clearly not true. Adding axioms (as long as they don't introduce consistency) can only reduce the set of models. Anything that satisfies the larger theory also satisfies the smaller theory. This is exactly why a group is a monoid is a semigroup. This is why fields are rings. In fact, this is why the rationals or the reals are fields: they satisfy the field axioms, and more (for example, they are ordered).

> In the definition of a field ∀ x . x/0 = undefined, not 0 or any other value you might prefer.

What is "undefined"? First let's look at the logic itself: What is true ∨ undefined ? What is true ∧ undefined? Now at the theory: What is undefined + x ? What is 0 * undefined ? What is 0 = undefined ? etc.[0]

While it is possible to formally define this magic non-value (sometimes written as ⊥ in the logics that contain it) as is done in some programming languages (and it has been done), this would entail adding quite a few more axioms to FOL and to the theory of fields. When people say FOL, they mean a particular language[1], one that is considered by mathematicians to be sufficient to formalize all of mathematics and has very particular syntax and semantics. FOL + undefined is a very different language, which much more complicated semantics. If you think that when people refer to FOL they refer to FOL + undefined, I challenge you to find any mention of it in descriptions of standard FOL. Similarly, if you think that by common theories, say fields or sets, people really mean field + undefined or ZFC + undefined (what is {undefined}? What is undefined ∈ {undefined}? etc.), I challenge you to find any mention of the complex axioms required in treatments of these common theories.

But it's not just a matter of convention. The reason you won't find it in the standard logics/theories is that it's completely unnecessary. If you work it out, you'll find that the theory of fields I provided and the more complicated one involving undefined that you suggest is the common formalization are the very same theory, in the sense that they yield exactly the same theorems, except for those specifically involving undefined (i.e., your theory has more theorems than mine). You'll find that you cannot find a "bad" theorem that you can prove with the simple theory but cannot with the one involving undefined, and therefore it is unhelpful except for the purpose of satisfying a certain desire for intuition that requires significantly complicating the formal system.[2]

There's a paper by Sol Feferman[3] reviewing formal systems with explicit handling of "undefined." AFAIK, they are rarely if ever used. Such semantics are certainly not part of the trusty-old FOL, considered the default language of formal mathematics.

[0]: BTW, if you think that the meaning of every expression involving undefined is undefined, then you'll see that this doesn't work. For example, you have: x=0 ⇒ x(1/x)=1. This is a valid formula, and so it's true even when x=0, but then you have undefined on the right-hand side, so you want at least false ⇒ undefined to be equal to true. But A ⇒ B = ¬A ∨ B, which means you want at least true ∨ undefined = true. Similarly, you'll want at least 0 = undefined to be false etc.

[1]: https://en.wikipedia.org/wiki/First-order_logic

[2]: E.g., while in your theory you will be able to prove the rather useless theorem 1/0 ≠ 0, in my theory you will not be able to prove 1/0 = x for any x, so it really poses no issue.

[3]: https://math.stanford.edu/~feferman/papers/definedness.pdf

>This is clearly not true. Adding axioms (as long as they >don't introduce consistency) can only reduce the set of >models. Anything that satisfies the larger theory also satisfies the smaller theory. This is exactly why a group is a monoid is a semigroup. This is why fields are rings. In fact, this is why the rationals or the reals are fields: they satisfy the field axioms, and more (for example, they are ordered).

Look at for example the set of real numbers. If you add the complex numbers to it, you can no longer speak of the real numbers. The real numbers form a subset of the complex numbers. The same thing happens if you add definitions to a field. You create something which has mayber has a field as a subset, but you can no longer speak of a field.

What is "undefined"? First let's look at the logic itself: What is true ∨ undefined ? What is true ∧ undefined? Now at the theory: What is undefined + x ? What is 0 * undefined ? What is 0 = undefined ? etc.[0]

Undefined is just undefined, no value, not a magic one, or just a random one, or one you prefer. Just void, the empty set. To understand it, look for example at the graph of y = sqrt(x), where x and y are real numbers. You see no points at negative x. Its undefined in the domain x < 0. Yes you can say at x < 0, y = 3, that is now my definition sqrt(), but then you no longer have the sqrt function mathematicians talk about. The same thing applies to fields and 1/x.

>What is "undefined"? First let's look at the logic itself: >What is true ∨ undefined ? What is true ∧ undefined? Now at the theory: What is undefined + x ? What is 0 * undefined ? What is 0 = undefined ? etc.[0]

Now you apply boolean logic to the result of calculations, numbers and non-numbers, not on statements. I can also ask what is 5 AND true? Is that true? The question doesn't make sense, so the answer is: depends on the programming language.

> Look at for example the set of real numbers. If you add the complex numbers to it, you can no longer speak of the real numbers.

What does this have to do with adding axioms? You don't get the complex numbers from the real numbers by adding axioms. For example, the following is provable for the reals, but not for complex numbers:

    ∀x,y . x < y ∨ x > y ∨ x = y

> You create something which has mayber has a field as a subset, but you can no longer speak of a field.

No. The class of all fields are all objects satisfying the field axioms. If you add axioms, you get get a subset of those fields. Each and every one of them is a field.

> Undefined is just undefined

I'm not looking for handwaving. Formal mathematics is math that can be done mechanically. Write down the axioms for undefined. Again -- I'm not saying it hasn't been done, but it's certainly not part of standard first-order logic, and it is unnecessary.

> To understand it, look for example at the graph

I understand what undefined means in informal mathematics. Try to see what it means in formal mathematics. But the important point is, try to understand why it is unnecessary in formal mathematics in most cases.

> Now you apply boolean logic to the result of calculations, numbers and non-numbers, not on statements.

No. You can write 1/x < 5 ∨ x > 20.

> The question doesn't make sense, so the answer is: depends on the programming language.

There is no such thing as "doesn't make sense" in formal math, even though there is such a thing in informal math. That's the whole point. Either the expression is ill-formed, i.e. not in the language or a "syntax error", or it must make some sense.

This is why it's useful and easy to say something is undefined in informal math, but not as useful and not as easy to do that in formal math.

>What does this have to do with adding axioms? You don't get the complex numbers from the real numbers by adding axioms. For example, the following is provable for the reals, but not for complex numbers:

> ∀x,y . x < y ∨ x > y ∨ x = y

Since R is a subset of C, you can write C as R with additional axioms. See for example:

http://www.math.mcgill.ca/gantumur/math249w15/numbers.pdf

>I'm not looking for handwaving. Formal mathematics is math that can be done mechanically. Write down the axioms for undefined. Again -- I'm not saying it hasn't been done, but it's certainly not part of standard first-order logic, and it is unnecessary.

Undefined is just undefined, that is no handwaving, it is a primitive notion. See https://en.wikipedia.org/wiki/Primitive_notion

You are trying to define the undefined in a formal system. Undefined is just the absence of a definition. Not 0, 3 , 2pi

> No. You can write 1/x < 5 ∨ x > 20. Yes, those are valid mathematical statements. 5 ∨ TRUE, or undefined V TRUE, I doubt it.

> There is no such thing as "doesn't make sense" in formal math, even though there is such a thing in informal math. >That's the whole point. Either the expression is ill-formed, i.e. not in the language or a "syntax error", or it must make some sense.

Well in language, in which I am corresponding with you, there is such a thing as 'makes no sense'.

You are somehow trying to capture everything in your logical system only to try to prove that 1/0 = 0 is part of a field, which it isn't. I've made my point here, it was nice talking to you.

> Since R is a subset of C, you can write C as R with additional axioms.

That's not even remotely how it works. You may want to read up on logical theories and models[1].

> Well in language, in which I am corresponding with you, there is such a thing as 'makes no sense'.

Yes, and for the same reason we can have such a thing as "undefined" (that means more than merely 'not specified') in informal mathematics -- because both English and informal math are informal. But we are talking about formal languages[2], which do not have such a thing.

[1]: https://en.wikipedia.org/wiki/Theory_(mathematical_logic), https://en.wikipedia.org/wiki/Structure_(mathematical_logic)

[2]: https://en.wikipedia.org/wiki/Formal_system

It seems like he covered that in the article. There is no multiplicative inverse of zero.

But that isn't the same as defining a division operation.

He didn't cover that in the article, or at least not in a way that actually supports his point. Since there is no multiplicative inverse of 0, division by 0 is undefined behavior. Trying to remediate that by refuting the "proof" that it's undefined while still asserting that we can define it as something else is mathematically incoherent.

If you want to see why it doesn't work from a number of different angles, read through the /r/math thread[1] or the Wolfram MathWorld blurb [2].

The formal problem comes down to one of uniqueness of elements. If you define division by zero in a field, you must end up in a place where it follows that every element is equal to every element. Then you only have one element - 0. So really we should be stating that division by zero is undefined behavior in fields with at least one nonzero element.

But again - we can neatly sidestep all of this, because trying to defend your choice of undefined behavior in a programming language based on the abstractions of field axioms is silly. In the actual world we don't even deal with real numbers computationally, let alone the particular nuances of whether or not our programming language implements number systems composing a field or any other algebraic structure.

__________________________

1. https://www.reddit.com/r/math/comments/3b5i6p/can_you_divide...

2. http://mathworld.wolfram.com/DivisionbyZero.html

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

https://coq.inria.fr/library/Coq.Init.Nat.html

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 :)

First, mathematics does not give us true statements about the world, it gives us consequences that must follow if we accept various axioms or definitions.

Isn't a consequence in itself a true statement?

Allow me to clarify that point. The idea is that - conceptually speaking - mathematics cannot be used to tell you empirical axioms about the world in which we reside. All it can do is tell you what must be true given certain well-defined assumptions. It is a phenomenally powerful tool for proving things about the world from empirical axioms, but which empirical axioms we choose to rely on in engineering is mostly the domain of physics or the sciences.

The underlying point here is mostly a philosophical one, but it has some bearing on the matter at hand. In effect, the definition (or lack thereof) for division by zero in fields is of no practical consequence for the real world impact of implementing an operation which admits division by zero. I can define an algebraic structure in which division by zero is sane (it is not in fields, despite what the article states!), or I can define an algebraic structure in which division by zero is insane. Both can be coherent, consistent and genuinely useful.

But whether or not I can define something that works has nothing to do with what happens "when the rubber meets the road", so to speak. It was a mistake to open up an argument about programming division by 0 using the field axioms in the first place. There is no "one truth", there are only facts which must follow as consequences from assumptions. This is especially the case for programming, considering that computers are fundamentally incapable of working with real numbers in the first place.

They're true statements about the mathematical system. They might have no relevance to reality.