Timeline for Is Bauer–Hanson’s result “there is a topos where the Dedekind reals are countable” novel?
Current License: CC BY-SA 4.0
23 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 15 at 11:51 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 22 characters in body
|
| Apr 15 at 11:50 | comment | added | Andrej Bauer | @WillSawin: Yes, that would make sense. I will fix it (and the timestamp year, thanks to Anurag). | |
| Apr 15 at 10:29 | comment | added | Will Sawin | If the goal is for sequence-avoiding to be stronger than uncountable, maybe the definition should just say that $A$ is inhabited and for every sequence $\mathbb N \to A$ there exists an element of $A$ that is not a term of the sequence? Otherwise the empty set is sequence-avoiding but not uncountable. | |
| Apr 15 at 7:41 | comment | added | Anurag Sahay | It seems like your edit timestamp has the wrong year. | |
| Apr 15 at 6:35 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 115 characters in body
|
| Apr 15 at 6:33 | comment | added | Andrej Bauer | @WillSawin: An interesting thought, but note that the usual proofs relying on countable choice that $\mathbb{R}$ is sequence-avoiding break down if we use $\mathbb{N} \to 1 + \mathbb{R}$. The problem is, given $a : \mathbb{N} \to \{\star\} + \mathbb{R}$, how do we make any progress in constructing a real $x$ that avoids $a$ when $a$ is just producing $\star$'s? In fact, I think in the effective topos the reals will not be sequence-avoiding in this sense. | |
| Apr 15 at 1:03 | history | edited | LSpice | CC BY-SA 4.0 |
Typos, while this is on the front page
|
| Apr 15 at 1:01 | comment | added | Will Sawin | Should the maps in the definition of sequence-avoiding be from $\mathbb N$ to $1+A$, for the same reason as in the definition of countable? | |
| Apr 14 at 23:57 | history | edited | Aaron Meyerowitz | CC BY-SA 4.0 |
SPELLING
|
| Sep 21, 2023 at 5:25 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
deleted 259 characters in body
|
| S Sep 21, 2023 at 5:25 | history | rollback | Andrej Bauer |
Rollback to Revision 4 - Edit approval overridden by post owner or moderator
|
|
| Sep 21, 2023 at 4:37 | history | suggested | Jim Kingdon | CC BY-SA 4.0 |
The reals are a set in CZF per comments elsewhere on this question or https://mathstodon.xyz/@MartinEscardo/110944257074282172
|
| Sep 21, 2023 at 4:28 | review | Suggested edits | |||
| S Sep 21, 2023 at 5:25 | |||||
| Aug 29, 2023 at 15:40 | comment | added | Anon | Thank you very much for clearing things up! I don't know why I was thinking subcountable and countable are equivalent. This answer really helped. | |
| Aug 29, 2023 at 15:18 | vote | accept | Anon | ||
| Aug 24, 2023 at 6:13 | comment | added | Andrej Bauer | @DavidRoberts: Thanks, fixed. | |
| Aug 24, 2023 at 6:12 | comment | added | Andrej Bauer | @LSpice: I improved the reference, although it is generally known that countable choice suffices for uncountability of reals, so that's by no means the only reference available. | |
| Aug 24, 2023 at 6:11 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 431 characters in body
|
| Aug 24, 2023 at 4:02 | comment | added | David Roberts♦ | The theorem giving the subcountability of the Dedekind reals and citing Hamkins' work, is the "no surjection" the other way around? Also, in the second of the two caveats, with the nested intervals method, it mentions with excluded middle and countable choice: is this meant to be without excluded middle? | |
| Aug 23, 2023 at 23:53 | history | edited | Sam Hopkins | CC BY-SA 4.0 |
added 1 character in body
|
| Aug 23, 2023 at 23:53 | comment | added | LSpice | You mention "Bishop's book on constructive analysis", but he seems to have at least 2. Did you mean "Foundations of constructive analysis" (MSN)? | |
| Aug 23, 2023 at 23:52 | history | edited | LSpice | CC BY-SA 4.0 |
Proofreading
|
| Aug 23, 2023 at 23:41 | history | answered | Andrej Bauer | CC BY-SA 4.0 |