You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Madeleine Birchfield (Feb 06 2024 at 05:43):Does weak countable choice imply that the (modulated) Cauchy real numbers and the Dedekind real numbers coincide?
Toby Bartels thought so in 2010 when he added the claim to the nLab in 2010:
https://ncatlab.org/nlab/revision/diff/Cauchy+real+number/7
but Andrej Bauer doesn't think so in the comments of this question from late last year:
https://mathoverflow.net/questions/461200/does-weak-countable-choice-imply-that-the-cauchy-reals-are-dedekind-complete
Andrew Swan (Feb 06 2024 at 07:49):I saw this on mathoverflow a while ago and had it in the back of my head. I'll post an answer there if I think of one.
Andrew Swan (Feb 06 2024 at 07:52):I will say that I can't see how to show every Cauchy real is Dedekind just using WCC, but also in all of the standard examples of toposes that I usually try first either WCC fails, or holds so it's tricky to come up with a counterexample.
Andrew Swan (Feb 06 2024 at 07:53):You can show that for any two Dedekind reals, there is a binary sequence which is constantly zero iff the reals are equal.
Nathanael Arkor (Feb 06 2024 at 08:48):Perhaps it would be worth sending an email to Toby Bartels to ask what his justification was for the claim?
Morgan Rogers (he/him) (Feb 06 2024 at 08:59):@Toby Bartels is a member of this Zulip, so might answer here, although he hasn't been active in a while.
Reid Barton (Feb 07 2024 at 01:35):What exactly is WCC, by the way?
John Baez (Feb 07 2024 at 03:05):I don't know anything about this but the nLab says
(WCC): A surjective function f:S→ℕ splits, if, whenever i≠j, either f *(i) or f *(j) is a singleton. (This is a rather special case of countable choice that can also be proved using only excluded middle.)
Toby Bartels (Feb 12 2024 at 18:34):Morgan Rogers (he/him) said:
Toby Bartels is a member of this Zulip, so might answer here, although he hasn't been active in a while.
I've never been active, although I can be summoned.
I've responded to the MO question. 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.
Morgan Rogers (he/him) (Feb 14 2024 at 16:40):Pinging @Dianthe Basak, since she mentioned variations on choice to me last week and may be interested in this conversation.