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).
Adding publication info and doi for reference:
Anonymouse
There’s a question on MathOverflow asking whether weak countable choice is sufficient to prove that the Cauchy real numbers with modulus are Dedekind complete:
According to the discussion under the question, none of the references at the bottom of the page seem to provide a proof using WCC.
Remove more spurious references to weak countable choice. ETA: also some details about choices for modulus.
@Guest #4 (maybe too late for you to see this):
No, I don't know of a reference, although the proof is fairly straightforward. Given a Dedekind cut ; the net is indexed by with the usual order and . Note that if you ignore , then you get the lower real numbers as equivalence classes of nets of rational numbers (although they're not necessarily Cauchy nets, even restricting to the bounded ones, without classical logic), so this effectively gives the Dedekind real numbers as the located lower real numbers. (Or you could take the index set to be with the opposite order, thinking of them as located upper real numbers.)
1 to 17 of 17