Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeMay 14th 2013
    • (edited May 3rd 2014)

    added to Cachy real number a pointer to

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeJan 8th 2018

    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.

    • CommentRowNumber3.
    • CommentAuthorTobyBartels
    • CommentTimeFeb 12th 2019

    Incorporate Wolfgang Keller's suggested edit.

    diff, v17, current

    • CommentRowNumber4.
    • CommentAuthorGuest
    • CommentTimeFeb 2nd 2022
    Is there a proof somewhere that the generalised Cauchy real numbers are the same as the Dedekind real numbers? None of the sources at the bottom article speak of Cauchy nets and generalised Cauchy real numbers.
    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 3rd 2022

    I don’t know offhand of it being written down anywhere. Maybe Toby does? I think I learned it from him.

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeFeb 10th 2023
    • (edited Feb 10th 2023)

    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:

    • Fred Richman, The fundamental theorem of algebra: a constructive development without choice (1998) [pdf]

    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!

    diff, v32, current

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeFeb 10th 2023

    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

    diff, v34, current

  1. 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.

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeFeb 10th 2023

    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)

    diff, v35, current

  2. 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.

    • CommentRowNumber11.
    • CommentAuthorGuest
    • CommentTimeFeb 10th 2023

    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.

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeFeb 10th 2023

    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).

  3. Adding publication info and doi for reference:

    Anonymouse

    diff, v44, current

  4. 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:

    https://mathoverflow.net/questions/461200/does-weak-countable-choice-imply-that-the-cauchy-reals-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.

    • CommentRowNumber15.
    • CommentAuthorTobyBartels
    • CommentTimeFeb 12th 2024
    • (edited Feb 12th 2024)

    Remove more spurious references to weak countable choice. ETA: also some details about choices for modulus.

    diff, v46, current

    • CommentRowNumber16.
    • CommentAuthorTobyBartels
    • CommentTimeFeb 12th 2024

    @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 (L,U)(L,U); the net is indexed by LL with the usual order and x q=qx_q = q. Note that if you ignore UU, 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 UU with the opposite order, thinking of them as located upper real numbers.)