And perhaps after that, May's The Geometry of Iterated Loop Spaces.

Awesome embedded image, Chris.

Thank you, KP Hart. I discovered a few days ago that this is the proof in Bourbaki (and it is also the point-set version of the localic proof alluded to by Mike Shulman in his answer, given by Johnstone in the Elephant).

"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.

Yes, that I agree with (and thanks for putting it concretely). And that certainly answers the first part of David's 3. Do you have a feeling about the second part (he asked whether any two models $E$, $E''$ could be connected by a span $E \leftarrow E' \to E''$, and based on something else he said he might be interested in more elaborate zigzags)?

... functor would afford a direct comparison between NNO's along the lines of having an elementary equivalence between them. It could be just a matter of inexperience on my part with models of (bounded) Zermelo set theory and what logical functors between them would entail, and I am open to being convinced by you, but I'm not seeing what you're saying at all clearly yet.

...is $N \times 2 \to 2$, and the logical functor $f: E \to E'$ given by pulling back along one of the elements $1 \to 2$ preserves NNO. (If it helps, you can think of $E'$ as a universe of Boolean-valued sets where the truth values lie in the Boolean algebra $P(2)$.) Internal to $E'$, the elements of its NNO are pairs of ordinary natural numbers; this NNO does not embed in the NNO of $E$. Now this example may seem unfair since $E'$ is not a model of ETCS, but suffice it to say that I have many such examples from topos theory that make me wary of believing that just having a logical (cont.)

Joel, it would take me quite a while to wrap my head around the question you just put to me, as we come perhaps from different mathematical cultures and my set theory is not particularly strong. So instead of trying to tackle your question head-on, I'll try to give the flavor of what I have in mind using slightly different examples from topos theory. There it is quite possible to construct a logical functor $f: E \to E'$ which takes the NNO of $E$ to the NNO to $E'$, but without one NNO being embedded in the other. For example, if $E$ is the topos Set/2 and $E'$ is Set, the NNO of $E$ (cont.)

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).

I agree this answers questions 1 and 2. I think there is some lingering question as to what one takes the morphisms between models of ETCS to be; for a category theorist, the notion of "logical functor" would be a natural choice, but a model theorist might gravitate toward something else (like elementary equivalence?). The answer to question 3 might depend on what one chooses. Logical functors preserve truth but do not necessarily reflect truth, so they can sometimes map one NNO to another even if the NNOs have somewhat different properties.

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)?

This discussion should probably be brought to a close (if you want you can write me at topological dot musings at gmail dot com), but in which statement of mine does it seem to you that I am missing the well-known fact that independence phenomena are embedded in theories? The question as to "how these issues are dealt with in category theory" has been partially addressed by Francois, but you seem to be advancing the idea that "category theory" gets it wrong somehow. I guess there are inexperienced category theorists who get it wrong sometimes, but I don't see that's happened here. Bye!

("Penultimate" now referring to the one beginning "no, if the set you have defined...")

@burned: your penultimate comment seems very confused. I'll reply to two things though. (1) "if the set you have defined exists or doesn't (in any form) then you have just made an assertion that extends beyond ZFC". What set? Say, the set of subsets of the reals whose cardinality is uncountable but less than the continuum? That set of subsets exists (using separation), even though such subsets may not. (2) "my problem is with logical consequences of being able to actually produce the value of such a limit". Whoever said that you can (always)?

@burned: in ZFC it is provable that small diagrams have limits and colimits. (The completely different question of whether the set of Suslin lines is empty or nonempty is different to the existence of that set. Are you confusing existence of the set with existence of elements of the set?)