## How do we compare models of ETCS?

The elementary theory of the category of sets (nLab) gives axioms on a category such that it is a category of sets. In answering this MO question I realised that we might have trouble comparing different models of ETCS. So here are some questions starting with easy ones (which I should know the answer to!) to the more difficult.

1. Are two models of ETCS necessarily equivalent categories?

2. Are two models of ETCS equivalent as well-pointed topoi with NNO and Choice?

3. Is there a functor (Edit: a logical functor, as Todd pointed out) between any two models of ETCS? A span?

4. Do models of ETCS necessarily even belong to the same category?

I wonder, because the sets that one model of ETCS has as hom-objects may be completely different to the sets that the other model has as hom-objects, and there is a priori no way to map between them.

-
For question 3, surely you mean not just "functor", but a "logical functor" which preserves finite limits, power objects, and natural numbers object? I'm not even sure what you mean by 4 (I mean, why not: just take objects to be ETCS categories and morphisms to be logical functors)? – Todd Trimble Oct 19 2010 at 0:24
Hmm, re 4: I suppose so. But are there many arrows in this category? Is it connected? I could be completely naive and ask: is there a weakly initial object? (The constructible universe, perhaps?) – David Roberts Oct 19 2010 at 0:48
And regarding 3: I really meant, 'is there a functor?', but this would allow silly functors like those mapping everything to the empty set. Let us say at least preserving finite limits. The flavour of set theory one is using clearly affects things like NNOs, as Joel pointed out (and I was aware of to begin with). – David Roberts Oct 19 2010 at 0:50
You probably want more than preservation of finite limits since otherwise you could just map everything to the terminal object. Being a category theorist, I think "logical functor" seems like a natural choice. If that is the choice, I believe there is no weakly initial object (and I could maybe rummage up some relevant nLab pages). – Todd Trimble Oct 19 2010 at 1:07
"Elementary" here refers to a theory which doesn't make reference to an external notion of set in the background. For example, when we refer to a small or locally small category, we refer to a background notion of set, whereas here the development is to be independent of any such prior notion. The terminology is due to Lawvere. – Todd Trimble Oct 19 2010 at 3:14

(Caveat: I come from set theory rather than category theory and know only a little about ETCS.)

The answer to your question is no. The basic reason is that even the models of set theory themselves can differ vastly. If $M$ is a model of ZFC, then the category $Set^M$, which is Set as interpreted in $M$, will be a model of ETCS. But if ZFC is consistent, then the models of set theory $M$ are diverse. For example, some have CH and others have $\neg CH$, and furthermore, by the incompleteness theorem, they can satisfy different arithmetic statements. Such statements show up in the category $Set^M$, since every arithmetic statement (first order statement about natural numbers) has a translation into the formal language of ETCS. So in general these categories are not elementary equivalent in the language of ETCS. In particular, the natural numbers objects of such categories will not in general be isomorphic, and so there can be no nice functors between the categories. For example, by the Lowenheim-Skolem theorem, some models of set theory will be countable and others will have an uncountable set of natural numbers, with a different theory, and these aspects will prevent their corresponding Set categories from being equivalent as categories or from having nice functors. In general, it will not be possible to map the natural number object from one to the other in any nice way.

-
The two Set's are two different categories, and you are asking for a functor between them. My point is that if the functor is at all nice, then this induces an isomorphism of the natural number objects with their successor functions, or at least an embedding from one to the other, which can be impossible. The isomorphism does not live in either of these categories, but in the set-theoretic background where the functor lives. In any case, the two models can have different arithmetic truths, and this arises in the theory of the categories, so they needn't be elementarily equivalent. – Joel David Hamkins Oct 19 2010 at 1:10
David, it is sensible to compare the natural number objects of two different models of ZFC, since these are just two models of PA, which can be considered (set-theoretically) outside of the context of the models of set theory in which they live. – Joel David Hamkins Oct 19 2010 at 1:20
Ah, I see now that perhaps you are confused and thought I was changing the ambient set-theoretic background, but no, I just mean to consider two set models of ZFC, which have different arithmetic truth. Thus, we get two categories of ETCS that are inequivalent as categories. – Joel David Hamkins Oct 19 2010 at 1:24
Todd, won't logical functors be fully truth-preserving for first-order arithmetic truth on the NNOs themselves, since full first order arithmetic truth corresponds to $\Delta_0$ truth in the larger structure, as all quantifiers are bounded by the NNO itself? That is, logical functors are $\Delta_0$-elementary on the full category, and this means fully first order elementary for arithmetic truth, right? – Joel David Hamkins Oct 19 2010 at 1:48
Logical functors between topoi preserve everything that can be expressed in the internal logic of the topoi. For models of ETCS, that would include not only first-order but also higher-order arithmetic. As Joel pointed out, even if we consider only models of ETCS that arise from models of (a sufficiently large fragment of) ZFC, they can disagree about many such statements. Such a disagreement prevents logical morphisms, spans, and even longer zigzags of logical morphisms. The category of models of ETCS and logical morphisms is therefore badly disconnected. – Andreas Blass Oct 19 2010 at 14:04