FOUR. I just posted FOUR topics.

This is a fun read. In our recent conversation I was lazy and equated division with multiplication by the inverse; this person is more of a stickler than me, and is right to be so.

The fact that we should have, symbolically, 1/0 = 1/0, is particularly amusing. In IEEE floating pointing, 1/0 resolves to NaN, Not-a-Number. Multiple bit-strings are defined as being NaN (I forget if these correspond to different error codes, or whether there's some flexibility to make implementation easier). However, NaNs are defined as having the very weird property of not being equal to themselves This leads, bizarrely, to the implementation of Java's Double.isNaN(double x) being x != x.

There is a bit of a bait and switch here, though:

Since this form of division is not defined for 0, it is a partial function over the reals: there is some value in its domain that we have not specified. Practically, this is fine: we're used to thinking of 1/0 as an impossible operation. But this has some weird consequences: one of our axioms is everything is equal to itself. So does 1/0 = 1/0? If you say that's silly, we no longer have a = a!

No, that's not a weird consequence of it. 1/0 is meaningless. Function notation is syntactic sugar for a set of ordered pairs (in one construction of mathematics!). If f is defined only on the reals, f(1+i) is meaningless as none of its ordered pairs have 1+i as the first element. Likewise, if division is a partial function on R^2, for every x the division set does not contains ((1,0),x).

Of course, for any extension of division to cover the entirety of R^2 (or Q^2, etc.), it is true that 1/0 = 1/0.

They make a good point about the typing of head. There are trade-offs in doing this, and in practice I'd probably feel unnecessarily wary.

Algebra does not equal programming, despite their happy co-dependent relationship. You only get one with the other, so to speak.

Better metaphor: Programming is the cranky uncle/aunt of maths. The one who is smart and very logical and also always wants to tell you about their new insight into base layer things that don't make sense when you just remove X as an assumption (it's always YOUR assumption).

Best to pat them on the head for really opening your eyes and move on...

Wait until this explorer discovers the Riemann series theorem.

The idea that we're throwing continuity out the window annoys me. 1/$\epsilon$ should be close to 1/0.

Oh, don't you know? As you move arbitrarily far away from the origin, you get arbitrarily close to 19.

Anyway, the programmer lolz seem a bit uncalled for, because 1) computer science is not programming, and 2) a bunch of proof systems support this. This is a logistician's game, not a programmer's.

Logistician? Logician. It's Monday.

I just posted FOUR topics

You already got enough credit for the last group of four things you produced.

As you move arbitrarily far away from your base of supply, your stocks get arbitrarily close to 0.

For some reason I always thought the Bard's Love Minus Zero/No Limit was a reference to division by zero.

And I though the Oxfordian theory was ridiculous.

8: and as he says, he asked several math folks to look it over.

Heebie, is it less continuous this way? 1/epsilon isn't close to "not defined", is it?

It's totally less continuous, because in the usual case division is continuous on its entire domain.

Seems like a trick!

10: Was it Kittens? or Snakes? are they loose in the house????

I didn't really get much out of this article. Sure you can define a function however you'd like if you don't care what properties it has! You could define 5/7 to be 0 too if you wanted. What I don't understand is why you'd want to define x/0 = 0. The people making Coq and Lean are smart people, so I'm sure there's some reason, but this article doesn't touch on it at all.

8: I didn't mean this specific programmer, specifically, just in general. Given [author] is a programmer, without math background, it doesn't seem like lulz to quip about. [x] is exploring and I read the article. Seems fair to me.

But you couldn't, because 7 has a multiplicative inverse? The whole point was that you can do this while preserving division's properties (those which were enumerated anyway).

18:Buffer overruns. IT'S ALWAYS THE BUFFER OVERRUNS.

You'd still have versions of those properties, if you simply check that the numbers involved weren't 5 and 7.

You'd still have versions of those properties, if you simply check that the numbers involved weren't 5 and 7.

You could define 5/7 to be 0 too if you wanted.

