Struggling with classes I am still struggling with the concept of classes in ZF set theory. From Jech, Set Theory, p.5:

That means: 


*

*For every formula $\varphi(x)$ there is a class (which is definable). There are countably many definable classes.

*For every formula $\varphi(x,y_1,\dots,y_n)$ and every tuple of sets $p_1,\dots,p_n$ there is a class (which is definable, when the sets $p_1,\dots,p_n$ are definable). There are "countably many times class-many", i.e. class-many such classes.
My questions are:


*

*Can the concept of "arbitrary collections" of sets be sensibly conceived that are not even classes, i.e. not given by a formula + parameters? 
(Possible answer: No, because we cannot talk about them.)

*Can the classes of NGB set theory be conceived as "arbitrary collections"?
If we consider sets (of ZF set theory) as the base type ("type 0"), there are three candidates for "type 1" as collections of sets:


*

*sets of sets (collections that are co-extensive with sets)

*classes of sets (collections that are given by a formula/property)

*arbitrary collections of sets


Have all of these "type theories" been worked out, or do some of them simply not work?
 A: I don't think it is quite right to say that there are countably many definable classes. In the context of $\mathsf{ZFC}$, countability is only defined for objects in the domain of discourse (thought of as sets.) Definable classes correspond to formulas, which are objects in an informal meta-theory.  One could try to get around this distinction somehow, but there are two problems.


*

*Although one can define a set $\text{Form}$ of elements of $V_\omega$ that code formulas, it's not generally possible to obtain a bijection between $\text{Form}$ and the collection of definable sets, nor is it even generally possible to formalize what it would mean to do so.  The naive attempt fails because of Tarski's theorem on the undefinability of truth.

*Obtaining a bijection between $\text{Form}$ and the collection of definable classes is even more problematic, because the elements of the bijection  would be sets (simply because in the $\mathsf{ZFC}$ context only sets can appear on the left side of "$\in$") but some of the classes in the desired range are proper classes.
I think it is fair to say that classes in the sense of $\mathsf{NBG}$ could be considered as "arbitrary collections" of sets, in the sense that if $\kappa$ is an inaccessible cardinal then $V_\kappa$ together with the collection of all subsets of $V_\kappa$ (that is, with $V_{\kappa+1}$) forms a model of $\mathsf{NBG}$.  However, the "intended model" of $\mathsf{NBG}$ is sometimes considered to be $V_\kappa$ together with all subsets that are first-order definable over $V_\kappa$.  The intended model of Morse–Kelley set theory is $V_\kappa$ together with all subsets of $V_\kappa$, so perhaps it is a better candidate for your purposes.
I don't know the answer to your last question about type theories.
