On Mar 8, 2008, at 12:51 AM, Michael Shulman wrote:
On Fri, Mar 7, 2008 at 2:52 PM, Steve Awodey <awodey@cmu.edu> wrote:
http://www.phil.cmu.edu/projects/ast/
The short answer is, it depends on how "Sets" sits in the category of classes. In fact, *any* topos can occur as a category of "Sets" satisfying replacement in a suitable category of classes constructed from the topos.
Very interesting! But I don't think that is the answer to the question I intended to ask, although perhaps I phrased the question poorly. As far as I can tell, you give a way of interpreting replacement/collection in such a way that it is satisfied in all toposes, by "constructivizing" the existential quantifier.
no, the existential quantifier has its standard (categorical) interpretation (direct image), not the "constructive" one from type theory. We do not reinterpret replacement/collection either -- they have their usual interpretation. What is a bit delicate is the background category of classes in which the (set-theoretically) unbounded quantifiers are interpreted.
But as you say, "In consequence, the standard arguments using Replacement that take one outside of V_\lambda(A) for \lambda non-inaccessible, are not reproducible." What I would really like to know is, can one formulate an elementary property of a topos which *does* allow one to reproduce the standard arguments of Replacement?
Here's another way to phrase the same (or a similar) question. Suppose I meet a mathematician who thinks categorically enough to dislike the membership-based nature of ZF(C), but doesn't want to give up any of its consequences. In particular, he wants to be able to use transfinite induction beyond \omega+\omega. For instance, he wants Borel determinacy to be true, which is provable in ZFC but not in Zermelo set theory (ZFC minus Replacement). Is there a categorical foundation I can tell him to use? That is, is there an elementary categorical theory which is as strong as ZF(C)?
AST? Steve
Mike