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



"classes" with no cardinality; "classes" with no equality notion
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*.


