Timeline for Difference between constructive Dedekind and Cauchy reals in computation
Current License: CC BY-SA 4.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Dec 28, 2023 at 21:26 | comment | added | Gro-Tsen | @AndrejBauer Thanks! | |
| Dec 28, 2023 at 17:00 | comment | added | Andrej Bauer | It's difficult to say what precisely the HoTT-style Cauchy reals correspond to in a topos, because a topos need not have higher inductive-inductive constructions. Nevertheless, the HoTT book shows that the Cauchy reals constructed therein are the smallest Cacuhy-complete archimedean ordered field. All the time, "Cacuhy" is defined in terms of Cauchy approximations (see comment above). In my head every Cauchy approximations gives a modulus, and ever modulus gives a Cauchy approximation, but I haven't checked on paper. | |
| Dec 28, 2023 at 9:52 | comment | added | Gro-Tsen | @AndrejBauer But, just to be clear, in a topos (or working within IZF), the reals you are talking about coincide with the smallest subset of the Dedekind reals that is closed under limits of Cauchy-sequences-with-modulus, correct? Not necessarily (or not obviously) with the a priori larger set defined as the smallest subset of the Dedekind reals that is closed under limits of Cauchy-sequences-without-modulus? (I think the latter definition makes sense, but maybe not, or maybe it's just widely believed to be uninteresting.) | |
| Dec 27, 2023 at 23:28 | comment | added | Andrej Bauer | See section 11.3 of the HoTT book. We don't use Cauchy sequences but rather Cauchy approximations: a map $x : \mathbb{Q}_{+} \to \mathbb{Q}$ such that $\forall \delta, \epsilon \in \mathbb{Q}_{+} .\, |x_\delta - x_\epsilon| < \delta + \epsilon$. This corresponds to having a modulus of continuity as a map, cf. section 11.2.2. (You can pretty much read Chapter 11 without reading the rest of the HoTT book.) | |
| Dec 27, 2023 at 22:17 | comment | added | Gro-Tsen | @AndrejBauer Is this for “Cauchy complete” in the sense of “Cauchy-with-modulus” or in the sense of “Cauchy-without-modulus”? (I don't know how to unambiguously refer to these two notions in a more concise way.) Or have both notions been considered? Do the completions perhaps coincide? | |
| Dec 27, 2023 at 19:33 | comment | added | Andrej Bauer | The least Cauchy complete subfield of Dedekind reals that contains $\mathbb{Q}$ is also known as Escardó-Simpson reals. In homotopy type theory it coincides with the construction of Cauchy reals as a higher inductive-inductive type. See doi.org/10.1109/LICS.2001.932488 and arxiv.org/abs/1706.05956 | |
| Dec 27, 2023 at 18:28 | history | answered | Gro-Tsen | CC BY-SA 4.0 |