On Thu, Mar 6, 2008 at 10:01 AM, Paul B Levy <P.B.Levy@cs.bham.ac.uk> wrote:
Maybe not the walls of mathematics, but what about theorems like "every polynomial functor on Set has a unique initial algebra whose structure map is an identity"? I think theorems like this are worth retaining (and antifoundation makes even more of them).
I'm not familiar with that particular result, but I know other categorical proofs which use set-theoretic ideas like transfinite induction, and so cannot be detached from ZF in an obvious way. On the other hand, there is nothing intrinsically "membership-based" in transfinite induction. The problem seems to be the lack of a categorical analogue of ZF's axiom of replacement, since the sets in V_{\omega+\omega} already form a well-pointed elementary topos with a NNO. I find this especially mysterious because on the surface, replacement merely replaces a set by an isomorphic one (or at most a quotient)! One categorical analogue of replacement comes from categories of classes in algebraic set theory. That is, we move from a categorical analogue of ZF to an analogue of Godel-Bernays set theory. But it seems natural to wonder whether there could be a categorical analogue of replacement expressible solely as a property of the category Set, without reference to how it sits in a category of classes. Has anyone studied this question? Mike
On Mar 7, 2008, at 5:18 AM, Michael Shulman wrote:
One categorical analogue of replacement comes from categories of classes in algebraic set theory. That is, we move from a categorical analogue of ZF to an analogue of Godel-Bernays set theory. But it seems natural to wonder whether there could be a categorical analogue of replacement expressible solely as a property of the category Set, without reference to how it sits in a category of classes. Has anyone studied this question?
yes: Carsten Butz, Thomas Streicher, Alex Simpson and I did. See the first two items under 2007 on the AST site: 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. Steve Awodey
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. 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)? Mike
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
Augmenting Steve Awodey's reply to M. Shulman I want to mention a further possibility which is more in the spirit of type / category theory, namely that of universes in toposes as described in my article with the same title (available under (www.mathematik.tu-darmstadt.de/~streicher/NOTES/UniTop.ps.gz). It is essentially a catgorical variant of Martin-Loef's notion of universe albeit an impredicative one. It was used a lot in categorical semantics of type theory (starting ~1985) but certainly part of the categorical folklore. The first written account I know of is Jean B'enabou's "Probl`emes dans le topos" from 1973. His main example that time was decidable K-finite objects in a topos with nno. A universe in a topos EE is a pullback stable class SS of morphism admitting a generic element in SS, i.e. a map E -> U in SS from which all other maps in SS can be obtained via pullback. Replacement is modelled by the requirement that SS be closed under composition. Of course, one usually requires more further closure properties (as in type theory). In the above mentioned paper I have shown that all Grothendieck and realizability toposes admit such universes (exploiting Grothendieck universes on the meta-level). As far as I can see universes serve well the purpose of replacement in mathematics, namely defining families of types by recursion. They achieve this goal in a more direct way than replacement does. The reason why they are presumably weaker than the setting Steve mentioned is that one needs a type-theoretic collection axiom (as in Joyal and Moerdijk's "Algebraic Set Theory") besides W-types for constructing set theoretic universes from type theoretic ones. I don't know why universes have hardly been considered in topos theory. (One notable exception being B'enabou's calibrations giving notions of size when considering locally small fibrations.) I think they are most useful and actually indispensible for doing category theory in the internal language of a topos. Algebraic Set Theory is an instance of universes, namely universes within categories modelling first order logic. Thomas
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
On Sat, Mar 8, 2008 at 2:45 PM, Colin McLarty <colin.mclarty@case.edu> wrote:
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. [...]
Thank you! This is exactly what I was looking for.
This has been known from the earliest days of categorical set theory.
But it doesn't seem to be *well* known any more, or at least well-disseminated and exposited. Several people have told me that they didn't think it was possible to express replacement category-theoretically without using a category of classes. And even now knowing what I'm looking for, I am unable to find more than a sentence or two about it in any book on topos theory, none of which actually gives any version of the axiom.
AUTHOR = "McLarty, Colin", TITLE = "Exploring Categorical Structuralism",
This raises another question. You mention at the end of this paper that large-cardinal axioms are "routinely pursued in isomorphism-invariant terms". This is clear to me for many types of large cardinals, but not for the stronger ones that involve elementary embeddings of the universe of sets. Ultrapowers have a categorical analogue, of course (filterquotient) but then there is a transitive collapse of the entire universe, from which I don't see immediately how to eliminate the global membership predicate. Can you give a clue or a reference? Thanks again, Mike
Wednesday, March 12, 2008 11:37 pm Subject: Re: categories: Re: replacing set theory Writes of the replacement scheme in categorical set theory
But it doesn't seem to be *well* known any more, or at least well-disseminated and exposited. Several people have told me that they didn't think it was possible to express replacement category-theoretically without using a category of classes.
There are two issues here, because there are two things to mean by "replacing set theory." On one hand it can mean replacing the membership-theoretic approach of ZF by the categorical approach of ETCS. This has long been routine and full details are found in Osius "Categorical Set theory: A Characterization of the Category of Sets", (Journal of Pure and Applied Algebra, 1974, pages 79--119). People do not talk about it a lot because it was a well-focussed problem which got a perfectly good answer and at the time there more pressing and more open-ended research issues. Perhaps also because Saunders Mac~Lane tended to stress that lots of higher set theory (like lots of logic in general) is very weakly linked to most of mathematics -- which is true, but is not to say that higher set theory (or logic in general) need be abandoned. He hoped they could be brought back into better touch. This is the issue raised for example by Feferman and Rao in Giandomenico Sica ed. _What is category theory?_ {Polimetrica, 2006) when they claim it is "unclear" whether certain ZF constructions can be given at all in categorical terms. Yes, it is clear they can, proven in detail by Osius in 1976 (not the first proof but my favorite reference on it). On the other hand, for some purposes we want to replace the category Set (no matter how it is axiomatized) by something more general, often by any elementary topos, or it could be any Boolean topos, or category with a category of classes. The categorical replacement scheme I mentioned generalizes very well to any well-pointed topos, but that is little more general than Set. It makes much use of fibers over global elements. To put it in the terms I like, it does nothing to say a family of sets S-->I defined by replacement should be "smooth" or "continuous over the index set I" in anyway. In Set the index *set* is not smooth or continuous to begin with, it is a discrete set. The idea of categories of classes is to get some sense of large collections that *do* vary "smoothly" or "continuously" when the base has some smooth or continuous character (in a very general sense, so for example effective computability is the relevant "smoothness" for those types in the effective topos close to the natural numbers). The next question brings us back to the first perspective. It is about the category Set, but wants to approach that category by categorical tools.
This raises another question. You mention at the end of this paper that large-cardinal axioms are "routinely pursued in isomorphism-invariant terms". This is clear to me for many types of large cardinals, but not for the stronger ones that involve elementary embeddings of the universe of sets. Ultrapowers have a categorical analogue, of course (filterquotient) but then there is a transitive collapse of the entire universe, from which I don't see immediately how to eliminate the global membership predicate. Can you give a clue or a reference?
Within ZF itself the global membership predicate X \in S is just one guise of the relation "the membership-tree of X is (isomorphic to) the restriction of the membership-tree of S to some node directly below the top." Transitive collapse can be re-cast in these terms as dealing with all well-founded extensional relations and not only dealing with restricted membership (i.e. restricted to some inner model of ZF) and actual membership of sets. In isomorphism invariant terms, a transitive collapse of the universe means a uniform method of taking any well-founded extensional relation (not just ZF membership on each transitive closure) and restricting it to a sub-relation which is still well-founded and extensional (which we do not bother collapsing to membership on some transitive closure) while preserving some properties of the first relation. And then we ask if a given collapse has any fixed points: are there any well-founded extensional relation so big that this collapse leaves an isomorphic relation? I have no idea what the practical effect would be of recasting collapse in these terms. I have never worked with large cardinals and transitive collapse. But it certainly *can* be recast this way. Some one should try it. best, Colin
If one assumes that epics split and that the Boolean algebra of subsets of 1 reduces to two elements, then (to a first approximation) the main effect of axiom schemes is to provide larger cardinals. That is explicitly exemplified in the document that has been available in the University of Chicago Math Library since 1965, and that has been available in recent years as a TAC Reprint. Using the definable classes of sets smaller than any given set, the postulate that there are arbitrarily large such classes closed under arbitrary definable operations phi is proposed. I am not aware of any further studies of that postulate. (This may be the first time that a geometer has shown persistent interest in replacement) Of course above I use the term "class" in the intuitive sense of a natural subset of every model of the theory ("meta-" in Mac lane's terminology), that objective meaning corresponding subjectively to a formula of the theory. That is, not in the sense of a half- hearted attempt to represent classes by elements V of the model. (Less half-hearted is the proposal that seems implicit in the 1963 reaction of Goedel & Bernays themselves when they heard, presumably from Kreisel, that work was underway on a categorical set theory. Namely try a category of classes of classes etc satisfying at least the intuitive property of cartesian closure.) The usual replacement scheme does seem at first to yield only cardinals smaller than given ones. But in the hierarchical view, that quotient set consists of elements which themselves have elements, thus the actual mathematical content is that of a family of sets, a concept whose geometrical expression is that of a fibration, hence Colin's formulation of the axiom. Indeed the formulation goes back many years, but I don't have a reference. Concerning an elementary self-embeddings of the universe, it is in any case an additional functor added to the basic structure, and since the basic structure of category is first-order, a scheme could be considered to the effect that such a functor commute with quantifiers. Bill On Wed Mar 12 23:37 , "Michael Shulman" sent:
On Sat, Mar 8, 2008 at 2:45 PM, Colin McLarty colin.mclarty@case.edu> wrote:
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. [...]
Thank you! This is exactly what I was looking for.
This has been known from the earliest days of categorical set theory.
But it doesn't seem to be *well* known any more, or at least well-disseminated and exposited. Several people have told me that they didn't think it was possible to express replacement category-theoretically without using a category of classes. And even now knowing what I'm looking for, I am unable to find more than a sentence or two about it in any book on topos theory, none of which actually gives any version of the axiom.
AUTHOR = "McLarty, Colin", TITLE = "Exploring Categorical Structuralism",
This raises another question. You mention at the end of this paper that large-cardinal axioms are "routinely pursued in isomorphism-invariant terms". This is clear to me for many types of large cardinals, but not for the stronger ones that involve elementary embeddings of the universe of sets. Ultrapowers have a categorical analogue, of course (filterquotient) but then there is a transitive collapse of the entire universe, from which I don't see immediately how to eliminate the global membership predicate. Can you give a clue or a reference?
Thanks again, Mike
wlawvere@buffalo.edu Thursday, March 13, 2008 9:20 pm Wrote, with much else, about an equivalent to the axiom scheme of replacement in ETCS, and his mimeographed notes on it now reprinted at TAC http://138.73.27.39/tac/reprints/articles/11/tr11abs.html
Using the definable classes of sets smaller than any given set, the postulate that there are arbitrarily large such classes closed under arbitrary definable operations phi is proposed. I am not aware of any further studies of that postulate.
It is right at the end, on p. 34 of the reprint. To me, it is really a very nice stream-lined version of a reflection principle and deserves more of a look. Up to now I have tended to translate it into a replacement scheme because they are more familiar to my audience. But it is much more elegant as it cuts straight down to a very elegant isomorphism-invariant principle. best, Colin
participants (5)
-
Colin McLarty -
Michael Shulman -
Steve Awodey -
Thomas Streicher -
wlawvere＠buffalo.edu