There's some funny apocryphal story about ill-suited names for things and all I remember about is that it started, "Let 6 be a group..."

Heebie, is it less continuous this way? 1/epsilon isn't close to "not defined", is it?

When pressed on what "infinity" means, I usually say "it's a direction, not a number", which is useful here for seeing how 1/epsilon approaches infinity as epsilon goes to zero. Or, the extended real line is nice too.

What does he want to define 2/2 mod 6 to be? 0 again? 1? 4?

Working in logic, I would expand out the statement that a function is continuous everywhere like this:

forall x. f is continuous at x
forall x. forall y. forall e. exists d. |x-y| < d => |f(x)-f(y)| < e

So there's a question now of how to treat this. Are functions sets of ordered pairs, or should we use the function symbols built in to most logics? As far as I can recall, the function symbols don't allow partial functions, so that makes them ill-suited for this approach. If we take the former approach, I'd expand it out as

forall x. forall y. exists z. exists w. (x,z) in f and (y,w) in f => forall e. exists d. |x-y| < d => |z-w| < e

which regular division satisfies (with any value you'd like for z when x = 0), and wacky 19=1/0 division doesn't.

I like to assume e = pi. It makes things easier.

I had a cat named Epi, but that's not why.

Also all the stuff about fields in the post just reads to me as "see I do know math!"-defensiveness, and doesn't really add anything to the argument.

My son is personally offended by i.

31: Teach him about Galois and field extensions, and why it's more important to be good at dueling than good at math.

I'd be much happier defining x/0 = 17. At least then you're unlikely to accidentally have equalities work out, and when you debug and suddenly think "why are these 17s here?" you can remember "oh yeah, I made x/0=17 for some reason" and find the source of the error.

How about 16.8?

Round numbers make people suspicious.

31: Not a fan of e.e. cummings?

Anyway, that 0/0 != 1 in that formulation makes it pretty worthless. You still have cases where you'd have to special case for zero, even for purely algebraic concerns. Multiplying by a form of 1 should be safe and useful.

Round numbers make people suspicious.

17 is way less round than 16.8. Look at all those curves.

You'd still have versions of those properties, if you simply check that the numbers involved weren't 5 and 7.

The point is that you don't need "versions" of those properties with the extension in the article. You have the same properties, because they were already, quite reasonably, formulated so as not to apply to division by zero.

Also all the stuff about fields in the post just reads to me as "see I do know math!"-defensiveness, and doesn't really add anything to the argument.

What do you think the argument even is?

What do you think the argument even is?

It's not good to be smug, because you're bound to be wrong sooner or later.

What do you think the argument even is?

Also, numbers are surprisingly complicated.

The argument is that if you have a function that's partially defined, then you can extend it everywhere in any way you like, and any statement about the original function will still hold so long as you restrict said statements to the original domain. It has nothing to do with multiplication, division, or fields.

Infinity divided by zero is the same as infinity squared.

So, two divided by zero is four.

Which journal should that go to?

Pacing!/0

There was an interesting, if depressing, story by Ted Chiang where a mathematician finds an obscure corner of mathematics where all the assumptions break down and you start being able to prove a = -a, forcing the understanding that mathematics is fundamentally a set of parlor tricks that is useful in real life but has no transcendent unity or meaning. It makes her suicidal.

That's what I was reminded of when I got to "It turns out that for certain choices of C, specifically 0, we can make some theorems stronger." Probably inappositely, as I don't think I actually understand this.

Isn't it assuming part of its conclusion with axiom 9, "Every element EXCEPT 0 has a multiplicative inverse"? Why must that be an axiom?

I said this in a previous thread that I'm too lazy to look up, but assume zero has a multiplicative inverse, Z. You're going to get the problems that people think of when they hear "division by zero."

0 = 0 (Reflexivity oof equality)
0 + 0 = 0 (Additive identity)
(0 + 0)*Z = 0*Z (Easy equality theorem)
0*Z + 0*Z = 0*Z (Distributivity)
1 + 1 = 1 (Z is multiplicative inverse of 0)
1 + 1 - 1 = 1 - 1 (Easy equality theorem)
1 + 0 = 0 (Additive inverse)
1 = 0 (Additive identity)

It's taken as an axiom that 1 != 0, but if you don't take that as an axiom, you can then show that for all x, x = 0:

1 = 0
1*x = 0*x
x = 0

So therefore you must be in a trivial, single-element space.

For what it's worth, there are a few places in the fundamentals of mathematics--sometimes philosophically, sometimes logically--where we aren't on as firm of ground as we'd like to be. But I think most people who think about that sort of thing aren't very worried about it.

But I think most people who think about that sort of thing aren't very worried about it.

Presumably because they also have real worries like toothaches, disobedient children, mortgage payments etc.

Honestly, having bought fifteen years ago really helps with one worry.

What do you think the argument even is?

Talk less, smile more.

I think it was a more popular thing to worry about in the first half of the 20th century (somebody with a better sense of the history here, please chime in). There was a lot of work that had to be done to get people to be comfortable, especially after Erdos changed everything.

s/Erdos/Godel/, jeez! They're both mathematicians with names that are five letters long and have a diacritic I tend to omit.

Isn't that the name of the super-trippy book from when I was 14?

25. One complication with the idea that 1/0->inf is that one needs to decide on which infinity, whether +inf, -inf, or complex-inf.

I just assumed epsilon was approaching zero by swirling around the complex plane as |ε|e^i/|ε| where |ε| → 0, and then restrict it to the positive reals. Why borrow trouble?

This guy. This guy. What a bullshit artist. Let me quote from https://tutorial.ponylang.org/gotchas/divide-by-zero.html

In Pony, integer division by zero results in zero. That's right,

let x = I64(1) / I64(0)

results in 0 being assigned to x. Baffling right? Well, yes and no. From a mathematical standpoint, it is very much baffling. From a practical standpoint, it is very much not.

Similarly, floating point division by zero results in inf or -inf, depending on the sign of the numerator.

I search his essay, for the words "integer", "real" and "floating". No instances other than "real math" (and its variants). He's cleverly (maybe even to himself) obscured the distinction between these two kinds of division. Oh, and: his "real mathematicians" are Paulson (computer scientist and mathematical logician), Lamport (computer scientist) and two Haskell/Coq guys who might have been mathematicians, but are today CS types.
This is .... underwhelming evidence that mathematicians agree with him. And why? B/c (setting aside Lamport, who's a CS guy thru and thru) they're mathematicial logicians. And that's like mathematics, in the way that pr0n is like a real sexual relationship. Crikey, it's so embarrassing.

If he'd said:

I've defined this function div1(x) =def= if x == 0 then 1 else 1/x, aren't I clever? It's almost like division, but it has this neato special case!

P.S. I lived in that world (of formal methods, constructivism) for a decade. I wrote Coq V5.10.
P.P.S. He says "do not mock other programmers". And yet, the people who defined the ANSI floating point standard are almost *certainly* more "real" programmers than the constructivists and logicians he cites.

I don't think the distinction between integer and floating point math really matters much to his point. And it's possible that the original tweeter is the one who scrubbed the distinction, or that the Pony maintainers changed it since that tweet. Here's the tweet, so the lack of reference to non-integer math is not on the blogger. (And honestly, getting a lot of attention via a viral tweet is a good reason to clarify your documentation.)

I disagree with the implementers of Pony that this is practical. Putting on my programmer hat, if I divide by zero, even integer zero, I probably screwed up and would like to fail fast via an exception or similar means. Even if we can extend the division function a value that doesn't lead to inconsistencies when we work in the restricted domain, it doesn't let me know when I've walked off the edge of the map.

I feel like the hypothetical quote you give is basically what he's saying? He's only referencing experts just in case you don't believe his arguments about consistency hold.

||

Quite the comedy-of-manners shaping up between Azalea Banks, Grimes, and Elon Musk.

I guess when people get super-rich enough they revert to the Wodehouse materteral-estate model where nodding acquaintances might stay for days on your whim.

|>

I was actually thinking earlier today "this would make way more sense if he were talking about integer division." The point is integer division a/b is really giving you the quotient (which is an integer) and a remainder which is maybe an integer but maybe is better thought of as a congruence class modulo b. The key relationship is a = bq + r. If b is zero then r lives in the integers mod 0, and so is just a, which means a should be zero. It's very defensible to say integer division by 0 gives 0, and totally nutty to say real division by 0 is 0.

There's a related error in his twitter which is claiming there's no justification for 0^0=1. That's true for real exponentiation, but for integer exponentiation there's an easy reason: a^b is the number of maps from an a element set to a b element set. So 0^0 is the number of maps from the empty set to itself, which is certainly 1.

Sorry there's errors in my comment. At any rate, for integer division any quotient makes sense (a = 0 q +a works no matter what q is), while for real division no quotient makes sense (you can't have 0 x/0 = x).

I'm not sure what to think about the link in the post.

I had trouble figuring out the types he was talking about. Integers or rationals? I don't think reals or IEEE 754 floats work.

There is a point to getting your definitions so your theorems don't have special case clauses.

Sorta on topic - were there mathematicians before the 19th century who worked out non-Euclidean geometries but could not accept them as consistent because of the surprising consequences?

Yes. That was Rule 33.

61: Or alternatively there's a quotient that makes sense for every value except 0/0, and you've just reduced your number of undefined cases from uncountably infinite to one.

Good point on integer multiplication, though.

The 0^0 thing was a question on a test I had to take for placement in my engineering school, and I remember being intensely frustrated by it--I had a very bad memory back then, and I couldn't figure out how to derive from first principles which function to make discontinuous.

Maybe I am being silly about types.

The author of the linked story explicitly distinguishes between the multiplicative inverse of 3 and 1/3. He wants to have a theorem that connects them, with a clause in the theorem about zero. But he starts with a field, not a commutative ring with unity.

If you enjoyed this you'll love this:

https://aip.scitation.org/doi/full/10.1063/1.4940236

It turns out loss aversion is only a thing if you assume wealth doesn't compound and running out of cash isn't a problem - and the source of the silly assumptions is that economists didn't integrate non-ergodicity when that became a thing in the 19th century. Also, Bernouilli got his sums wrong and nobody noticed.

Fortunately it was the gambling problem rather than aerodynamics:-)

