Michael Shulman <shulman@uchicago.edu> Saturday, March 8, 2008 3:05 pm Asks
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?
Yes, What you do is start with ETCS, and adjoin an axiom scheme of replacement. The axiom scheme says: Suppose a formula associates to each element x of a set S a set we may call Sx (unique up to isomorphism). Then there is some function f:X-->S such that the fiber of f over each element x is isomorphic to Sx. Lawvere's ETCS plus this axiom scheme is intertanslateable in the obvious way with ZF, preserving theorems in both directions (you may include AxCh in both ETCS and ZF, or exclude it from both). This has been known from the earliest days of categorical set theory. My favorite early published proof was stated slightly differently, using reflection rather than replacement, but it trivially comes to the same thing. That is: AUTHOR = "Osius, Gerhard", TITLE = "Logical and set-theoretical tools in elementary topoi", BOOKTITLE = "Model Theory and Topoi", series = "Lecture Notes in Mathematics 445", PUBLISHER = "Springer-Verlag", YEAR = "1975", editor = "F. Lawvere, and C. Maurer, and G. Wraith", pages = "297--346",
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)?
The proof in Osius (and several later tests) implies that every consistent extension of a certain very weak fragment of ZF is intertranslateable (preserving theorems) with a corresponding extension of a certain slight extension of ETCS. Further, when you read the proof, you see the correspondence is entirely natural. For details on replacement (as opposed to Osius's use of reflection) and foundational discussion see AUTHOR = "McLarty, Colin", TITLE = "Exploring Categorical Structuralism", JOURNAL = "Philosophia Mathematica", YEAR = "2004", pages = "37--53", best, Colin