On Fri, Jul 15, 2011 at 8:30 AM, Peter Selinger <selinger@mathstat.dal.ca> wrote:
However, after some more digging, I found that the axiom of collection indeed follows from for axiom of replacement (along with the rest of ZF) without using choice.
Right (although the argument does use Regularity, I believe). Collection is also generally included in constructive/intuitionistic set theories such as IZF and CZF. Moreover, collection is automatically true (suitably interpreted) in the internal logic of any category.
Finally, if the goal is to complete a small subcategory of Set under finite limits, I wonder if the axiom of collection is even needed at all. Certainly the collection of finite diagrams (in the original subcategory) forms a set. Since each finite diagram in Set has a distinguished canonical limit (for example, the one that arises as a subset of the cartesian product of all the objects in the diagram), adding all of these limits to the original subcategory gives a new small subcategory and requires no choices. One can then iterate the construction and take the union. Right?
Yes, certainly, if the category Set is constructed out of sets in some set theory like ZF, then there are indeed canonically specified limits of any finite diagram, and choice is unnecessary. (I thought someone had already mentioned this on the list, but now I can't find it.) However, I think Eduardo mentioned that the motivation behind his question was to complete small subcategories of other toposes under finite limits as well (such as a small subcategory of generators). Mike