[FRIAM] actual vs potential ∞

[uǝlƃ ↙↙↙]

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ƃ