Timeline for How much Replacement does this axiom provide?
Current License: CC BY-SA 4.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 18, 2022 at 1:41 | comment | added | Joel David Hamkins | @TomLeinster Mathias has emphasized that what set theory is about at its core is transfinite recursion---giving a satisfactory account of well-founded recursion is what the entire subject is aimed at. The ability to implement this in ETCS, consequently, to my way of thinking would be a measure of how well that theory captures core set-theoretic concerns. | |
| May 15, 2019 at 8:36 | comment | added | Tom Leinster | (continued) Despite all that, maybe there's some way of phrasing the transfinite recursion principle in ETCS, by thinking about it differently rather than simply attempting to mimic the ZF-type formulation. | |
| May 15, 2019 at 8:32 | comment | added | Tom Leinster | Thank you, Joel and @DavidRoberts. Re defining $V$, I see the following obstacles: (1) defining $V$ usually involves taking unions of abstract sets, which in ETCS doesn't make sense (because you can't ask whether elements of two different sets are equal). (2) ETCS doesn't prove the existence of a coproduct of $\mathbb{N}, P(\mathbb{N}), P(P(\mathbb{N})), \ldots$; one needs to add some form of replacement/cocompleteness axiom for that. So roughly speaking that means we don't have $V_{\omega+\omega}$. (Continues) | |
| May 14, 2019 at 21:55 | comment | added | David Roberts♦ | @AsafKaragila Here's a preprint version, if you don't want to give E a click researchgate.net/publication/… (I only promised not to do free work for them, not to avoid reading authors who still do :-) | |
| May 14, 2019 at 13:55 | comment | added | Asaf Karagila♦ | @David: Are we allowed to read papers that were published by Elsevier again? | |
| May 14, 2019 at 0:30 | comment | added | David Roberts♦ | @Tom There's doi.org/10.1016/j.apal.2013.06.004 by Awodey et al, and Mike Shulman's unreleased (unfinished?) hint from the references in (the arXiv version of) his stack semantics paper, "Michael A. Shulman. 2-categories of classes. In preparation" | |
| May 13, 2019 at 21:12 | comment | added | Joel David Hamkins | I'm not sure. The idea is that any definable operation should be allowed, and I'm unsure of the exact expressive power of ETCS. I worry that the language of that set-up might be limited to bounded quantifiers, in which case you are only getting replacement for $\Delta_0$-assertions, which would be weaker than full replacement. Something like the axiom of collection appearing in Kripke-Platek set theory. | |
| May 13, 2019 at 20:22 | comment | added | Tom Leinster | Your blog post was one of the things I read before posting, so I'll take the opportunity to ask now what I wondered then: if we're using the language of ETCS (so, no assuming that elements of sets are sets, etc.), how would you define $V$ and "class function"? | |
| May 13, 2019 at 11:45 | history | answered | Joel David Hamkins | CC BY-SA 4.0 |