5
$\begingroup$

Assuming the axiom of weak countable choice, is the set of modulated Cauchy reals Dedekind complete?

The second theorem on this ncatlab page claims something equivalent, but it doesn't contain a proof and I can't find any references for the claim outside of ncatlab.

Theorems. (assuming WCC ).

Every classical Cauchy real number is modulated, and any two equal Cauchy real numbers are equal as modulated Cauchy real numbers.

Every multivalued Cauchy real number is equal (as a multivalued Cauchy real number) to some classical Cauchy real number, and two classical Cauchy real numbers are equal if they are equal as multivalued Cauchy real numbers.

I know that both WCC and the Dedekind completeness of the Cauchy reals follow from $\text{CC} \lor \text{LEM}$, but I am unable to verify any implication between them.

Trying to prove it myself, the line of thought I keep pursuing is that since every irrational Dedekind real has a modulated Cauchy sequence, perhaps you only need to make a choice when the Dedekind real is near a rational number. The problem is that no matter how precise you get, you never know for sure when the time to make the choice is. With CC making the choice prematurely is fine, but with WCC you can only make one choice, so you can't "waste it".

Improve this question
$\endgroup$
9
  • $\begingroup$ Can you be a bit more specific about the "second theorem on the page" claiming "something equivalent"? Which theorem is the "second one" and what is the precise claim? The only thing I can see is about Cauchy nets. $\endgroup$
    – Andrej Bauer
    Commented Dec 28, 2023 at 20:42
  • 1
    $\begingroup$ Something is fishy here: in Lubarsky & Richman, “Signed-Bit Representations of Real Numbers”, the question of what Choice principles can be used to prove that Cauchy and Dedekind reals coincide (all right, they're mostly talking about Cauchy reals without modulus, but still), and they don't mention WCC at all, even though there is an author in common with the Bridges, Richman & Schuster paper that defined it. Surely they would have said so if WCC were relevant for this! $\endgroup$
    – Gro-Tsen
    Commented Dec 28, 2023 at 22:01
  • 2
    $\begingroup$ (I mean, if Richman coauthored a paper about a weak Choice principle, and Richman later coauthors a paper about Cauchy reals, with and without modulus, versus Dedekind reals which has a section about Choice principles, surely you would expect the latter paper to cite the former if the former is relevant to proving that Cauchy reals with modulus are in fact the same as Dedekind reals. I know absence of evidence is not evidence of absence, but still, this would be really bizarre.) $\endgroup$
    – Gro-Tsen
    Commented Dec 28, 2023 at 22:05
  • 2
    $\begingroup$ For what it's worth, my gut feeling is that WCC is not enough to show that (modulated) Cauchy reals and Dedekind reals coincide. $\endgroup$
    – Andrej Bauer
    Commented Dec 28, 2023 at 22:49
  • 1
    $\begingroup$ @ChristopherKing You might want to ask Toby Bartels since he was the one who added the claims to the nLab back in 2010: ncatlab.org/nlab/revision/diff/Cauchy+real+number/7 $\endgroup$
    – Madeleine Birchfield
    Commented Feb 6 at 5:29

1 Answer 1

Reset to default
4
$\begingroup$

I don't have a definitive answer, but since I wrote the text on nLab that sparked the question, I do have some things to say. Short version: This (probably) doesn't follow from WCC (and so I will edit the nLab page); instead, it follows from a different classically trivial form of countable choice.

There's a fair amount of material on WCC on Fred Richman's page at Flordia Atlantic, which seems to have disappeared last year, but is saved on the Internet Archive. If the result is true, then I probably got it from something there, although some of that was unpublished (and so not peer-reviewed, much like the nLab itself). Since Richman didn't cite it in his other paper, perhaps he realized that it was a mistake, or decided that WCC isn't that important after all, or else he only proved it after that paper.

More likely, the mistake was mine. One interesting thing about WCC is that it follows separately from Excluded Middle (without choice) and from Countable Choice (constructively). There is a different weak choice principle that has these two properties, and which does prove that every Dedekind real is a modulated Cauchy real: countable choice for subsets of $ \{ 0 , 1 \} $. That is, every $ \mathbb N $-indexed family of inhabited subsets of $ \{ 0 , 1 \} $ has a choice function; this follows from Countable Choice by fiat, and from Excluded Middle by picking $ 0 $ if it's available and $ 1 $ otherwise. (This is equivalent to the principle $ AC _ { weak } $ at another MO question.)

I believe that this explains the nLab page. But this doesn't actually answer the question as to whether WCC might imply the Dedekind completeness of the modulated Cauchy reals by some other trick.

Improve this answer
$\endgroup$
8
  • 1
    $\begingroup$ Note that $\text{AC}_{\mathbb N, \mathbb N}$ also follows from $\text{CC} \lor \text{LEM}$. That's because LEM let's you pick a minimum from an inhabited sets of natural numbers. $\endgroup$
    – Christopher King
    Commented Feb 12 at 19:42
  • $\begingroup$ Lemma 11.4.1 in the HoTT book attacks coincidence of Cauchy and Dedekind reals along the lines of choice of subsets of $\{0,1\}$. I don't know where we got it from when we wrote that, but I was definitely aware of this approach before 2012. How far back can we trace the observation? $\endgroup$
    – Andrej Bauer
    Commented Feb 12 at 21:44
  • $\begingroup$ @AndrejBauer it's obvious that it implies the existence of locators, so observing that $x$ having a locator implies that $x$ is a Cauchy real would count. I don't know how far that observation goes back tho. $\endgroup$
    – Christopher King
    Commented Feb 12 at 21:52
  • $\begingroup$ As far as I am aware, locators appeared in Auke Booij's thesis in 2020, so pretty new. $\endgroup$
    – Andrej Bauer
    Commented Feb 12 at 21:58
  • $\begingroup$ Locators are the name Auke Booij gave to the elements of the dependent product that appears in Lemma 11.4.1 in the HoTT book. $\endgroup$
    – Madeleine Birchfield
    Commented Feb 13 at 1:47

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .