[pron]

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.

[throwawaymath]

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.

[pron]

> If 0 has no multiplicative inverse, there is no division by 0. The two concepts are one and the same.

But formalizing the statement "there is no division" poses challenges. If you agree that a formalization of fields that is acceptable to you exists, please write a formal axiom/theorem in that theory which would break if we were to extend the definition of division.

> just as is the case for subtraction and additive inverses.

No, because subtraction is not partial, and therefore poses no challenge for formalization.

> there is no what happens because nothing happens at all.

This is fine when working informally, but doesn't work for formalizations, and formalizations of fields do exist.

> You can't engage with the problem because it only exists as a syntactical annoyance.

But that is the heart of the problem. Either you say one cannot formalize fields at all, or you must admit that some acceptable formalizations do not break. No one is claiming that one should be able to divide by zero in informal mathematics.

> I'm not going to continue arguing this with you.

That's fine, but settling this argument is very easy: write a theorem of fields in a formal language that would break if we extend division, one that cannot be equivalently written in an acceptable formalization in a form that does not break. This can literally be done in one line. If you cannot write such a theorem, then there really is no point arguing, because you cannot provide a counter-argument. Repeating the same informal theorems over and over is indeed pointless.

> You've alternated between saying those proofs are either incorrect outright or not applicable because they don't have relevance for programming.

I've not alternated on anything. Your proofs are incorrect in formal systems that you yourself would find acceptable.

> and I've tried to direct you to other resources

Resources about informal mathematics, on which everyone agrees. That the informal concept of division cannot be extended to 0 is obvious. The only question is whether a formal definition of division would necessarily break formal field theorems if extended to division by zero. You seem to claim that's the case, yet have not stated a single formal theorem of the kind.

> If you actually believe division by 0 is possible in fields you have an immediately publishable math paper waiting for you to submit it.

I would if only that result (doesn't merit a paper) had not already been published by at least Paulson and Avigad, two of the world's best known logicians. The formal field theory in the Lean proof assistant explicitly allows division by zero. That division coincides with the informal division everywhere but at zero, and the extension introduces no inconsistencies to the theory.

> the author's discussion of fields is irrelevant for programming language theory in the first place.

It's not about programming, but about any formalization (which includes, but is not limited to programming).

Anyway, see my comment https://news.ycombinator.com/item?id=17738558, which distills the debate into a concise, precise form.