This explanation isn't logically complete. It starts by asking why division by zero is undefined and concludes with "0/0 = 2, which is just not true."
But how can it be "just not true"? The point of this exercise was to investigate whether we can find a definition for division by zero, and here we've just produced a candidate! You could just define division by zero to be 2 and move on. To throw away this possibility at this point is to assume the conclusion.
It's not obviously false that 0/0 = 2 (yet).
The problem comes in when you repeat the exercise on a different example and find that also 0/0 = 3, or whatever. And now you start to see something is really amiss.
> The problem comes in when you repeat the exercise on a different example and find that also 0/0 = 3, or whatever. And now you start to see something is really amiss.
I think that this proves that dividing by zero produces the set of all numbers, which is what it looks like to me when you graph this problem (y=1/x) using increasingly small positive and negative values for x. Smaller positive x values tend to positive infinity, smaller negative x values tend to negative infinity. When the x value reaches zero you have a vertical line from positive to negative infinity. ie dividing by zero corresponds to all numbers. That's how it appears to me. So 0/0=2 and it equals 3 etc. I admit this doesn't seem that useful.
The thing about division by zero is that it does not make sense only because you don't know the math to make sense of it.
Math has a long honorable tradition of things that did not make sense until somebody invented the math to describe them.
A inane short list of stuff invented just to deal with results that did not make sense from a person who is terrible at math.
Subtract 5 from 3, the result does not make sense, someone had to invent a whole new category of numbers to handle screw ball results like this.
The square roots of negative numbers. What sort of black magic is this.
divide something by nothing. get out of here you witch. The interesting thing is that the mechanics of computation(which surprisingly has little to do with actual math) has to do something with the operation. My favorite is this one. https://www.youtube.com/watch?v=7Kd3R_RlXgc (curiousmarc)
There are some contexts in which division by zero is defined in a meaningful way. The most common such situation is the real projective line or its complex analogue, the Riemann sphere [0].
We’ll focus on the latter, since it has a richer structure. The Riemann sphere is essentially just the complex plane “closed up” (compactified) by adding a point at infinity. The metric is defined such that points of very large norm are all close to infinity, and hence to one another.
Any nonzero number divided by zero is infinity. Zero divided by zero is undefined. The operation of adding 1 has a parabolic fixed point at infinity.
The Riemann sphere is not a group, but it still has many very nice properties. For instance, the set of analytic maps from the Riemann sphere to itself is precisely the set of rational functions (together with the constant map infinity).
A much more profound statement is Thurston’s characterization of rational functions [1], which states that every orientation preserving branched covering map F from the sphere to itself is equivalent (topologically conjugate) to a rational map on the Riemann sphere, unless F satisfies a certain computable property.
In other words, maps on one of the most ubiquitous topological spaces, namely the sphere, are often best understood by introducing a structure where division by zero is allowed.
While I enjoy your overall tone and enthusiasm, there's no guarantee doing a weird operation will create a new useful mathematical object. The imaginary unit, i, follows associative/commutativity laws etc and is so enshrined. However, defining something like 1/0 as the "zero divided unit" it doesn't follow any of those laws to make it a group etc. So it can't be manipulated like a normal quantity in your algebra. Though it could be manipulated in other algebraic structures, such as wheels. However, if you haven't thought through this before, I think you totally have the right attitude, the right way you want to approach mathematics.
I don't really have the discipline to sit down and actually learn some useful math, however I enjoy the subject at a superficial level, so... that is, everything I say is wrong.
There was an interesting comment in the CouriusMarc video I linked. Quoted in full.
"Folks, no need to argue about colorful alternative mathematical theories - the thorny problem of division by zero was solved for good over 100 years ago by the rigorous development of infinitesimal calculus. Which says: division of a positive non-zero constant by something that tends to zero, tends to infinity [added note: dividing "zero by zero", or more exactly, two things that tend towards zero, is more complicated: it can give zero, infinity, or anything in-between, but that's for another time...]. So the calculator sort of gives the right answer, using almost the correct method: trying to fit an infinitesimally small number into a big one, and finding it fits so many times it goes to infinity. I would put it in the category of happy mechanical accidents."
Which fails to entirely satisfy, I suspect this is because it focuses on the mechanics of one view of the problem and leaves many other views still conflicting. The heart of the problem, that is, why the operation tends to be left as undefined, is that to be mathematically rigorous you have to satisfy all views as to what division actually means.
Yeah, the limit view is only defined in specific cases. For instance, if you have ((x+3)(x-5))/(x-5), this expression evaluates at x=5 to 0/0, but approaching it from either side, evaluates to 8. However, (x+3)/(x-5) at x=5 will be approaching -inf on one side and inf on the other.
I have an anecdote here too. When I learned about automatic differentiation, I very excitedly told one of my formalist math professors about the quantity e, e^2=0, e!=0, and how it could be used to compute the derivative of a function. He couldn't understand and essentially asked me to motivate the number and sketch the proofs that it's a well-behaved extension, which I couldn't do at all at the time, and he dismissed the whole thing which is actually the basis for some pretty important machine learning these days, among other things. So sometimes you can do pretty weird operations to get an extension, but without an intuitive grasp of how it works - either with a proof it is a well -behaved extension or by analogy for example, it's really hard to tell how useful such a concept is to a mathematician, how well it plays by the rules.
Being mathematically rigorous, you will have to define what the views you are talking about. In the one input function limit case, you need to check the limit from both sides. In the 2 input case, you need to check all possible approach paths to prove the limit exists. It gets out of hand. However, these are different views within a formal mathematical system. We don't need to reach consensus among different formal systems which happen to use the same symbols. For instance, I can define the set {cow,0} and equip it with operator '/' such that cow/0= and 0/cow=0 etc. This might be isomorphic to Z mod 2. Then cow by zero is defined, yet we can still agree that division by 0 is undefined, because when we are in general talking about division by 0, we're talking about an operation in a relatively specific context - how numbers behave. So, there really can be a very wide set of perspectives, and being rigorous must also specify the perspectives that count. Also - the cow case is pretty trivial, though this point could also be made with more complex structures, like wheels, that may also have useful physical interpretations, and they still wouldn't affect the collective agreement here because it's a contextually isolated case.
2) ignore (subtract away) the terms not proportional to dx
3) of the terms proportional, only care about terms minimally proportional (i.e. divide by dx, keep terms no longer proportional to dx, eliminate any still proportional to dx.)
The last step corresponds to eliminating terms proportional to dx^2 or higher
You could just as easily have said: You can’t subtract large numbers from smaller numbers because that’s not “natural math”. Extending beyond that will not impact “natural math”.
I am pointing out that calling something “arithmetic” in a narrow sense, then declaring that extended concepts can’t be handled within your previous narrow definition is just a tautology of terminology choice.
Yes, a change is a change. And an extension is an extension.
Even if the modern math notation with a minus sign is a fairly recent invention, subtracting 5 from 3 has made sense to human beings since the dawn of civilization, because that is how debt works.
Math is like a game where you can pick the rules but you have to live with the consequences, and if we choose to define division by zero, a result is that we can prove any number equal to another, e.g. 1 = 2. This ruleset is not fruitful, so we don't do it, but it can be that a new choice unlocks interesting dynamics, like choosing a definition that allows handling roots of negative numbers.
Floating point numbers are more like the extended real line, which has a +inf and a -inf, than the Riemann sphere, which only has the single infinity, that you approach when travelling in any direction away from zero.
This is a really weird thing for someone to say. Everything a computer does is, by definition, proper math. Any system of rules of any kind is math; that's all math is.
Sorry, this is my personal pet peeve: Your using two definitions of math. Let’s call them proper math and using math. Proper math consists solely of tautologies; statements that are always true. Using math is when you make use of these tautologies.
Computers don’t do proper math, they use math. For example: We usually try to remove all tautologies from our programs.
A system of rules is not math. We can sometimes use math to analyze such a system though. For example: Law is a system of rules that’s definitely not math.
> Proper math consists solely of tautologies; statements that are always true. Using math is when you make use of these tautologies.
You forgot about axioms and definitions. If all you have is tautologies, you can never get to the point that 1+1 is 2, because 1 won't have a meaning.
But by the time you're defining objects and their behavior, you've already lost the hypothetical distinction between "proper math" and "using math". There is no such distinction.
Yeah, it’s a simplification. You need to have something to make statements about. But that doesn’t change that what computers are doing is something completely different than what mathematics as a discipline cares about. It’s the same difference as the difference between high school math and mathematics as a discipline. Just because we use the same name for both doesn’t mean they are one.
I find the explanation by limits more convincing. The limit of 1/n as n approaches 0 from the positive direction is a positive infinity. The limit of 1/n as n approaches 0 from the negative direction is a negative infinity. Those are different, the overall limit diverges, so 1/0 is undefined. The same argument applies to all nonzero numbers in glace of 1. 0/n as n goes to 0 does limit to 0 but it's "cleaner" to not have the special case.
On the complex plane, you can take the limit as n->0 of 1/n from any direction on the circle. The Riemann Sphere [1] ties up all these infinities into one and places it at the North Pole, opposing zero which is at the South Pole. Since now all these directional limits converge to the same value, the limit is well-defined in the Riemann Sphere and so we can close it, giving 1/0 the well-defined value of infinity.
It doesn't matter whether the two sides diverge. For the 1/(n^2) function, this is not the case; does that make 1/0 defined if we express it as 1/(0^2)? ;)
What question are we actually asking when we ask “what is 8 divided by 2”? We’re asking “If I have 8 jellybeans and break then into two groups, how many jellybeans are in each group?”
So Consider the question for 8/0: “If I have 8 jellybeans and break them into zero groups, how many jellybeans are in each group?” The question itself is invalid. Answering with any number wouldn’t make sense, the only response that would make sense would be “what do you mean? There are no groups!” It’s almost like it stops being a math problem at all, hence no mathematical answer.
The problem with this explanation is that I should perfectly well be able to divide my jellybeans into 0.5 or -1 groups, though those also make no real sense in this example.
Exactly. And I find this is also the best explanation to give to people who don't have a maths background, but who still want to know "Why does the calculator say ERROR?"
One of my favorite math quotes -- definitions are neither true nor false, they're either useful or not useful.
So this misses it a bit. You can divide 0 by 0 for example and it's 1. In fact you've probably already done it without thinking about it because it's so intuitive.
and 0^0 = 0/0. It's a definition that's useful. If you remember your calculus you probably also remember that inf * 0 is also indeterminate but in measure theory you just define it to be 0 and move on.
Also you can just straight up divide any number by 0 on the Riemann Sphere (the complex
numbers adjoin infinity) and such a construction turns out to be good for modeling real world things.
The floating point numbers adjoin infinity and make some definitions to make them work and it's good because again it's useful for the calculations people want to do.
I get that it's not satisfying but division by 0 is whatever we want it to be because the answer isn't prescribed by the ring axioms. But if you make it too weird it won't by good for anything and every theorem and formula will have to account for your special case.
> But if we have 2 * 0 = 0, the inverse of that would be 0 / 0 = 2, which is just not true.
This is complete non-sense. You defined a number (zero) and defined a relation (2 * 0 = 0). Then you concluded that 0 / 0 = 2 is not true? You could also equally say that 0 / 0 = 2 or any number or non-number really.
The author doesn't explain the argument in detail, but he is trying to say:
when you have "x * y = z" you can perform "x = z / y"
ie: "2 * 3 = 6" therefore "2 = 6 / 3"
But it breaks if you try to do division by zero
ie: "2 * 0 = 0" translates into "2 = 0 / 0", we could assume this is good, but if you use any different value for X, you get other nonsensical answers , say "x = 3" ... so "3 * 0 = 0" therefore "3 = 0 / 0"
So as long as you don't divide by zero, the conversion of "x * y = z" into "x = z / y" will work. If "y" is zero, then the conversion breaks down. Hence division by zero is undefined because there is no correct answer.
----
The other argument one could do, not mention in the article, is the "limit of division by zero", which is a fancy way, what is the result if we don't divide by zero but get close to it.
Say we have number 2, and we keep dividing it by a number that gets closer and closer to zero
2 / 1 = 2
2 / 0.5 = 4
2 / 0.25 = 8
2 / 0.125 = 16
2 / 0.0625 = 32
So as our divisor gets closer to zero, our result gets closer to infinity.
But the problem is, what happens if we approach the zero from the other side,
2 / -1 = -2
2 / -0.5 = -4
2 / -0.25 = -8
2 / -0.125 = -16
2 / -0.0625 = -32
So as the divisor gets closer from the 'left side', from the negative side, the result is going to negative infinity.
This means that there is no convergence because dividing left of zero, and right of zero, leads to different result.
This is same as studying limit of lim of x->0 for cot(x) where the result leads to undefined value because limit approaching from left side does not converge to the limit approaching from the right side.
> This means that there is no convergence because dividing left of zero, and right of zero, leads to different result.
Isn't this related to the reason why if a series can be proven to converge absolutely it's considered convergent? And the simpler tests like comparison, limit comparison, integral test for absolute value by just forcing the expression to be absolute notation?
I always just chalk this up to resolving an ambiguous meaning of "less than", in one sense referring to a relative X position from another spot A on the number line, and another sense referring to a relative X position from zero in either direction.
I was somehow thinking of division by zero in the shower or something the other day, and got something that convinced me about it's undefined-ness.
If we take the equation `x = a/0` and solve for a we get:
```
x = a/0 |*0
a = 0x
a = 0
```
Since `a` could be any number, the statement is false unless `a` is defined as zero or there exists some number `x` which when multiplied by zero does not yield zero.
In this case though, even if `a = 0`, we can't really determine `x` because `0/0` is not something commonly defined in mathematics.
I don't know what the point is of having no apples and no baskets to divide them in to.
In non-standard analysis a whole set of infinitesinal numbers is introduced which are essentially zero. But you can do math with them (including division) and they are very useful for an alternative version of calculus.
My first, empirical answer: physically, dividing a candybar into x parts leaves x parts. Dividing it by 1 OR 0 or -x is not dividing it. You're left with 1 candybar. Infinity? is overthinkig it.
It also depends on how you divide. Dividing the Rosetta Stone into two parts, much information can be lost depending on the orientation of the cut. Say you divide it at a 45° angle from top left to bottom right) might be ok, depending on how much the pieces are separated.
Clearly the simple little word 'divide' is carrying too much weight here. Mathers, feh.
>But if we have 2 * 0 = 0, the inverse of that would be 0 / 0 = 2, which is just not true
By the article's own definition, there are two inversions for each operation so why is only one of them given as "proof"? Taking the other inversion, we have 0 / 2 = 0 which is perfectly correct, and contradicts the claim that inversions "prove" why we can't divide by zero.
Why can't 0 / 0 be defined to be any number you wish? The inversions would work fine.
Eddie Woo has an excellent explanation on this topic [1] that I came across a few years ago. After watching it, I was really questioning why on earth we never had this concept discussed in school, and we were only told that we can't and it's undefined. Other simple math operations like why 0!=1 and e0=1 are cool to explore too.
Because in school, you are still a babbling infant learning to use the new language that you’re learning: mathematics. You don’t try to teach infants who are still on the babbling phase, the complexities of metaphor or nuance.
People have a very funny view of education sometimes. Like, this thing exists, so we should’ve been told about it in school. Like, imagine the consequences of that kind of pedagogy. In order to know something about the subject and be able to learn more about it, you must know everything there is to know about it. Learning is a good example of the hermeneutic circle at work. On first entry into a topic, you don’t know anything and are bewildered by everything. Slowly, you begin to get a foothold where you recognize things vaguely. Then, as you go deeper, your understanding of what you learned at the beginning, also becomes deeper and richer. The simplifications begin to fall away. Complexity emerges, complexity that you are now in a position to handle because you are not completely lost anymore.
İt depends on how number is defined. Euclid defined number as multitude of units. Zero does not have units so zero is not a number and cannot enter arithmetic operations such addition and subtraction. (Division is repeated subtraction.) For the same reason one was not a number in Euclid.
I’m trying to find out when did Euclid lose his authority. By 1901, Bertrand Russell was defining number as an abstract relation, namely, as a one-to-one relation between two sets.
If you have gradient=2, you'll have a line that goes through origin and (1,2).
If you increase the gradient, it'll decrease the apparent 'dy'. You do it until the line becomes vertical, equivalent of dy=0. A vertical line is a valid object, but mathematically, it's no longer a function. You might say your math breaks describing the thing so you'll need a different math.
That’s exactly the point: we want division to model inverses of multiplication, but an inverse requires a 1-1 relationship.
What the vertical line tells us is that division by zero can’t map to a unique value — it has to give us back the whole set. So we can discuss division by zero in the contexts of inverse maps, but there’s no way to have a function that inverts multiplication by zero.
If you try it with long division, you'll notice that the process never terminates, regardless of the digits you put as the answer. It's hardly a rigorous proof, but it's a good hint that something strange is happening.
One of the first functions I define in a new environment/language is div(int m, int n) that returns 0 if n is 0.
Maths apart, is what you want almost always IRL - if you have 0 pages visited out of 0 pages, 0% will do. It saves me from tracking an exception, hamming result that is not an integer and handling the case when printing it. in practice it’s good enough.
Like "division by zero is one and only one of the following: a) zero in the case of 1,273 historical contexts where that answer just made things work out smoothly for everyone involved, b) zero in a new case, pending addition to the official tally in 'a' above, c) infinity, for use in science fiction, or d) undefined."
I have always thought of it as (using people for easier understanding): dividing something to nobody means nothing was divided. Eg. I have to give away 8 apples to 0 people, so no action was taken due to there being no recipients, the whole action was a NOP.
I understand it as num / 1 = num. num / 0.5 = num * 2. Smaller the number I try to divide with, larger the answer. Means closer you get to zero the answer is already too large and at 0 it has to be infinite. The answer can't be just 0 at that point.
The actual reason is asymptotes. I leave it as an exercise to the reader to see what happens as you divide by smaller and smaller numbers as they approach zero.
In calculus you want continuity. You don't want your curve to suddenly jump to some inane location - like zero - as some have suggested for the solution to 2/0.
Tragically this is a blog post where the author clearly doesn't have any math background at all.
The worst part is that they are both, in a critical sense, wrong. There is no absolute 100% universal "right" answer to how division works—it's just a matter of convention! Merely getting into the argument of whether 1/0 "is" 0 is wrong.
There are practical reasons why we leave division by 0 undefined in "normal" arithmetic but we could, just as easily, operate in a world where 1/0 is defined. In some contexts, 1/0 = 0 is a totally sensible convention! In others, we can define it to be ∞ or, hell, something else entirely.
This approach of teaching math as a bunch of universal facts that are either true or false is actively harmful—but super convenient for top-down education and assessment!—because it teaches people the wrong way to think about math or even about conceptual models in general.
Yet we can still plainly declare that the teacher is incorrect, unless we missed the part of the story where they were discussing floating point arithmetic, or the extended complex plane, or some other deliberate definition unrelated to the arithmetic of the reals.
Of course it’s a matter of convention. But it’s a convention without which the rest of mathematics taught to school children throughout the world falls apart.
Calling the color of the sky blue is just a matter of convention as well, but if one random teacher starts calling it green, she’s doing a terrible disservice to her students. It doesn’t matter that there exists some languages without a difference between blue and green.
What is the application for 1/0 = 0? Where is this used? Does it actually make a meaningful appearance outside of drunken barroom conversations, and classrooms staffed by clowns?
If you know more than others, that's great, but in that case the thing to do is to share some of what you know, so others can learn. If you don't want to do that, that's fine, but in that case please don't post. Putdowns and swipes only degrade the discussion.
> The worst part is that they are both, in a critical sense, wrong.
I thought the worst part is that in context of "normal" mathematics taught in schools one is obviously wrong, and also unable to do research and admit own mistakes, and that one is actually teaching children.
> This approach of teaching math as a bunch of universal facts that are either true or false is actively harmful
Kids are taught not philosophy or logic but certain mathematical paradigm (that you call "normal") in which division by zero is an error. If you have a formula you decompose it to smaller formulas, if in a smaller formula you have a division by zero you simplify it to zero then you screwed up the entire thing. There's no true or false value for 1/0, the right move is not to play and not solve any equation in which division by zero appears.
I taught a friend's elementary aged kid that 1 + 1 = 10, who then got into trouble for arguing with her teacher. Even after saying that 1+1=10 in binary, she got in trouble for being argumentative even if she wasn't wrong. Apparently, making the teacher look bad in front of the class is frowned upon.
As someone studying education... you're right, but you're also kind of a prick.
Actually, let me rephrase. It's a bad situation all-round. I assume you didn't tell your friend's kid to go in and argue with her teacher. (If you did, then you are a prick. Otherwise, I rescind the above.) At that age, kids want to tell people when they learn fun or exciting things (well, that's not really restricted to that age), but they don't always think through the effects of saying them. Now, I definitely do know a number of elementary teachers who aren't great at math, but even if the teacher is good at math, imagine their perspective. Off the top of my head, I can only think of a small number of options: 1. agree, move on, and have a bunch of kids who are either confused or are going around telling everyone they know "1 + 1 = 10" without understanding why; 2. scrap whatever lesson they were supposed to do and go into a long, unplanned explanation of how different number bases work and interact with place value; 3. tell the girl she's wrong. Quite frankly, none of these are good options.
I can't really fault you for teaching her fun math, but for an elementary teacher that's a really rough spot to be put in.
And yes, letting everyone be argumentative all the time is how classroom management goes out the window.
A big issue in the west is the school system will put lot of effort trying to teach children it deems "special need" but will shut down ASAP the ones curious enough to learn something outside the curriculum. Fact is, school is where intellectual curiosity goes to die.
yes, i'm a prick for exposing curious kids to stuff outside of their class' curriculum. heaven forbid someone providing learning more advanced than the other students.
it's people like you that are pricks for thinking that anyone with extra learning are punishing everyone else in class. it's never a problem for keeping students ready to advance faster than the rest of class keeping them all held back at the slower pace.
you're also a prick for assuming the way the conversation came about. you're a prick for not thinking that the conversation was about how math can be fun where things that are simple and considered basic can be different and more advanced where 1+1=2 can also be 1+1=10. but now, you just go off and assume i'm a dick saying 1+1=2 is wrong and the correct answer is 1+1=10 or whatever nonsense led you to thinking i'm a prick.
i'm going to go out on a limb and say that starting a conversation by calling someone a prick is just not going to be received well. at. all.
how about teachers should be much less aggrieved that an elementary student is probably smarter than they are. when a student shows initiative to learn something on their own, rather than being an ignorant person and send the kid to the principal's office because they think the kid made a bomb or is learning maths at a pace faster than the hayseed teacher is.
see, that whole paragraph has a point that would probably be made much more acceptable if I didn't phrase it in an insulting manner
I feel like a proof assistant is amongst the worst places to have something like this rather than (I don’t know how lean works) raising an error. What are the justifications for this convention?
But there's a single crucial difference: in programming, the "do something" is really important, whereas in Lean, the "prove something" isn't important at all: as long as the typechecker is happy with it, everyone can forget about it once it's written.
So as long as your assumptions and conclusion don't involve any division by zero, it doesn't matter what goes on inside the proof.
Regarding division by zero, you sort of have three options:
* Output an error / checked null when there's division by zero.
* Require a proof that the denominator is nonzero before you're even allowed to use division.
* Allow division by zero, making it return some nonsense. Then, add an assumption that the denominator is nonzero to all your theorems about division.
The first two options (especially the second one) make the definition of functions that involve division horrifically messy. (Idk, it might be easier if Lean had exceptions, but that also sounds messy.) I think that's why Lean goes with the third option.
You typically can't "raise an error" in such contexts in formal reasoning tools. There's no "runtime" per se to raise an error from -- the expressions themselves are manipulated to derive truths -- the division by zero may simply be implicit e.g. in a statement about division by some arbitrary number.
Trying to solve the problem with e.g. dependent typechecking quickly gets complicated (both implementation and theory). And adding a concept such as infinity may complicate proofs which now need to deal with infinity being a "number" but which behaves differently from other numbers.
Thankfully mathematics has the nice property that you can define concepts any way you want so long as they're self-consistent and match one's expectations. So rather than treating division by zero as an exceptional case -- either by disallowing it in the typesystem, "raising an error", or by introducing a "special" value -- some (most?) verification languages simply define division by zero to have a numeric value, and make it known that this is the case. Users know that they must then write expressions to be explicit about division by zero if they care about that case. (This turns out to be not much different than having to write expressions to satisfy a dependent type system.)
((x / y) * y) = x is not a true statement about real numbers, regardless of if division by zero is defined as an error or as being equal to 0. The true statement is ( y != 0 -> ((x / y) * y) = x ), and this holds no matter how you define division by zero.
More generally, in normal math, every theorem that involves division by some value Y which could be zero must have as hypothesis that Y is not equal to zero. All these theorems still work in systems like Lean where division by zero is defined to be zero, so nothing is lost.
> You typically can't "raise an error" in such contexts in formal reasoning tools.
You could write all your formulas in the Maybe / Option monad (which I guess is the same as 'introducing a "special" value') but that sounds painful...
> There are good reasons for this convention in the context of Lean
There are good reasons for the convention of assigning nonsense values to computations that are formally invalid. The convention is so important that it is introduced in the Natural Number Game, where the remarks include a brief discussion of why the predecessor of 0 is defined to be 37.
I don't think there's any particular reason why you'd assign 0 as the nonsense value?
But how can it be "just not true"? The point of this exercise was to investigate whether we can find a definition for division by zero, and here we've just produced a candidate! You could just define division by zero to be 2 and move on. To throw away this possibility at this point is to assume the conclusion.
It's not obviously false that 0/0 = 2 (yet).
The problem comes in when you repeat the exercise on a different example and find that also 0/0 = 3, or whatever. And now you start to see something is really amiss.