"classes" with no cardinality; "classes" with no equality notion

Question

Hello,

If we look at the class of all vector spaces over some field, we can note two things:

1) this class should not have cardinality.

2) for two elements of this class, we should not want to be able to verify whether they are equal

But we can have some situations which have only one of the two features. For example:

• Look at "beasts" which assign to every vector space a morphism from it to its dual. Then the class of all such beasts should not have cardinality, but we can say whether two such beasts are equal or not.

My question is rather vague: Does (axiomatic) set theory think about the difference between these two features 1) and 2) ? Or, can someone share his way of thinking about the two features and their relation?

Edit: I apologize for being not very precise. In (2), I am talking from a (biased?) categorical point of view; there should be no meaning for two vector spaces to be equal; they can be known to be isomorphic, or given a specific isomorphism, but not equal (if we can or can not ask in a specific axiomatic system whether two vector spaces are equal does not really make a difference). In (*), we can verify whether two beasts are equal just by checking, for every vector space, whether the morphisms from it to its dual provided by the two beasts are equal or not. In a comment it was told the collection of beasts does have a cardinality; Anyway, it was just an example. I would think of them as not having cardinality (probably one might provide some example in the same spirit for which there is no cardinality?), or would not care about their cardinality, just to stress the point.

Thank you, Sasha

Answer 1

Classical axiomatic set theories (eg ZFC, NGB) are formulated in first-order logic with equality, so any things you can quantify over (i.e. that you can talk about as actual objects of the language), you can talk about equality of, as a basic given of the language.

In particular, in either ZFC or NGB, you can certainly talk about equality of vector spaces. In ZFC, you can’t talk about beasts as quantify-over-able objects (since they can only be represented as proper classes, not as sets); in NGB, you can, and so you get equality of them.

Cardinality is a bit slipperier: it’s generally considered as a defined rather than a basic notion, and the exact definitions used vary in ways your question will be sensitive to. Most often, an object called the “cardinality” is only specifically defined for sets^[1]; for classes, “C and D have the same cardinality” is considered syntactic sugar for “there is a class-bijection between C and D”. So it’s not quite clear what it means to ask if a class “has cardinality”, but whatever it is depends heavily on having an equality relation on it, to be able to talk about bijections to/from it.

---

On the other hand, there are some more recent set/type theories in which equality isn’t given, or is a more flexible notion.

In some versions of the Calculus of Constructions, if I remember right, there is a universe of small sets (possibly multiple universes), and an arbitrary product of sets is again a set, possibly in some higher universe (this has to be formulated carefully to avoid inconsistency); and each set has equality on it, but there’s no equality on the universe(s). So there, vector spaces wouldn’t form a set, and wouldn’t have an equality relation; but beasts would form a set (a certain product of hom-sets) so would have an equality relation. (The C of C’s is a little out of what I know, so this may need correcting by someone more knowledgeable.)

Similarly, there are versions of Martin-Löf Type Theory with identity types which address this issue; roughly, identity types can represent something like an ordinary equality relation, but more generally they can also look like the sets/categories of (weak) ismorphisms in a (higher) category. So you can define an object to be 0-categorical^[1] if all its identity types are just truth-values; then an arbitrary product of 0-categorical types is again 0-categorical.

In this setup, the type of all vector spaces within some universe will have identity types, so equality of a sort, but not of the objectionable kind — “equality” of vector spaces will exactly be isomorphism between them. The type of beasts over this universe will now be 0-categorical: we will have equality of beasts in the simplest sense. (Also, in this foundation, all beasts will automatically respect isomorphism!)

---

[1]: The two main definitions of $\|X\|$ I know are “the least ordinal bijective to $X$” (elegant, but requires choice to be defined for all $X$), or “$\{ Y \in V_\alpha\ |\ Y \cong X \}$, where $\alpha$ is minimal such that this is non-empty” (less transparent but more robust).

[2]: I first heard this definition from Voevodsky, though I’m pretty sure it had been considered by others before as well. He calls this property being a set, but I want to make unambiguous that it’s a restriction of categorical dimension not of size.

Answer 2

Peter's answer is very good, I just wanted to add a little bit. Namely, in addition to "classical" axiomatic set theories such as ZFC and NBG, and type theories such as CoC and MLTT, there is a third foundational option which one may call "structural" or "categori(c)al" set theory. The first such theory was Lawvere's ETCS; more recently I wrote up a slight variant which I think "looks more set-theoretic" called SEAR.

These theories are similar to classical set theories in some ways and to type theories in other ways. On the one hand, SEARC (SEAR with choice) is completely equivalent to ZFC, in that not only does a model of either one give rise to a model of the other, but one from which the original model can be reconstructed up to equivalence. On the other hand, like type theory, SEAR does not, and ETCS can be formulated so as to not, include a notion of equality for sets (only for functions between sets or elements of a fixed set). So in these foundations, the "class" of vector spaces has no equality, and I don't think there is much of a way to give sense to it having a cardinality.