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.
Perhaps we should have a page for the category of ZF-classes (if we don’t have one already, I can’t check atm). Aside from being a pretopos, it’s (small) cocomplete with NNO (and W-types more generally) and with subobject classifier. There is this paper which is relevant.
Those are some good points, David.
The closest page we have might be algebraic set theory.
I think the standard material set theory model for algebraic set theory is NBG, to that proper classes are first-class objects and not mere syntactic devices.
But that’s basically equivalent.
I’m sure you know better than me, but aren’t the classes of ZF just the definable classes, as opposed to NBG classes which could be more arbitrary? I can certainly imagine that there could be classes in a model of NBG that don’t arise from propositions in the first-order language of sets.
Yes, you’re right, that’s true. But NBG doesn’t allow you to construct any non-definable classes (in contrast to MK).
I guess maybe my point is that I don’t think it would be worth having separate pages about the category of ZF-classes versus the category of NBG-classes, as the former is a special case of the latter.
No, just perhaps it would be good for searchability to have something like category of classes, separate from ’algebraic set theory’, which isn’t a very enlightening title for a materially-trained mathematician.
Oh, I certainly agree; I was just pointing out AST as the closest thing we already had.
1 to 10 of 10