Timeline for Equivalence of omniscience principles for natural numbers and analytic omniscience principles for Cauchy real numbers
Current License: CC BY-SA 4.0
11 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 15 at 14:58 | comment | added | Christopher King | Note that the "property for Cauchy real implies property for natural numbers" direction is given by using the principles on Cantor set (whose elements are all Cauchy reals). | |
| Jul 7 at 4:28 | history | became hot network question | |||
| Jul 6 at 22:37 | answer | added | Gro-Tsen | timeline score: 5 | |
| Jul 6 at 21:56 | comment | added | Gro-Tsen | Thank you for the clarification. For the record, as evidence that it is not so standard to assume (in the absence of Choice) that Cauchy sequences have a modulus of convergence, I can point to this paper (which explicitly says “Cauchy sequence with modulus” when it assumes one) and that one (which speaks of “regular reals” for the ones defined by a Cauchy sequence with modulus, and “Cauchy reals” for the ones without). So I think it's best to always clarify. | |
| Jul 6 at 21:55 | comment | added | Madeleine Birchfield | As for Markov's principle, Toby Bartels made a similar claim on the nLab in 2011 when he wrote on the nLab "Equivalent forms: ... If a Cauchy real number does not equal zero, then it is apart from zero in that it has a multiplicative inverse." but didn't provide a proof or reference for that either. | |
| Jul 6 at 21:46 | comment | added | Madeleine Birchfield | @AndrejBauer We do not have countable choice here. We are using the Cauchy real numbers here because that is what Toby Bartels was talking about in 2012 when he wrote on the nLab "In any case, if we use the Cauchy real numbers (sequential real numbers), then the sequential analytic (L)LPO is the same as the (L)LPO for natural numbers." but he did not provide a proof or reference for that statement. | |
| Jul 6 at 21:44 | comment | added | Madeleine Birchfield | @Gro-Tsen These Cauchy sequences come with a modulus as that is the convention in constructive mathematics when constructing the Cauchy real numbers as far as I am aware. I have edited the question to clarify that. | |
| Jul 6 at 21:42 | history | edited | Madeleine Birchfield | CC BY-SA 4.0 |
added 32 characters in body
|
| Jul 6 at 21:31 | comment | added | Gro-Tsen | By a “Cauchy sequence” $(u_n)$, do you mean a Cauchy-with-modulus sequence $∃μ:\mathbb{N}\to\mathbb{N}.∀k.∀p,q≥μ(k).|u_p-u_q|<2^{-k}$ or a Cauchy-without-modulus sequence $∀k.∃n.∀p,q≥n.|u_p-u_q|<2^{-k}$ ? Both have been called “Cauchy sequence”, so it would really be best to avoid the term without clarifying it as “with modulus” or “without modulus”. | |
| Jul 6 at 20:57 | comment | added | Andrej Bauer | Do we have countable choice? If not, why are we using Cauchy reals? | |
| Jul 6 at 20:28 | history | asked | Madeleine Birchfield | CC BY-SA 4.0 |