imh 7 months ago | favorite | on: 1/0 = 0 But the point is you keep the structure of a field for everything that already has it, right? No structure is taken away. All statements valid on any subset of the reals are still valid without modification under this new definition. The algebraic structure is still a field obeying the same axioms. There are just some new valid statements too.

 No that's not correct, and this is why I think the author's entire point is pretty inane. If you're going to start off your argument with the full formalism of field axioms and consequent theorems, you need to be prepared to split hairs about whether or not your definitions constitute a field.Mathematics is thoroughly pedantic about definitions for a reason. If those formalisms don't matter because what you've done is "close enough", then skip the song and dance about field definitions and stop trying to use it to justify the behavior of an undefined operation in a programming language. Just say you're defining 1/0 to be equal to whatever you want because the world doesn't break down. It actually detracts the author's point to so confidently (and incorrectly) refute something that is robustly proved in the first few weeks of an undergraduate analysis course. Why is this even in a blog post about a programming language?!This is essentially the same point as the extended real (or complex) number systems. The sets of all real and complex numbers (respectively) form fields under the axioms of addition and multiplication. But you can define division by 0 and division by infinity in a way that works with familiar arithmetic (I explained how to do this in another comment barely two weeks ago [1]). But the key point here is that in doing this you sacrifice the uniqueness of real numbers.The author tries to refute this observation by claiming the proof uses an undefined division operation, but that's a red herring. The real assertion is that you cannot define division as an inverse operation from multiplication to be inclusive of division by the unique unit (i.e. 0, in the real field) unless you are willing to state that every number is equal to every other number in the entire field. And you can do that, but it trivially follows that you no longer have a field without a nonzero element.So really the actual proof is that division by 0 is undefined for any field with at least one nonzero element.__________________________________
 Is there a proof or something elsewhere you can link to? To be honest I can't really tell the point you're trying to make.
 I can give you a simple proof by contradiction.1. Let F be a field containing an element x =/= 0.2. Suppose we have defined division by zero in F such that, for all x in F, there exists an element y = x/0 (i.e. F adheres to the field axiom of multiplicative closure). Note that at this point it does not matter how we have defined division by 0, we will just generously continue and assume you've done it in a way that maintains the other field axioms.3. Since y = x/0, it follows that the product of y and 0 is equal to x, because division is the inverse of multiplication. By the field axioms, division does not exist if there is no multiplicative inverse with which to multiply.4. But by the field axioms this implies that x = 0, which contradicts our initial assumption. Likewise, since we can repeat this procedure with any element x in F, this demonstrates that there exists no nonzero element x in F, and in fact F = {0}.The failure in the article's refutation is that this proof is designed to permit you to assume you have suitably defined division by zero, then proceed to demonstrate without any loss of generality that you could not possibly have unless 1) F is not a field, or 2) F contains only 0. The fundamental algebraic property you sacrifice by defining division by zero is uniqueness, and uniqueness is a hard requirement in fields with nonzero elements.
 There is a mistake in your step 3, as it relies on an informal and imprecise "division is the inverse of multiplication". If you were to write that formally, you'd get `∀ x ≠ 0 . x(1/x) = 1`. This holds unchanged even if you define division by zero.Even if you could come up with another formalization that does cause a problem, e.g. `∀ x ∈ dom(1/t) . x(1/x) = 1` (and I would say that this is the only formalization that causes an issue, and it requires the use of a language with a dom operator, something that is absolutely not required for theories of fields), it won't matter because the question is not whether one could come up with a formalization that leads to contradiction, but whether there are reasonable formalizations of fields where this does not happen, and there are (in fact, most of them satisfy this, as they do not rely on a dom operator).In addition, it is not true that "by the field axioms, division does not exist if there is no multiplicative inverse with which to multiply." It's just that the field axioms do not define what the meaning of division is in that case. Defining it, however, does not lead to contradiction with the axioms, at least not a contradiction you've point out. In fact, most common languages of mathematics cannot even explicitly express the statement "x is not in the domain of f." All they can do is define f(x) for values of x in the domain, and not define f(x) for values outside it. The "exist" in your statement does not refer to ordinary mathematical existence (usually formally expressed with the existential quantifier) but to an informal notion of definedness (discussed by Feferman) that has no formal counterpart in most formal systems, because it is very rarely needed; it is certainly not needed to state the field axioms.
 This is nonsense. If F is a field with elements x, y, then the quotient x/y is equivalent to the product x(1/y). If 0 has no multiplicative inverse, there is no division by 0. The two concepts are one and the same, just as is the case for subtraction and additive inverses. The problem is not that field theory doesn't tell you "what happens" when you divide by 0 - you haven't defined that, there is no what happens because nothing happens at all.You can't engage with the problem because it only exists as a syntactical annoyance. You seem to acknowledge this, but then continue to argue when I explicitly tell you I am in agreement on that point. Then you proceed to argue the theoretical basis all over again.I'm not going to continue arguing this with you. You're presently the only one in this thread who isn't following and I've tried to direct you to other resources. You've alternated between saying those proofs are either incorrect outright or not applicable because they don't have relevance for programming. If you actually believe division by 0 is possible in fields you have an immediately publishable math paper waiting for you to submit it.Otherwise we're just talking past each other because my whole point here has been that the author's discussion of fields is irrelevant for programming language theory in the first place.