2
$\begingroup$

(By request from a comment: UF stands for Univalent Foundations)

Correct me if I'm wrong, but in a model $M$ of ZF each element $x$ of $M$ should produce a directed-graph-with-a-marked-sink $G_x$ having $x$ as marked sink, as follows: to $\varnothing$, i. e. the element with no $y$ satisfying $y\in\varnothing$, assign the graph with the single node $\varnothing$ which is marked, and no arrows. If the graphs $G_y$ for each $y\in x$ are known, then let $G_x$ be the disjoint union of all $G_y$, one more node $x$, and new arrows $y\to x$ for each $y$, with $x$ marked.

Something like univalence would tell us that if there is an isomorphism between $G_x$ and $G_{x'}$ under which isomorphism $x$ and $x'$ correspond to each other, then it must be the case that $x=x'$.

Does every model of ZF satisfy this? If yes, is it trivial? If no, are there some additional axioms known that would ensure it?

On the other side, does this construction allow to construct a model of ZF from every univalent universe? If yes, is it trivial? If no, are there some additional axioms known that would ensure it?

Last question - are these matters addressed somewhere? Where can I read about it?

Improve this question
$\endgroup$
13
  • 7
    $\begingroup$ I think the answer is essentially, "see Mostowski's collapse lemma." $\endgroup$
    – Monroe Eskew
    Commented Oct 21, 2020 at 10:23
  • $\begingroup$ @MonroeEskew Could you elaborate please? Do you imply that one does not need any additional axioms? $\endgroup$
    – მამუკა ჯიბლაძე
    Commented Oct 21, 2020 at 12:44
  • 3
    $\begingroup$ Regarding the part of the question pertaining to univalence, see Section 10.5 of the HoTT book, where models of ZF are built using inductive types. $\endgroup$
    – Andrej Bauer
    Commented Oct 21, 2020 at 13:13
  • 4
    $\begingroup$ If I am reading/translating correctly, you are describing a way of encoding the transitive closure of a set into a directed graph, aka binary relation, by recursion on rank. Mostowski's lemma says that for any well-founded extensional binary relation $E$ on a set $X$, $(X,E)$ is isomorphic in a unique way to a unique structure $(Y,\in)$, where $Y$ is transitive-- this is called the transitive collapse of $(X,E)$. So since ZF includes Extensionality and Foundation, we get that if $G_x \cong G_{x'}$, then the transitive collapses are the same and hence $x=x'$. $\endgroup$
    – Monroe Eskew
    Commented Oct 21, 2020 at 13:24
  • 4
    $\begingroup$ If you start with two sets $x,x’$, then the digraph $G_x$ is isomorphic to $(\mathsf{trcl}(\{ x \}),\in)$ and the same for $x’$. By Mostowski, there is no other transitive set $y$ such that $G_x \cong (y,\in)$. So if $G_x \cong G_{x’}$, then it must be that $x=x’$ since they are both the highest rank object in the transitive $y$ as above. $\endgroup$
    – Monroe Eskew
    Commented Oct 21, 2020 at 18:24

1 Answer 1

Reset to default
8
$\begingroup$

This is a standard way of building a model of "material" / membership-based set theory (such as ZFC) from a "structural" / categorical set theory (such as ETCS or the sets in HoTT/UF). In the context of comparing membership-based set theories to category theory and topos theory, it goes back at least to the work of Mitchell, Cole, and Osius in the 70s. There are various different versions of it that use rigid trees (which I think is what you describe) or extensional graphs (a quotient of the tree). A more recent sketch of one using trees can be found in Mac Lane and Moerdijk's Sheaves in Geometry and Logic. I recently wrote a detailed exposition [1] of the extensional-graph version that compares the strength of various axioms on both sides of the translation. The construction in the HoTT Book that Andrej mentioned was inspired by these older versions, and I believe is essentially equivalent, though it is formulated in terms of an inductive construction of the entire universe of sets (related is Joyal-Moerdijk's book Algebraic set theory, LMS Lecture Note Series 220 (1995) doi:10.1017/CBO9780511752483).

In particular, if you start from a model of ZFC, take its category of sets, then rebuild a model of ZFC, you get something isomorphic to the model you started from (because of Mostowski's collapsing principle, as mentioned in the comments). Thus, every model of ZFC can be obtained in this way. (However, for weaker set theories less can be said.)

[1] Comparing material and structural set theories, Annals of Pure and Applied Logic 170 Issue 4 (2019) 465–504, doi:10.1016/j.apal.2018.11.002, arXiv:1808.05204

Improve this answer
$\endgroup$
5
  • $\begingroup$ Thank you! Just one thing that I don't understand, please: your last argument about rebuilding only shows that you can obtain any model of ZFC from something not necessarily univalent. Can one also see that any model of ZFC can be obtained from some univalent universe? $\endgroup$
    – მამუკა ჯიბლაძე
    Commented Oct 22, 2020 at 5:18
  • 1
    $\begingroup$ @მამუკაჯიბლაძე Well, that gets a little fiddlier with universes, since univalence is a property of a universe, while an arbitrary model of ZFC may contain no universes. But if your model of ZFC does contain a universe (i.e. an inaccessible cardinal), then Voevodsky's simplicial model constructed from it contains a univalent universe, and the model of sets in that univalent universe should be isomorphic to the small sets (those of rank below the inaccessible) in your original model. Although I don't know if anyone has proven that carefully. $\endgroup$
    – Mike Shulman
    Commented Oct 22, 2020 at 14:37
  • $\begingroup$ One might also hope that starting from an arbitrary model of ZFC one could build a "class model" of HoTT in which the universe of sets in the model is univalent, and from which one could reconstruct the original model. But I don't think anyone has done this either. $\endgroup$
    – Mike Shulman
    Commented Oct 22, 2020 at 14:38
  • $\begingroup$ I see. So if you construct a model of ZFC from "something structural", there is no way to judge from this model alone whether that something was univalent in one sense or other? $\endgroup$
    – მამუკა ჯიბლაძე
    Commented Oct 22, 2020 at 14:54
  • 1
    $\begingroup$ Yes, a model of ZFC is purely set-level, so it doesn't know about anything univalent. $\endgroup$
    – Mike Shulman
    Commented Oct 22, 2020 at 15:32

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .