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