I'm not sure whether to be sad or happy that my company blocks the domain of the OP link.

Incidentally, Floats/Doubles are not Rational Numbers, they are Integers in drag.

48: My math is old (in the years sense) but this one stumped me.

0*Z + 0*Z = 0*Z (Distributivity)
1 + 1 = 1 (Z is multiplicative inverse of 0)

Isn't multiplicative inverse applicable only to non-zero stuff?

67: You'd think getting up in drag would make them better at associating, not less.

68: Yes, it is. This was explicitly assuming that such a multiplicative inverse exists, to see the weird state it gets you in. (It isn't quite a proof by contradiction, if you're willing to accept that sometimes 1 = 0.)

Thanks! Weirdness is inherent when the OP is just ignoring stuff for his field then we use non-field properties.

I mean the whole OP boils down to computers don't like dividing by zero because it causes blue screens of death, does this mean zero is divisible? Some thoughts!!!!

I had the same reaction as 18 -- I don't really get the point. You necessarily have either a partial function that satisfies all the equations that you'd like, and a total function that doesn't. In either case the fact that the equations don't hold unconditionally will sometimes bite you.

In primitive recursive arithmetic, which is only defined for natural numbers, you define 0 - 1 to be 0. Why? Because for this setting it's easier to work with total functions.

FORTRAN defined 1/0 as 0 for years. So did most machine languages. Of course the set of integers from 0 to 2^N-1 isn't a ring. Nowadays, 1/0 triggers an error to be handled as an exception, either that or it returns NaN which is IEEE for not a number.