Timeline for Is every set smaller than a regular cardinal, constructively?
Current License: CC BY-SA 4.0
Post Revisions
15 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| S Aug 26, 2022 at 13:07 | history | suggested | Ulrik Buchholtz | CC BY-SA 4.0 |
corrected typo, improved typography
|
| Aug 26, 2022 at 12:45 | review | Suggested edits | |||
| S Aug 26, 2022 at 13:07 | |||||
| Jun 20, 2018 at 3:09 | comment | added | David Roberts♦ | It might be worth considering whether any predicative topos, in Benno's sense, has internally 'enough regular sets', where by regular I mean one of the characterisations on the nLab page about regular cardinals in terms of small categories of sets having colimits up to a certain size. | |
| Jun 19, 2018 at 14:12 | vote | accept | Tim Campion | ||
| Jun 19, 2018 at 13:23 | answer | added | aws | timeline score: 5 | |
| Jun 16, 2018 at 22:25 | comment | added | Tim Campion | But the question of whether there's a notion of "countable" which forms a $\Sigma$-universe seems like a good place to start. Maybe one has to work with subquotients of $\mathbb N$ rather than quotients. I'll also remark that the notion is reminiscent of the way object classifiers work in $\infty$-topoi. | |
| Jun 16, 2018 at 22:18 | comment | added | Tim Campion | Both of them use entire relations rather than functions -- maybe in a setting like a topos with some impredicativity one doesn't have to worry about this kind of thing? I should point out that this discussion also leads to a note by van den Berg where he shows (see the final remark) that in ZF, the axiom WISC implies there are arbitrarily large regular cardinals. (there's some discussion under the previous ncafe link too). I don't understand what's going on well enough to see if this generalizes. | |
| Jun 16, 2018 at 22:14 | comment | added | Tim Campion | @IngoBlechschmidt In the formulation I had in mind, there would be no size restriction on $Y$ -- e.g. I'd expect "maps with finite fibers" to form a $\Sigma$-universe. The nlab article that godelian links to above in turn links to an ncafe discussion from 2012 where Benno van den Berg gives a definition that seems similar in spirit. He worries about some kind of issue about theories with weak comprehension. Mike Shulman replies with an alternative definition... | |
| Jun 16, 2018 at 20:47 | comment | added | Ingo Blechschmidt | Excellent question. Tim, in intuitionistic set theory, the correspondence between maps with codomain $Y$ and $Y$-indexed sets still works, so I think your formulation is just fine. I'm wondering: Is even the collection of triples $(X,Y,f)$ where $X$ and $Y$ admit surjections from $\mathbb{N}$ a $\Sigma$-universe, constructively? That seems to be the most basic example classically. But I don't immediately see that it works constructively, because I don't see why fibers should be countable again. | |
| Jun 15, 2018 at 22:03 | comment | added | Tim Campion | The intention in formulating this in terms of maps $f: X \to Y$ was for such a map to constitute a family of sets $\{X_y\}_{y \in Y}$ indexed by $Y$. But I'm suddenly realizing that this might not be a correct formulation of this notion in some constructive settings. I'm not sure how to formulate my question in such settings. | |
| Jun 15, 2018 at 21:54 | comment | added | Tim Campion | @Goldstern I don't intend anything exotic by "function" -- a function $f: X \to Y$ is the same thing as a subset $S \subseteq X \times Y$ such that $\forall x \in X \exists! y \in Y S(x,y)$. I'm sure there are subtleties about this that I don't have an appreciation of, so let me know if that's not sufficiently clear. Base change of $f: X \to Y$ along $g: Y' \to Y$ means the projection function $X \times_Y Y' \to Y'$. Here $X \times_Y Y' = \{(x,y) \in X \times Y' \mid f(x) = g(y)\}$. Here $g$ is an arbitrary function (not assumed to be in the $\Sigma$-universe). | |
| Jun 15, 2018 at 21:38 | comment | added | Goldstern | What is a "base change"? Also, what is a function? In set theory, it would be a set of ordered pairs, but you may speak a different language. | |
| Jun 15, 2018 at 21:28 | comment | added | Trevor Wilson | Gitik's model in which every uncountable cardinal is singular seems like it might be relevant. | |
| Jun 15, 2018 at 21:25 | comment | added | godelian | You might want to look for REA, the regular extension axiom, which is usually used within constructive Zermelo-Fraenkel CZF. See ncatlab.org/nlab/show/regular+extension+axiom and the references there, in particular the paper by M. Rathjen and B. Lubarsky. | |
| Jun 15, 2018 at 20:23 | history | asked | Tim Campion | CC BY-SA 4.0 |