Post A3FXs1UP4yECHD1vQe by JordiGH@mathstodon.xyz
 (DIR) More posts by JordiGH@mathstodon.xyz
 (DIR) Post #A3FXroHsAFTpKa4Eam by JordiGH@mathstodon.xyz
       2021-01-15T03:00:56Z
       
       0 likes, 0 repeats
       
       I'm having a moment of self-doubt here.I was working yesterday on the book and I couldn't think of a good way to explain that the rationals are incomplete in the sense that there are  bounded sets of rationals with no greatest element and no least upper bound.But my explanation was all very mathematical. Not something I could convey to someone who knows how to code.I know how to code. I think I know a little bit about computer science. I thought I could explain this in the appropriate way.
       
 (DIR) Post #A3FXrw7t1GFHdvSN8a by JordiGH@mathstodon.xyz
       2021-01-15T03:03:12Z
       
       0 likes, 0 repeats
       
       I think of what really delights other programmers. They love, or want to love Haskell. They love logic and set theory. Homotopy type theory is sublime. They want to turn all of mathematics into formal proofs. They ask why can't we define mathematical syntax the way we define a programming language syntax.As I was writing yesterday, all of these sentiments were utterly alien to me. I can't stand the Haskell way of thought. Most of the time I barely tolerate functional programming.
       
 (DIR) Post #A3FXryF39bAECip7a4 by JordiGH@mathstodon.xyz
       2021-01-15T03:03:56Z
       
       0 likes, 0 repeats
       
       I don't want to write proofs as boring and as dry as mathematical programs. I want to write them in natural language! I want to make them fun, and interesting, and maybe even funny!
       
 (DIR) Post #A3FXrzdXy0LyWzICP2 by JordiGH@mathstodon.xyz
       2021-01-15T03:05:58Z
       
       0 likes, 0 repeats
       
       So that's my self doubt.Maybe... maybe I'm not the one who can explain to programmers what mathematics is like. Maybe there's no way I can explain the incompleteness of the rationals via programming analogies.Or maybe.. maybe! I just need to change how I'm thinking and try to think how would I write a program to find the greatest element of the set or the least upper bound and why neither of those programs would ever terminate...
       
 (DIR) Post #A3FXs0VQjfSHE6VEOG by codepuppy@mathstodon.xyz
       2021-01-15T03:11:06Z
       
       0 likes, 0 repeats
       
       @JordiGH   You could practice on me :>I'm a programmer-who-likes-math and doesn't understand this "Incompleteness of Rationals" thing you speak of but wants to :>
       
 (DIR) Post #A3FXs1UP4yECHD1vQe by JordiGH@mathstodon.xyz
       2021-01-15T03:13:54Z
       
       0 likes, 0 repeats
       
       @codepuppy Consider the following set of numbers, of decimal approximations to \(\pi\):\[\{3,~3.1,~3.14,~3.145,\ldots\}\]It is a bounded set, because, say, \(3.2\) is larger than every element of this set.Also, this set has no greatest number. Each of the approximations gets every slightly larger but there is no largest approximation.
       
 (DIR) Post #A3FXs1yBIG2zlYxhqK by JordiGH@mathstodon.xyz
       2021-01-15T03:15:41Z
       
       0 likes, 0 repeats
       
       @codepuppy Now, all of this could be true with the real numbers too. But something is missing in the rationals.This set also doesn't have a *least* upper bound. We found one upper bound, \(3.2\). A smaller upper bound is \(3.15\). An even smaller one is \(3.142\). But there is no smallest rational upper bound. I could write a program to give me ever smaller upper bounds to this set and the program would never terminate.
       
 (DIR) Post #A3FXs2w5hVyAlMzYDw by JordiGH@mathstodon.xyz
       2021-01-15T03:16:25Z
       
       0 likes, 0 repeats
       
       @codepuppy So the point is, in the reals this doesn't happen. Every bounded set of reals has a real least upper bound. In this case, that least upper bound would be \(\pi\).
       
 (DIR) Post #A3FXs4YlfCV9nc5x9E by codepuppy@mathstodon.xyz
       2021-01-15T03:20:43Z
       
       0 likes, 0 repeats
       
       @JordiGH So basically every finite set of rationals has a definite greatest and least element, but not every infinite-set-defined-by-a-computation has a greatest and/or least element that is also (in itself) a rational number?  :D
       
 (DIR) Post #A3FXs7u9EAO0An7ZOC by JordiGH@mathstodon.xyz
       2021-01-15T03:22:02Z
       
       0 likes, 0 repeats
       
       @codepuppy Yes, every finite set of rationals has a least upper rational bound.Some infinite sets of rationals don't have a rational least upper bound.
       
 (DIR) Post #A3FXsALAAhBTj9mAm8 by codepuppy@mathstodon.xyz
       2021-01-15T03:31:15Z
       
       0 likes, 0 repeats
       
       @JordiGH Also my programmer self subjectively feels like this is "caused by" allowing infinite sets to be defined by infinite sequences like this rather than "caused by" the numbers being rational—but that's an entirely subjective feeling and I don't think it affects anything XDAlso I wonder if this means computable numbers are "hole-less"?Finite-digit numbers for finite sets, infinite-digit numbers for infinite sets?  :>(Crudelys-speaking; where repeating digits count as "finite digits")
       
 (DIR) Post #A3FXsCPqSG7MAFywLo by JordiGH@mathstodon.xyz
       2021-01-15T03:33:58Z
       
       0 likes, 0 repeats
       
       @codepuppy The holes in the rationals are caused by allowing infinite sequences of rationals, yeah.But there's also another way in which the rationals are deficient. You can't solve the equation \(x^2 = 2\) in rationals.
       
 (DIR) Post #A3FXsEqVQ6dFhWTGBU by chuculate@anime.website
       2021-01-15T03:59:00.095269Z
       
       0 likes, 0 repeats
       
       @JordiGH @codepuppy I told a friend, "what if √2 didn't exist among the real numbers? What if a (1;1) rect isoceles triangle hipotenuse couldn't be extended and marked on the x axis?"He didn't understand, he didn't even seem to try because, as long as he was concerned, √2 is real.I lost my patience that time.