Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
added to Cachy real number a pointer to
I added to Cauchy real number a link to Lubarsky’s paper on (the constructive lack of) Cauchy completeness of the Cauchy reals, and some discussion of his countermodels — which I’m almost certain are actually generic objects in classifying toposes, but oddly (for a paper about constructive mathematics written in 2007) he makes no mention of toposes at all.
I don’t know offhand of it being written down anywhere. Maybe Toby does? I think I learned it from him.
touched the list of references
these two references, with their comments, look superficially contradictory to each other:
On why Cauchy sequences with a modulus of convergence are sequentially Cauchy complete:
On why the modulated Cauchy real numbers are not sequentially Cauchy complete
Scanning over the entry it is not readily clear what resolves this apparent contradiction:
Apparently and surprisingly, there is a major difference between the meaning of the terms:
“Cauchy sequences with a modulus of convergence”
and
“modulated Cauchy real numbers”
?
I haven’t dug enough through the references yet to sort this out. If anyone knows, let’s add a Remark to the entry to clarify this!
For what it’s worth, I discovered the old github repository corresponding to Lundfall 2015, and so I added the pointer (here and elsewhere): github.com/MrChico/Reals-in-agda
Urs,
Apparently and surprisingly, there is a major difference between the meaning of the terms: “Cauchy sequences with a modulus of convergence” and “modulated Cauchy real numbers”?
That’s because the latter are constructed as a quotient set of the former. In particular, there are many Cauchy sequences with a modulus of convergence which have the same limit, the quotient identifies those Cauchy sequences with the same limit as being equal to each other.
I see. The wording in the entry made it sound (to me anyway) as if this was about fine-print in what is meant by “modulated”.
But if what is meant is the usual issue of whether or not one passes to equivalence classes of sequences, then this is just the usual statement, going back to Bishop (1967, p. 27) and then Bishop & Bridges (1985, p. 29) not to Richman 1988 (in fact, scanning through Richman’s article, it is not immediately clear which statement in there is meant to be cited here).
So I have reworded somewhat, and brought in the relevant original references (here)
I think the term “modulated Cauchy real number” means that the quotient is constructed from the set of Cauchy sequences with a modulus of convergence, while the other term “Cauchy real number” without “modulated” means that the quotient is constructed from the set of arbitrary Cauchy sequences (no modulus of convergence assumed). I haven’t read Richman but the term “modulated Cauchy real number” appears in Ruitenburg’s Constructing Roots of Polynomials over the Complex Numbers.
The term “Cauchy real number” is overloaded in the literature. In the HoTT book for example the “Cauchy real numbers” are constructed in such a way that they are Cauchy complete (no choice principles assumed), while elsewhere in the literature the “Cauchy real numbers” are not Cauchy complete. Then one could use nets or filters instead of sequences and get “Cauchy real numbers” which are Dedekind complete.
Guest, sure, that’s the point of the discussion.
In my last edit I tried to make clear where in the literature list (here) we are referring to Bishop-style Cauchy sequences, or to equivalence classes of these, or to the novel inductive-inductive thing. If you see room to add further clarifications, let us know where exactly. (I don’t vouch for the bulk of the article, though, I only worked on the list of references).
1 to 12 of 12