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.

Has someone thought about this? Or does it make no sense what I am talking about (making classes sets again...)?

  • $\begingroup$ 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) $\endgroup$ Jul 13 '17 at 21:51
  • $\begingroup$ I might have misunderstood your question to some degree. I'm not sure. It's a bit late. Do let me know... $\endgroup$
    – Asaf Karagila
    Jul 13 '17 at 22:01
  • $\begingroup$ @Max you mean $\neg \exists x \forall y : y \in x$, or? $\endgroup$
    – StefanH
    Jul 14 '17 at 11:11
  • $\begingroup$ @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? $\endgroup$
    – StefanH
    Jul 14 '17 at 11:14
  • $\begingroup$ 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? $\endgroup$
    – Asaf Karagila
    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.

If you want your classes to also satisfy some basic set theoretic properties, like "power class", for example, and Replacement, then you're not too far off the Tarski–Grothendieck set theory augmented by the axiom "Every set is an element of a universe".


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.