Timeline for Is any Cauchy sequence for completion of rational semicomputable?
Current License: CC BY-SA 3.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 21, 2017 at 8:07 | comment | added | Andrej Bauer | Right. Without countable choice you can't show that the Cauchy completion of rationals is Cauchy complete. You need to keep completeing. The only way I know how to do Cauchy reals in a reasonable way (Bishop-style sets with equality and setoids in type theory are not reasonable) is to use higher-inductive-inductive types in homotopy-type theory (as written up in the HoTT book). | |
| Aug 21, 2017 at 6:00 | comment | added | David Roberts♦ | @AndrejBauer I guess if you are working with Cauchy reals anyway, you want countable choice up your sleeve, so no worries. | |
| Aug 21, 2017 at 5:14 | comment | added | Andrej Bauer | @DavidRoberts That's not really needed if you have dependent choice (I think just countable choice might suffice). It lets you recover a subsequence with a given rate of convergence from an ordinary sequence. | |
| Aug 21, 2017 at 0:47 | comment | added | David Roberts♦ | Don't you want to have control over the rate of convergence for Cauchy sequences, like $|q_n - q_{n+m} |\lt 2^n$? | |
| Aug 20, 2017 at 22:43 | vote | accept | XL _At_Here_There | ||
| Aug 20, 2017 at 22:40 | vote | accept | XL _At_Here_There | ||
| Aug 20, 2017 at 22:43 | |||||
| Aug 20, 2017 at 21:44 | comment | added | Andrej Bauer | Yes, in a way. Constructive math does not explicitly refer to computability. Explanations and justifications for it do, but when you make those precise you get models. | |
| Aug 20, 2017 at 20:01 | comment | added | XL _At_Here_There | I am somehow confused, you mean I have mixed the theory with it's models? | |
| Aug 20, 2017 at 19:37 | history | answered | Andrej Bauer | CC BY-SA 3.0 |