Every (proper) class in ZFC is a set if we "objectify" the metalanguage, and is "class" a metalanguage notion?

In ZFC set theory, what is called a class is a notion of the metalanguage, not the object language, right? (the collection defined by some formula)

And if so, if we talk about axiomatic set theory, and formalize exactly this reasoning, then do we have to introduce sets on this metalanguage level and its formalization (using ZFC again) what where classes before, are now sets.

So by this process of formalising the metalanguage and making it the object language of the next "layer" we get an infinite of models of (ZFC-) set theory, where even the proper classes become sets in "the new viewpoint".

But does this make any sense? By this process every model is enlarged, so there is no "largest" one.

• If $U$ is a model of ZF, then "from.our point of view", $U$ is a set (by definition of model), however, in the eyes of $U$,$U$ is a proper class. That is, $\forall x\in U, x\in U$ (trivial) and $U\models \neg \exists z, \forall x,x\in z$ (classical theorem of ZF) Jul 13 '17 at 21:51
• I might have misunderstood your question to some degree. I'm not sure. It's a bit late. Do let me know... Jul 13 '17 at 22:01
• @Max you mean $\neg \exists x \forall y : y \in x$, or? Jul 14 '17 at 11:11
• @Asaf Karagila Yes, your answer is good. But one last point: Isn't it somewhat circular if we use set theory to formalize set theory, i.e. in ZFC we have classes which are sets in your metalanguage which seems somehow circular to me, so we define something by using it, which is problematic, or not? Jul 14 '17 at 11:14
• Sure. You can use arithmetic to formalize set theory. Then classes are not really objects, as much as they are just formulas. But then you can ask, how do we formalize arithmetic? Jul 14 '17 at 11:17

Yes, this is essentially the way we move from first-order $\sf ZFC$ to its conservative second-order extension $\sf NBG$.
Given a model $(M,E)$ of $\sf ZFC$, we can look at $(M,E,\mathcal C)$ where $\mathcal C$ is all the definable classes of $M$, as a model of $\sf NBG$. This can be extended in some cases, by taking even more classes and getting a model of $\sf KM$ (Kelley–Morse set theory), although this theory is stronger in consistency and so the extension is no longer conservative.
Repeating this process will inevitably give you something akin to a simple type theory. You will have objects, sets; then classes, which are collections of sets; $2$-classes which will be collections of classes; then $n$-classes, which will be collections of $2$-classes; and so on. In theory, you can proceed through all the ordinals, but this is not particularly useful. Going through $\omega$ is generally enough for most of what you might want to do, or at most going through the recursive ordinals in order to preserve some semblance of recursive enumeration of your language and theory.
What you may want to do first, however, is understand what exactly are the properties and interactions you expect your $n$-classes to have with themselves, and other $m$-classes.