I might modify this slightly to For any r in R, however large, there exists x in R, and epsilon > 0 in R such that 1/x > r for x < epsilon.
I'm not sure that makes a difference but it may make it clearer. On Mon, Aug 3, 2020 at 11:14 AM Frank Wimberly <wimber...@gmail.com> wrote: > My opinion. 1/0 is undefined. Depending on the context you can define it > in a way that's useful in that context. > > To say that lim(1/x) as x ->0 = infinity means precisely: > > For any r in R, however large, there exists an x in R such that 1/x > r. > > Frank > > --- > Frank C. Wimberly > 140 Calle Ojo Feliz, > Santa Fe, NM 87505 > > 505 670-9918 > Santa Fe, NM > > On Mon, Aug 3, 2020, 11:03 AM uǝlƃ ↙↙↙ <geprope...@gmail.com> wrote: > >> >> 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: >> >> Belief in the Sinularity is Fideistic >> https://link.springer.com/chapter/10.1007%2F978-3-642-32560-1_19 >> >> 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. >> >> 1/0 = 0 >> https://www.hillelwayne.com/post/divide-by-zero/ >> >> Here's the (really uninformative!) SMMRY L7: >> >> https://smmry.com/https://www.hillelwayne.com/post/divide-by-zero/#&SM_LENGTH=7 >> > Since 1 0, there is no multiplicative inverse of 0⁻. Okay, now we can >> talk about division in the reals. >> > >> > 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. >> > >> > We'll define division as follows: IF b = 0 THEN a/b = 1 ELSE a/b = a * >> b⁻. >> > >> > Doing so is mathematically consistent, because under this definition of >> division you can't take 1/0 = 1 and prove something false. >> > >> > 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. >> > >> > 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. >> > >> > Ab = cb => a = c but with division by zero we have 1 * 0 = 2 * 0 => 1 = >> 2. >> >> >> >> [⛧] 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. >> >> -- >> ↙↙↙ uǝlƃ >> >> - .... . -..-. . -. -.. -..-. .. ... -..-. .... . .-. . >> FRIAM Applied Complexity Group listserv >> Zoom Fridays 9:30a-12p Mtn GMT-6 bit.ly/virtualfriam >> un/subscribe http://redfish.com/mailman/listinfo/friam_redfish.com >> archives: http://friam.471366.n2.nabble.com/ >> FRIAM-COMIC <http://friam.471366.n2.nabble.com/FRIAM-COMIC> >> http://friam-comic.blogspot.com/ >> > -- Frank Wimberly 140 Calle Ojo Feliz Santa Fe, NM 87505 505 670-9918
- .... . -..-. . -. -.. -..-. .. ... -..-. .... . .-. . FRIAM Applied Complexity Group listserv Zoom Fridays 9:30a-12p Mtn GMT-6 bit.ly/virtualfriam un/subscribe http://redfish.com/mailman/listinfo/friam_redfish.com archives: http://friam.471366.n2.nabble.com/ FRIAM-COMIC http://friam-comic.blogspot.com/