Timeline for The constructive Eudoxus reals
Current License: CC BY-SA 4.0
12 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 13 at 16:55 | review | Close votes | |||
| Apr 17 at 7:38 | |||||
| Apr 13 at 14:18 | comment | added | Ember Edison | @Gro-Tsen I don't know Reverse Mathematics, and there's a lot of folklore about Eudoxus Reals, so I can't get a very reasonable (bishop's style constructivism) definition. The Eudoxus Reals I agree with are just quotient inductive-inductive types, but that's probably not useful for sorting out different real numbers. | |
| Apr 13 at 6:55 | comment | added | Gro-Tsen | […contd.] So, could you kindly spell out exactly what you call the (constructive) “Eudoxus reals” and how they differ from those other Eudoxus reals that happen to be equivalent to the Cauchy reals, and also what is known about the relation between the Eudoxus reals you're interested in and the Cauchy and Dedekind reals. (If you're interested in whether they can be countable, I suppose you already know a few things about them: so, could you summarize that?) | |
| Apr 13 at 6:51 | comment | added | Gro-Tsen | OK, now I'm even more confused. The paper you linked to, The Eudoxus Real Numbers by R. D. Arthan, takes place in classical math, and even explicitly states (last paragraph before “sources and remarks”) that the reals they construct are equivalent to the Cauchy and Dedekind ones. I don't see where there are three constructions in it, but even so, there are tons of ways to turn any classical definition into a constructive one. Now there appears to be a somewhat-standard definition of constructive Eudoxus reals, but you say that's not the one you want. [contd…] | |
| Apr 12 at 23:28 | history | edited | David Roberts♦ | CC BY-SA 4.0 |
Author and title for arXiv link
|
| Apr 12 at 20:22 | comment | added | Ember Edison | @Gro-Tsen I have linked the definition of Eudoxus reals that I agree with to the correct arxiv paper. There are three proposed implementations of Eudoxus reals in that paper, and the equivalent of Cauchy reals is only one of them. | |
| Apr 12 at 20:15 | history | edited | Ember Edison | CC BY-SA 4.0 |
Replace with the correct link.
|
| Apr 12 at 13:07 | comment | added | Gro-Tsen | Also, it is worth pointing out explicitly that, according to the Bauer and Hanson paper cited, “the Cauchy reals are sequence-avoiding in any parameterized realizability topos”, so if an example of a topos where the Cauchy=Eudoxus reals are countable is to be found, it should be of a different kind. | |
| Apr 12 at 13:05 | comment | added | Gro-Tsen | The terminology of constructive real numbers is a giant pile of mess because subtly different concepts sometimes go by the same name or vice versa, and not every author takes the trouble to recall every relevant definition; but IIUC, the nLab page (and this question), the “Eudoxus reals” are the same as the (unmodulated?) Cauchy reals, which seems to be a more standard terminology. If this is correct, I suggest writing “Cauchy reals (aka Eudoxus reals)” in this question, unless you have some reason to emphasize Eudoxus (in which case, maybe state it). | |
| Apr 12 at 6:24 | history | edited | David Roberts♦ | CC BY-SA 4.0 |
tags, links, paper details
|
| Apr 12 at 6:22 | comment | added | David Roberts♦ | For reference, here's a bunch of discussion by Andrej Bauer mathoverflow.net/a/453340/4177 | |
| Apr 12 at 6:03 | history | asked | Ember Edison | CC BY-SA 4.0 |