Timeline for How do we compare models of ETCS?
Current License: CC BY-SA 2.5
17 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 19, 2010 at 14:04 | comment | added | Andreas Blass | 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. | |
| Oct 19, 2010 at 3:25 | comment | added | Joel David Hamkins | If span just means that there is an $E'$ with logical functors into both, then if the functors are arithemtic-truth-preserving, then there could be no span either when the arithmetic theories of the models of set theory are not the same. But I'm not sure about the extent to which we can expect the functors to be arithmetic truth-preserving---Mike Shulman once told me something definite about this, and perhaps he'll show up here. | |
| Oct 19, 2010 at 3:02 | comment | added | Todd Trimble | 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)? | |
| Oct 19, 2010 at 2:55 | comment | added | Joel David Hamkins | Todd, to make it more concrete, if one model has an integer solution to a certain diophantine equation, then I think that the image of that solution under a logical functor would have to satisfy the same equation in the other model. Thus, if the two models disagree about whether there is a solution (which is possible), then there can be no logical functor in that direction. | |
| Oct 19, 2010 at 2:37 | comment | added | Todd Trimble | ... 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. | |
| Oct 19, 2010 at 2:32 | comment | added | Todd Trimble | ...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.) | |
| Oct 19, 2010 at 2:22 | comment | added | Todd Trimble | 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.) | |
| Oct 19, 2010 at 1:48 | comment | added | Joel David Hamkins | 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? | |
| Oct 19, 2010 at 1:24 | comment | added | Joel David Hamkins | 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. | |
| Oct 19, 2010 at 1:20 | comment | added | Joel David Hamkins | 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. | |
| Oct 19, 2010 at 1:10 | comment | added | Joel David Hamkins | 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. | |
| Oct 19, 2010 at 1:02 | comment | added | Todd Trimble | 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. | |
| Oct 19, 2010 at 0:50 | comment | added | David Roberts♦ | Arg, what happened to the LaTeX in my comment? | |
| Oct 19, 2010 at 0:46 | comment | added | David Roberts♦ | But you can't even talk about the isomorphism or otherwise of two $\mathbb{N}^M$ as they are objects of different categories. And one can legitimately talk about a functor that maps the NNO from one model to the other model: a functor doesn't give a function from one NNO to the other after all. One would need, OTOH, a map $End(\mathbb{N}^{M_1}) \to End(\mathbb{N}^{M_2})$, for example. If the functor preserved NNOs, then it might be a bit tricky, but I don't have any idea what would happen then. | |
| Oct 19, 2010 at 0:32 | history | edited | Joel David Hamkins | CC BY-SA 2.5 |
added 365 characters in body
|
| Oct 18, 2010 at 23:57 | history | edited | Joel David Hamkins | CC BY-SA 2.5 |
added 15 characters in body
|
| Oct 18, 2010 at 23:52 | history | answered | Joel David Hamkins | CC BY-SA 2.5 |