Timeline for Proof in constructive mathematics that the principal square root function exists in any Cauchy complete Archimedean ordered field
Current License: CC BY-SA 4.0
17 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 12, 2024 at 21:50 | comment | added | Christopher King | Do you think $\lim_{N \to \infty} \sqrt{x+\frac 1N}$ would work? | |
| Jul 6, 2022 at 20:14 | comment | added | François G. Dorais | However, after a quick look, it seems that Booij does actually mean with a modulus of convergence since that is what the propositions-as-types interpretations yields. | |
| Jul 6, 2022 at 20:05 | comment | added | François G. Dorais | @Gro-Tsen: I usually assume the latter, unless otherwise specified. However, the first appears to be sufficient for my answer since I could produce a uniform modulus of convergence at the two places I use it. I don't think univalent type theory changes much here. | |
| Jul 6, 2022 at 19:59 | comment | added | Gro-Tsen | @FrançoisG.Dorais I know nothing about univalent type theory, but I imagine any constructive math framework that doesn't have countable choice would distinguish “Cauchy sequence with a modulus of convergence” ($∃h:ℕ→ℕ.∀m:ℕ.∀p,q≥h(m).(|u_p-u_q|<1/m)$) and “Cauchy sequence not assuming a modulus of convergence” ($∀m:ℕ.∃N:ℕ.∀p,q≥N.(|u_p-u_q|<1/m)$): which is meant when speaking of “Cauchy completeness”? | |
| Jul 6, 2022 at 16:10 | history | edited | user483446 | CC BY-SA 4.0 | added 169 characters in body |
| Jul 6, 2022 at 15:58 | comment | added | user483446 | @Gro-Tsen in type theory one could directly construct the initial Cauchy complete Archimedean ordered field: etheses.bham.ac.uk/id/eprint/10411/7/Booij2020PhD.pdf | |
| Jul 6, 2022 at 15:50 | comment | added | François G. Dorais | @Gro-Tsen I don't think DC matters here since the question assumes that there happens to be a Cauchy complete Archimedean ordered field, not that any specific construction gives such a field nor that there is only one such field. | |
| Jul 6, 2022 at 15:06 | comment | added | Gro-Tsen | You need to specify whether you allow dependent/countable choice in “constructive mathematics”, and, if not, what “Cauchy sequence” means (do you assume a modulus of convergence?), because, as you probably know, the Cauchy reals can fail to be Cauchy complete, which makes the whole notion of Cauchy completeness rather dubious in value, to say the least. | |
| Jul 6, 2022 at 12:54 | answer | added | Neil Strickland | timeline score: 6 | |
| Jul 6, 2022 at 10:26 | history | became hot network question | |||
| Jul 6, 2022 at 6:16 | vote | accept | CommunityBot | ||
| Jul 6, 2022 at 6:05 | answer | added | François G. Dorais | timeline score: 9 | |
| Jul 6, 2022 at 5:51 | history | edited | user483446 | CC BY-SA 4.0 | added 568 characters in body |
| Jul 6, 2022 at 5:05 | comment | added | user483446 | @FrançoisG.Dorais According to mathoverflow.net/questions/302037/… the principle of unique choice should be valid in my variety of constructivism. | |
| Jul 6, 2022 at 3:12 | comment | added | François G. Dorais | Is definite description (aka unique choice) valid in your variety of constructivism? | |
| Jul 6, 2022 at 2:24 | history | edited | user483446 | CC BY-SA 4.0 | added 213 characters in body |
| Jul 6, 2022 at 2:19 | history | asked | user483446 | CC BY-SA 4.0 |