Classes, sets and Russell's paradox

There are lots of ways to paint the fine details, but the broad stroke is:

• A set can be a member of a class
• A proper class cannot be a member of a class

When you use class-builder notation, such as in $\{ x \mid x \notin x \}$, the notation is only meaningful when $x$ quantifies over sets (or some subclass thereof).

In order to speak of collections of classes, you would need to appeal to some higher object, which we might call a 2-class. And to speak of collections of 2-classes, you'd need a 3-class, and so forth.

For example, one way to make this all precise is by higher order logic. As applied to ZFC, sets would be the elements of the theory, classes would be (first-order) predicates on sets, 2-classes would be second order predicates, and so forth.

In ZF set theory, a set is an element of a model of ZF, which is a collection of things together with a relation called $\in$ between them satisfying the ZF axioms. Classes are not directly discussed by the axioms but one can describe classes as first-order formulas describing a property a set may have. For example, the property corresponding to the class in Russell's paradox is $x \not \in x$, and the property corresponding to the class of all sets is $\top$ (true).

Given such a first-order property one can ask whether there exists a set $S$ such that $x \in S$ if and only if $x$ has that property. The answer is sometimes yes and sometimes no; for both of the properties above it is no in ZF because of the axiom of regularity. And since the first-order formulas describing properties of sets can only refer to sets and not to classes, it is not possible to run the same argument directly for classes in ZF; that is, there is no way of talking directly about classes internal to ZF.

In a system like MK (Morse-Kelley) set theory where there are two sorts, intended to be one for sets and one for classes in general, we can indeed construct (as an object in the system) any class of the form $\{ x : Set(x) \land φ(x) \}$, where $Set$ is the predicate corresponding to the sort intended for sets. It is then possible to prove that this object is not a set, via Russell's proof. Namely in MK you would be able to prove the following sentence:

$\neg Set(\{ x : Set(x) \land x \notin x \})$.

Note that there is little point in having the predicate $Class$ corresponding to the sort intended for classes, because in MK we have essentially that $\forall x\ ( Class(x) )$.

In practice when working in MK we say "$x$ is a set" to mean "$Set(x)$" and "$x$ is a class" to mean "$Class(x)$", which we just mentioned is totally redundant since everything is a class in MK. Well why do people still say it then? It is because most mathematical work actually is based on some informal type theory (see this article by De Bruijn and this book), and so we think of each object actually as having a type, rather than being a set or class!

Now if you want to work in ZFC completely, then you cannot even talk about classes in the same way, since they are not even objects in the system. In ZFC, we can only define classes in the limited sense that we can define new predicate-symbols, if our system supports definitorial expansion. So the Russell class does not exist as an object in the system, but we can define the predicate-symbol $Russell$ as follows:

Let $Russell$ be a $1$-place predicate such that $\forall x\ ( Russell(x) \equiv x \notin x )$.

Being a predicate-symbol rather than a collection, it makes no sense to ask whether $Russell$ is a member of itself. Likewise, in ZFC "$x \in S$" when $S$ is a class should be considered as syntactic sugar for "$S(x)$". That is the precise sense in which we can handle classes in pure ZFC. Similarly, using definitorial expansion we can handle class-functions, because defining them amounts to defining new function-symbols. For example in ZFC the power-set function-symbol "$\mathcal{P}$" is not a function but a class-function.