Earlier quoted context omitted.
> 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 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. Dif…
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.