Talk:Existence of Square Roots of Positive Real Number
Possible mistake, more likely omission
I attempted to formalize this proof in the Dafny verification programming language. I was able to get it to verify using one assumption. However, ideally there should be a way to remove the assumption/axiom and verify using only the completeness axiom. https://github.com/hath995/Dafny4.4/blob/main/realAnalysis.dfy#L219
Basically, for the case of $u^2 > r$ basically it boils down how to we know that $u - \dfrac 1 n \ > 0$?
- Because $u - \dfrac {u^2 - 2 r} {2 u} = \dfrac {u^2 + 2 r} {2 u} > 0$ and so $\dfrac 1 n < \dfrac {u^2 - 2 r} {2 u} < u$ and so $u - \dfrac 1 n > 0$. --prime mover (talk) 15:05, 15 February 2024 (UTC)
How much bigger is $u^2$ than r? Is it less than 1, because r+1 is the only other upper bound mentioned? How do we show that though?
- Why do we need know? The argument works however big $u^2$ is. The only reason we invoked $r + 1$ is to establish that $S$ has an upper bound. --prime mover (talk) 15:05, 15 February 2024 (UTC)
Another line of reasoning seems to be that $u - \dfrac 1 n > r$ which would make it an upper bound and it would be less than $u$ which would lead to contradiction. However, given $u^2 >r$ that doesn't imply that $u > r$.
- If you can craft another proof, then go to it. --prime mover (talk) 15:05, 15 February 2024 (UTC)
- Oh, and please sign your posts. --prime mover (talk) 15:05, 15 February 2024 (UTC)
Lol, I don't know why I didn't think about actually just subtracting and seeing the result. That was what I needed, the proof verifies now. My implementation can definitely be cleaned up and simplified some but it is nice to see it verifies even though it is not exactly pretty.--Hath995 (talk) 16:30, 15 February 2024 (UTC)
- I've added that basic bit of clarification. I think it's fairly solid now. Thanks for your contribution. --prime mover (talk) 16:15, 16 February 2024 (UTC)
Welcome, one detail I had to fill for the formalization is for the case of $u^2 < r$ was if $u \le 0$. For negatives it was clearly not an upper bound of S. For $u = 0$ then I had to make an argument based on the value of $r$ if $r > 1$ then $1 \in S$ and so $u$ is not an upper bound, if $r < 1$ then $r^2 < r$ which implies $r^2 \in S$ therefore $u$ is not an upperbound. --Hath995 (talk) 16:42, 16 February 2024 (UTC)
Possible mistake
There is a comment on Math Stack Exchange stating that a part of this proof is incorrect. Basically, $u + \frac 1 n$ may not be rational. Is anyone willing to check it out?--Julius (talk) 11:13, 7 October 2022 (UTC)
- Yes I see now, that last line $u + \dfrac 1 n \in S$ is a mistake. But it's simple to fix, we just need to invoke the fact that because $u + \dfrac 1 n < r$ then $\exists m \in S$ such that $u + \dfrac 1 n < m < r$ which can be done from Between two Real Numbers exists Rational Number. Oh, and there's also a couple of instances of $4 u$ which I think may need to be $2 u$, but I haven't studied it carefully enough to be sure about that.
- I don't have the time to do this immediately (shouldn't really be doing this, I'm supposed to be debugging an app right now) so if anyone else is up for it, let them. --prime mover (talk) 11:30, 7 October 2022 (UTC)
- I think I might have been getting confused with something I'd read about Dedekind cuts and the proof of the existence of the square root of $2$ from the existence of the rational numbers. Or something. --prime mover (talk) 21:18, 7 October 2022 (UTC)