In his comments to both cody and Nik Weaver regarding his answer to user7280899's mathoverflow question "What kind of foundation are mathematicians using when proving metatheorems?", Mike Shulman writes:

I care more about not relative consistency, but "interpretability": that you can directly construct a model of one theory from the other theory in a relatively straightforward way. This tells us how to actually relate (at least in principle) mathematics formalized in the two theories. If someone proves a theorem in $ZFC$, then I understand directly what it means in $SEAR$ [Sets, Elements, And Relations] as a theorem about hereditarily well-founded relations, and vice versa: a theorem in $SEAR$ is a theorem in $ZF$ about the category of sets...Put differently, consider the category of models of $ZF$ and the category of models of $SEAR$. To say $Con(ZF)$ $\Leftrightarrow$ $Con(SEAR)$ is to say that if one of these categories has an object, so does the other. I would much rather know that these categories are related by an adjunction or an equivalence, even if I need a stronger metatheory.

Which brings me to my question:

How are material set theory and structural set theory related from the point of view of category theory? More specifically, how is the category of models of $ZF$ related to the category of models of $SEAR$ from the point of view of category theory? And what is the significance of this relation to the foundations of mathematics (since Set Theory and Category Theory have been considered (per se) to be alternate foundations for mathematics)?

  • $\begingroup$ @Vincent: Thanks for the edit. Very nice. $\endgroup$ Feb 9, 2017 at 14:27
  • 1
    $\begingroup$ Most set theorists also care more about relative interpretability than relative consistency, which is why we value forcing arguments, for example, over mere relatively consistency results. Meanwhile, when one statement has higher consistency strength than another, however, one can use this to show the absence of an interpretability result, which otherwise would be very hard to prove. $\endgroup$ Feb 9, 2017 at 15:47
  • $\begingroup$ @JoelDavidHamkins To be sure; I didn't mean to imply otherwise. $\endgroup$ Feb 9, 2017 at 18:21

1 Answer 1


I think this question has not been satisfactorily studied, but we can say something. Firstly, note that since a model of SEAR (or other structural set theory) is really a category, such models form not a 1-category but a 2-category.

It's easy to see that the two model constructions act functorially on isomorphisms of models of ZF and on equivalences of models of SEAR. Moreover, any model of ZF can be reconstructed (up to isomorphism) from its category of sets (since by the axiom of foundation and Mostowski's collapsing lemma, transitive sets are the same as well-founded extensional relations), and any model of SEAR+choice can be reconstructed (up to equivalence) from its ZF-model (since by AC, any set can be well-ordered, which is a well-founded extensional structure). So the sets of isomorphism classes of models of ZFC and equivalence classes of models of SEARC are isomorphic.

I don't know to what extent these isomorphisms are natural or 2-natural even on equivalences. (Since well-founded extensional structures admit no nonidentity automorphisms, if they were 2-natural then the 2-groupoid of models of SEARC would in fact be a 1-groupoid; I don't even know whether that's likely to be true.) Moreover, it's not as clear what to do about non-invertible morphisms. The only reference I'm aware of that really discusses this question is Mitchell's Categories of Boolean topoi from 1973, in which he comes close to constructing some kind of adjunction, although he didn't use 2-categorical language.

  • $\begingroup$ @MlkeShulman: Thanks for your answer and the links to the Mitchell papers--very helpful. Do you see any implications for the foundations of mathematics coming out of knowing the relations between material and structural set theories? $\endgroup$ Feb 10, 2017 at 8:59
  • $\begingroup$ The bi-interpretability of the two theories is of course very important, because it means that in a formal sense they are equally sufficient as foundations for mathematics. And the isomorphism of equivalence classes that I mentioned means, in a sense, that moreover neither one contains "more information" than the other. But I don't know of any "foundational" implications for a functorial enhancement of this equivalence. $\endgroup$ Feb 10, 2017 at 11:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.