<div dir="auto">My opinion.  1/0 is undefined.  Depending on the context you can define it in a way that's useful in that context.<div dir="auto"><br></div><div dir="auto">To say that   lim(1/x) as x ->0 = infinity means precisely: </div><div dir="auto"><br></div><div dir="auto">For any r in R, however large, there exists an x in R such that  1/x > r.</div><div dir="auto"><br></div><div dir="auto">Frank<br><br><div data-smartmail="gmail_signature" dir="auto">---<br>Frank C. Wimberly<br>140 Calle Ojo Feliz, <br>Santa Fe, NM 87505<br><br>505 670-9918<br>Santa Fe, NM</div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, Aug 3, 2020, 11:03 AM uǝlƃ ↙↙↙ <<a href="mailto:gepropella@gmail.com">gepropella@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br>
I know I've posted this before. I don't remember it getting any traction with y'all. But it's relevant to my struggles with beliefs in potential vs actual infinity:<br>
<br>
  Belief in the Sinularity is Fideistic<br>
  <a href="https://link.springer.com/chapter/10.1007%2F978-3-642-32560-1_19" rel="noreferrer noreferrer" target="_blank">https://link.springer.com/chapter/10.1007%2F978-3-642-32560-1_19</a><br>
<br>
Not unrelated, I've often been a fan of trying identify *where* an argument goes wrong. And because this post mentions not only 1/0, but Isabelle, Coq [⛧], Idris, and Agda, I figured it might be a good follow-up to our modeling discussion on Friday, including my predisposition against upper ontologies.<br>
<br>
  1/0 = 0<br>
  <a href="https://www.hillelwayne.com/post/divide-by-zero/" rel="noreferrer noreferrer" target="_blank">https://www.hillelwayne.com/post/divide-by-zero/</a><br>
<br>
Here's the (really uninformative!) SMMRY L7:<br>
<a href="https://smmry.com/https://www.hillelwayne.com/post/divide-by-zero/#&SM_LENGTH=7" rel="noreferrer noreferrer" target="_blank">https://smmry.com/https://www.hillelwayne.com/post/divide-by-zero/#&SM_LENGTH=7</a><br>
> Since 1 0, there is no multiplicative inverse of 0⁻. Okay, now we can talk about division in the reals.<br>
> <br>
> So what's -1 * π? How do you sum up something times? While it would be nice if division didn't have any "Oddness" to it, we can't guarantee that without kneecapping mathematics.<br>
> <br>
> We'll define division as follows: IF b = 0 THEN a/b = 1 ELSE a/b = a * b⁻.<br>
> <br>
> Doing so is mathematically consistent, because under this definition of division you can't take 1/0 = 1 and prove something false.<br>
> <br>
> The problem is in step: our division theorem is only valid for c 0, so you can't go from 1/0 * 0 to 1 * 0/0. The "Denominator is nonzero" clause prevents us from taking our definition and reaching this contradiction.<br>
> <br>
> Under this definition of division step in the counterargument above is now valid: we can say that 1/0 * 0 = 1 * 0/0. However, in step we say that 0/0 = 1.<br>
> <br>
> Ab = cb => a = c but with division by zero we have 1 * 0 = 2 * 0 => 1 = 2.<br>
<br>
<br>
<br>
[⛧] I decided awhile back to focus on Coq because it seems to have libraries of theorems for a large body of standard math. But still NOT having explored it much, yet learning some meta-stuff surrounding the domain(s), I'm really leaning toward Isabelle. I suppose, in the end, I won't learn to use any of it, except to pretend like I know what I'm talking about down at the pub.<br>
<br>
-- <br>
↙↙↙ uǝlƃ<br>
<br>
- .... . -..-. . -. -.. -..-. .. ... -..-. .... . .-. .<br>
FRIAM Applied Complexity Group listserv<br>
Zoom Fridays 9:30a-12p Mtn GMT-6  <a href="http://bit.ly/virtualfriam" rel="noreferrer noreferrer" target="_blank">bit.ly/virtualfriam</a><br>
un/subscribe <a href="http://redfish.com/mailman/listinfo/friam_redfish.com" rel="noreferrer noreferrer" target="_blank">http://redfish.com/mailman/listinfo/friam_redfish.com</a><br>
archives: <a href="http://friam.471366.n2.nabble.com/FRIAM-COMIC" rel="noreferrer noreferrer" target="_blank">http://friam.471366.n2.nabble.com/<br>
FRIAM-COMIC</a> <a href="http://friam-comic.blogspot.com/" rel="noreferrer noreferrer" target="_blank">http://friam-comic.blogspot.com/</a> <br>
</blockquote></div>