# Does equality between sets contradict the philosophy behind structural set theory?

Zermelo-Fraenkel set theory (with choice) is commonly accepted as the standard foundation of mathematics. It is a material set theory. This means that for every two objects/sets $a,b$ one can ask whether $a=b$ or not. Also, one can always ask whether $a∈b$ is true or not. So $\in$ is a global element relation.

As an alternative foundation for set theory, Lawvere proposed ETCS (= elementary theory of the category of sets). It is the standard example of a structural set theory. The idea behind structural set theory is that elements—in contrast to material set theory—have no internal structure, i.e. are just "abstract dots". Thus there there is no global element relation, and "objects" are not indepedent things, they always lie in a particular structure (for example, we cannot speak about 2 as an object that exists on its own, but we instead talk about the "2 in the structure IN" or the "2 in the structure IR", and strictly speaking, these are not the "same" objects, but we have a natural injection IN -> IR which maps the "natural number 2" to the "real number 2").

There have been controversial discussion whether ETCS is more appropriate as a foundation for mathematics than ZFC. I don't want to discuss this here, but want to point you to this paper:

https://arxiv.org/pdf/1212.6543.pdf

in which Tom Leinster introduces ETCS and argues that this foundational system is much nearer to the practice of mathematicians than ZFC.

Quite at the end of the paper, Leinster states that Sets for Mathematics by Lawvere and Rosebrugh is the quite the only book that teaches set theory in the flavour of structural set theory (ETCS)—which makes sense, since Lawvere is the "founder" of structural set theory.

Now, let me come to my question: Does equality between sets contradict the philosophy behind structural set theory? Obviously, when doing set theory in the spirit of structural set theory, we don't need equality between sets. Instead, we talk about isomorphisms, which makes more sense structurally. Also, the typical definition of equality between sets (extensionality) can't be formulated in ETCS. Thus it seems to me that the notion of "equality between sets" doesn't make much sense in structural set theory. Of course, we could say that two sets are equal if there is a bijection between them, or state that equality exists between sets without further specifying what it does (in particular, if we identify all isomorphic sets, whether there are infinitely many isomorphic sets that are not equal, ...). But this wouldn't yield to additional value, and is thus superfluous. Having this thoughts in mind, I was surprised when I read the following in Sets for Mathematics—the standard text book for structural set theory (on page 2!):

Notation 1.1: The arrow notation f : A -> B just means the domain of f is A and the codomain of f is B, and we write dom(f) = A and cod(f) = B.

Here, the authors talk about the equality of two sets (dom(f) = A). They also use the "big bag of morphisms"-definition of category and not the "by pairs (A, B) of objects indexed family of hom-sets". But in this definition, one must talk about operations dom and cod which specify for each morphism a unique domain and codomain. But the word "unique" here presupposes that we have a notion of equality between objects.

Could someone from the foundations of mathematics clarify my confusion? On the nLab (see https://ncatlab.org/nlab/show/category ) there are two definitions of the term "category" ("With one collection of morphisms" and "With a family of collections of morphisms"), and to me it seems the second ("With a family of collections of morphisms") is more appropriate for structural set theory. But then, why does Lawvere—the founder of structural set theory—uses the first one ("With one collection of morphisms") in the only book about structural set theory?

• I'd like someone more steeped in (e.g.) type theory to answer more fully, but you probably want to read up on the distinction between equality judgments and equality propositions. In a material or membership-based set theory like ZFC, there is a criterion for proving an equality proposition. Whereas in a structural set theory, the statement $A = B$ as an equality between objects is not something one can prove in the theory, but is a judgment made as a meta-statement. See ncatlab.org/nlab/show/equality Feb 24 '17 at 18:10
• @ToddTrimble: I think the equality used here is not just a judgement, but a proposition. Feb 24 '17 at 18:37
• Why would you say that? Feb 24 '17 at 19:21
• @ToddTrimble: Because, as far as I understand the difference between judgements and propositions, judgements always stay alone: we can only "prove" them, but we can't negate them nor combine judgements to complex ones (like "A and B", "A or B", "(A and B) implies (C or D or F)"). But with propositions we can do that. Lawvere uses the combound statement "$dom(f) = A$ and $cod(f) = B$" and denotes it by $f : A\to B$. That's why I think the equations must be propositions rather than judgements. Feb 24 '17 at 19:29
• You can perform some combinations with judgements. It's very common to say $P \vdash J$, where $P$ is a proposition and $J$ is a judgement; this is analogous to $P \to J$ (if $J$ were also a proposition). Similarly, if you say $J_1$ and then say $J_2$; then you have effectively said $J_1 \wedge J_2$. That said, I believe that you are correct that Lawvere treated everything as propositions; there is certainly nothing in Sets for Mathematics that suggests a distinction between propositions and judgements to me. Feb 24 '17 at 20:40

I can't give you an answer that fully addresses what Lawvere and Rosebrugh were thinking, since I haven't asked them. (If you want to ask them, Rosebrugh runs a category-theory mailing list at https://www.mta.ca/~cat-dist/; he is an active participant, and Lawvere has been known to comment from time to time as well.) But I can say something about what can be done with equality between objects in ETCS.

For the most part, I think that ETCS has equality between objects by default. First-order logic, as usually treated, is both untyped and equipped with a global equality predicate, and since ZFC is usually written in such a first-order logic, Lawvere wrote ETCS in that logic too. Using an untyped logic requires him to put all morphisms into a single class (and to put objects in that class as well, identifying an object with its identity morphism), which means that he needs that global equality predicate.

On the other hand, it's quite possible to write ETCS in a typed first-order logic, with a type of sets, a dependent type of morphisms (dependent on two terms of the type of sets), and a dependent equality predicate for morphisms, but no equality predicate for sets. This is how Leinster does it; although he doesn't say things like ‘dependent type’ and ‘equality predicate’, such types and predicates are what appear in his paper. (And while he never denies the existence of an equality predicate between sets, no such predicate appears in his paper either.)

I think that Leinster's way of putting it is more in the structural spirit than Lawvere's, for the reasons in your question. But I don't think that Lawvere made a conscious choice to reject that argument either.

• Some additional comments to not clog up the answer: When Mike Shulman wrote SEAR (ncatlab.org/nlab/show/SEAR), a structural set theory intended to look less like category theory than ETCS (and in particular based on elements and relations rather than functions as the main concepts), he made a deliberate choice to write it in a dependently typed logic without an equality predicate on the type of sets. But just as ETCS can also be written in such a logic, so SEAR could also be written in an untyped logic with a global equality predicate. Feb 24 '17 at 21:31
• If I want to post to that mailing list, what should I do? Just write an email to categories@mta.ca and then they write back to me? Or do I need to subscribe somewhere? Feb 24 '17 at 21:34
• Even among category theorists, there has been resistance to the idea that the category of sets does not come with a notion of equality of objects stronger than isomorphism. If you write down a general-purpose definition of category in the language of set theory (and it's irrelevant whether that set theory is material or structural), then a category has a set (or class) of objects, so objects can be compared for equality. I discuss these issues at ncatlab.org/nlab/show/strict+category, although maybe that should be edited to be easier for newcomers to follow. Feb 24 '17 at 21:38
• Last additional comment: In type theory, you can relax the logical properties required of equality, and this is what is done in Homotopy Type Theory (homotopytypetheory.org). Then the type of objects of any category automatically comes with a notion of equality, but that equality is simply isomorphism. Feb 24 '17 at 21:41
• "such a first-order logic, Lawvere wrote ETCS in that logic too". Mhm, the book Sets for Mathematics doesn't even deal with first-order logic ... Feb 24 '17 at 21:43