10
$\begingroup$

Suppose a statement $\phi$ that doesn't use the global $\in$-relation or the global $=$-relation in an essential way is provable in some material set theory, say bounded Zermelo with choice. (So that the statement $\phi$ itself essentially is structural while, in theory, the intermediate steps in the proof of $\phi$ might be material, thus containing the global $\in$-relation or the global $=$-relation in an essential way!) Can it be proved that $\phi$ (or, rather, the translation of $\phi$ into the appropriate structural set theory) is nevertheless provable in some structural set theory, say ETCS, meaning that all the material intermediate steps can be eliminated? (Note that since $\phi$ doesn't use the global $\in$-relation or the global $=$-relation in an essential way, such a translation should exist.)

Of course, in practice, most proofs are already structural. But who knows what crazy things could be done in theory by exploiting the global $\in$-relation?

I already know that ETCS and bounded Zermelo with choice are equiconsistent. Though related, it seems I'm asking for something stronger.

Improve this question
$\endgroup$
16
  • 3
    $\begingroup$ What is "global $\in$-relation" and "global $=$-relation", and what does it mean to (not) use them in an "essential way"? $\endgroup$
    – Wojowu
    Commented Mar 29, 2021 at 12:51
  • 3
    $\begingroup$ It depends on the specific theories involved. $\endgroup$
    – Monroe Eskew
    Commented Mar 29, 2021 at 13:04
  • 3
    $\begingroup$ @Wojowu in material set theories like ZF you are allowed to use the $\in$ or $=$ relation for arbitrary sets (it makes sense to ask whether $2 \in \pi$ or $exp = \mathbb{Q}$). In a structual set theories it only makes sense to ask whether two elements of a same sets are equal, or whether an element of a set X belong a subset U of X. I think the concrete formulation of the question is "Given a statement in the language of, say, ETCS which can be proved - when translated - in bounded ZF, can it be proved in ETCS ?" $\endgroup$
    – Simon Henry
    Commented Mar 29, 2021 at 13:16
  • 3
    $\begingroup$ @Simon: In structural set theory it makes sense to ask "is $\sqrt2$ surjective?" $\endgroup$
    – Asaf Karagila ♦
    Commented Mar 29, 2021 at 13:56
  • 5
    $\begingroup$ @Simon: I'm sorry if I'm somewhat aggressive here. My point here is that people treat this as a good reason to think that ZFC is not "worth the effort", and in a world where I repeatedly hear about how set theory "is dying out", repeating these claims that somehow structural set theory is "free of junk" is both false and damaging to an entire field of mathematics. So I get a bit anxious when I see it. $\endgroup$
    – Asaf Karagila ♦
    Commented Mar 29, 2021 at 14:59

1 Answer 1

Reset to default
11
$\begingroup$

This will obviously be highly dependent on the concrete theory you are considering. But overall the answer is yes.

The most general version of these results I'm aware of are in Mike Shulman's Comparing material and structural set theories. You'll find all the answer you want in this paper. But let me try to give you some pointers: I think the most relevant result here is lemma 9.1 which (roughly, see the paper for the details) says:

"Given $\mathbf{Set}$ ( a suitable pretopos, for eg. a model of ETCS) then the inclusion $\mathbb{S}\mathbb{V}(\mathbf{Set}) \to \mathbf{Set}$ is an equivalence if and only if every object of $\mathbf{Set}$ can be embedded into an extentional well founded graph"

where $\mathbb{V}$ denotes the construction described in Mike's paper that attach a material set theory to a structural theory and $\mathbb{S}$ takes a material set theory to its category of sets.

Any formula in $\phi$ in the language of a structural set theory is in particular a forumla in the 'language of categories' so is invariant by equivalence of categories. So, if the lemma applies, a formula $\phi$ is valid in $\mathbf{Set}$ if and only if it is valid in $\mathbb{S}\mathbb{V}(\mathbf{Set})$ that is exactly if the material translation of $\phi$ is valid in $\mathbb{V}(\mathbf{Set})$.

So if the material translation of $\phi$ is provable in the theory of $\mathbb{V}(\mathbf{Set})$ then it holds in $\mathbf{Set}$. If $\mathbf{Set}$ is a model of ETCS, then $\mathbb{V}(\mathbf{Set})$ satisfies Bounded Zermelo with choice ( and Mostowski principle and transitive closure, again, see mike's paper for the details). So that answer your question.

Note that, In the general case, the key condition is whether in $\mathbf{Set}$ every object can be embedded into an extentional well founded graph. Working with ETCS, or more generally if you have choice then this is really not a problem (e.g. put a well order on your set), but in more generality it might be problematic:

By construction material set theory (well founded and with transitive closure) always construct a set as a subset of an extentional well founded graph (its transitive closure with the $\in$ relation), so if your structural set theory cannot do this as well, this gives a counter-example to the question you are asking, as the existence of such an embedding is a meaningful structural statement.

Maybe there is a generalization of this construction that allows to get non well founded set theories that would go arround this problem, but I am not aware of this having been studied (?).

Improve this answer
$\endgroup$
1
  • 4
    $\begingroup$ There is certainly a generalization to non-well-founded set theories, although I don't know if it's been written down. However, it doesn't go around the problem completely, because you still have to impose some extensionality conditions on the graphs, and AFAIK there is still no way to prove structurally that every set can be embedded into such a graph, even though the class of graphs is now somewhat wider. $\endgroup$
    – Mike Shulman
    Commented Mar 29, 2021 at 14:50

You must log in to answer this question.

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