Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Finally started ZFC.
Mike, I'd appreciate it if you'd check the claims there about variations. Perhaps I should write axiom of separation and axiom of replacement to clarify what my terms for variations on those axioms mean, but you can probably guess.
Thanks for doing this, ZFC has been missing for too long. I didn't check your assertions about the variations on separation, replacement, and collection (too lazy to figure out what the different versions refer to at the moment), but I made a few corrections, namely (1) MK is weaker than an inaccessible cardinal and (2) Replacement + PEM implies Full Separation. I also added some comments about V=L, AD, and GCH, and a query about the inclusion of dependent choice in CZF.
I figured out (1) by the bottom of the page but didn't fix the top (and didn't write the bottom very clearly either). I plumb forgot about (2)! Thanks for the additions.
I put all of the names of theories (rather than names of axioms) into boldface, but maybe that will be too much trouble to keep up. Do you think that there's any point to it?
I don't see much point to putting theory-names in bold; I've noticed that you do it all the time but never really understood why.
I picked it up from … some books. I can see the point; you can tell at a glance what's a whole theory and what's merely an axiom. It seems to me much like putting category names in bold.
But we don't do that in the Lab, and even I don't do that in the Lab (although I do in my own writing), following … John or Urs, whoever first set the standard here.
So probably I should just give up the boldface for theories in the Lab too.
Now we've got Tarski–Grothendieck set theory there too, mostly just because it was listed as a variation at Wikipedia.
I started axiom of replacement, but I'm getting tired.
at ZFC in the statement of axiom 3 “pairing” I fixed the spurious upper-case to lower-case.
I’ve read into Aczel old unfinished book draft on constructive set theory and surveyed the internet and the local library this week.
I found there’s a theme where even set theorists like Hamkins aren’t sure what goes into the old Zermelo theory. The ZFC article here also implies it has Foundation, although that’s a young axiom, relatively speaking (Wikipedia says it’s not in the theory). Now I wouldn’t bother about the conventions too much, but the article also says that if you have Separation bounded, this is equivalent to ETCS, and the two ETCS articles doesn’t speak about the ZFC axioms too directly (only talk about well-pointedness). In the Rethinking set theory paper, regularity doesn’t seem to pop up, so is the ZFC article misleading in that regard? On that note, just to make sure, is Separation the only axiom that needs a boundedness requirement (the answer might be yes simply by virtue of powerset giving us all collection instances that we sometimes also see in bounded fashions)?
Sorry, I’m confused, what exactly are you asking?
Whether, if we say bounded Zermelo theory ZB is equivalent to ETCS, if we speak of a ZB that includes the Foundation axiom. In the list on that page, this axiom with number 10 is included, while historically Foundation is not a part of Z. E.g. are infinity descending chains impossible in the ETCS world? Thanks.
Asking directly whether ETCS satisfies foundation is nonsensical: foundation only makes sense in the world of material set theory. When constructing a model of material set theory (like BZ) from a model of structural set theory (like ETCS), you can choose to build either a well-founded one or an ill-founded one (e.g. satisfying some anti-foundation axiom).
BZ is not equivalent to ETCS in the strong sense that ZFC is equivalent to ETCS+R, instead it is only equiconsistent: we can construct a model of each from a model of the other, but the round-trip composites need not be the identity. Foundation is irrelevant for this equiconsistency: it’s unneeded when constructing a model of ETCS from the sets in BZ, and as I mentioned above you can choose for it to be satisfied or not when going in the other direction. Where it does become relevant is when asking whether the roundtrip from BZ to ETCS to BZ is the identity; obviously if in the second step you choose to satisfy foundation, you won’t get back the original model unless that already satisfied foundation.
I see that our page ZFC uses the word “equivalent”; it might be better to correct that to “equiconsistent”.
Aren’t ZFC and ZFC-Foundation equiconsistent as well? I mean, you can always build von Neumann’s inside ZFC-Foundation (I think this was his motivation), and clearly a model of ZFC is a model of ZFC-Foundation.
Yes, absolutely. In fact a complicated way of saying that is that you build a model of ETCS from your model of ZFC-Foundation, then build a model of ZFC from that. That detour is overkill for ZFC, but for weaker theories that don’t start out satisfying the “co-foundation axiom” of Mostowski collapse it’s sometimes actually what you want to do (e.g. I believe it’s basically what Mathias does in “The strength of Mac Lane set theory”).
1 to 16 of 16