ZFC with class terms: is any set also a class?

In ZFC with class terms a class is merely a unary predicate $\varphi$ of the language which we then write as

$$\{X\mid\varphi(X)\}$$

which only suggests that we have built a collection out of these objects. We write $Y\in\{X\mid \varphi(X)\}$ for $\varphi(Y)$. Further we say that such a class (term) $\mathcal C$ is a set if

$$\exists X\forall Y[Y\in X\leftrightarrow Y\in\mathcal C].$$

In NBG and similar set theories (which build on classes instead of sets) every set is also a class. But is this true for this ZFC approach? For me it seems that a class is just a formula. And there are sets that I cannot fully describe using such a formula, e.g. a set given to me by the axiom of choice.

Are sets and classes in ZFC (with class terms) just different concept, each one not a "sub-concept" of the other?

I do not feel very well when writing $\{X\mid X\in A\}$ for arbitrary sets $A$ because for me $A$ is not a symbol of the language. However, when my set $A$ is definable by a predicate $\varphi$ with

$$\mathrm{ZFC}\vdash \exists A \varphi(A) \quad\text{ and }\quad \mathrm{ZFC}\vdash\varphi(A)\wedge \varphi(B)\to A=B,$$

then I could write $\{X\mid \forall A[\varphi(A)\to X\in A]\}$, and this would feel okay. But my problem are the sets for which there is no such $\varphi$. I do not know how I can include such an abbreviating notion (like $\{X\mid X\in A\}$) into a formal proof without feeling not quite sure what I am actually doing.

• As written, you are correct -- but usually in this formulation, the formula $\phi$ is allowed to have a parameter $A$; that is, you can actually, for each set $A$, form the class $\{X \mid \phi(X,A)\}$, and then $Y \in \{X \mid \phi(X,A)\}$ becomes a shorthand for $\phi(Y,A)$. In that case it is easy to show that every set is also a class: for a set $A$, you take the formula $\phi(X,A)$ to be $X \in A$. May 17, 2017 at 9:33
• Correct; in $\mathsf {ZFC}$ "domain" there is only one kind of objext: sets. The language of the theory uses formulas and we call a certain type of them "class-formula". May 17, 2017 at 9:37
• @Mees Doesn't this give me more of a "dependent class" $\mathcal C(A)$? I understand this approach in axioms like the axiom of specialization, where one quantifies universally over such $A$'s. But here, I have problems to see how $\varphi$ is still a valid formula of the language if I fix a set in there which is something more associated with the interpretation than the syntax. May 17, 2017 at 9:40
• May 17, 2017 at 9:43
• @Mauron What certain type exactly? Unary predicates? May 17, 2017 at 9:44

Yes. Sets are always classes in $\sf ZF$.

The reason is that while we often like to omit the parameters from our formulas, they can still be used when talking about classes. For example, "all the ordinals above $\kappa$" is a class definable with a parameter: $\kappa$.

Equally, a set $A$ is exactly the class $\{x\mid x\in A\}$.

Caveat lector: if we are talking about non-transitive models, then from the outside there is a difference between $x$ and $\{y\mid M\models y\in x\}$, but we can make this identification between sets and class so they are considered to be the same.

• I do not feel very well when writing $\{x\mid x\in A\}$ because for me $A$ is not a symbol of the language. However, when my set $A$ is definable by a predicate $\varphi$ like $\mathrm{ZFC}\vdash \exists A \varphi(A)$ and $\mathrm{ZFC}\vdash\varphi(A)\wedge \varphi(B)\to A=B$, then I could write $\{x\mid \forall A[\varphi(A)\to x\in A]\}$, and this would feel ok. But my problem are the sets for which there is not such a $\varphi$. I do not know how I can include such an abbreviating notion into a formal proof without feeling not quite sure what I am doing. May 17, 2017 at 10:30
• But you do feel right writing $\{\alpha<\kappa\mid\operatorname{cf}(\alpha)=\lambda\}$ where $\kappa$ and $\lambda$ are two completely arbitrary ordinals? I get why this bothers you, because $x\in A$ is a very simple formula. But this is about semantics, especially if you think about proper classes as collections of a universe. If you want to think about this purely syntactic, then you don't have access to "most things", and then you can take $A$ as a free variable, and prove that $x\in A$ if and only if $x\in A$ to get the same thing, so $\forall A(x\in A\leftrightarrow x\in A)$ is provable May 17, 2017 at 10:53
• Actually I do not feel well using this either (when being very formal of course). But, I could write $\forall \kappa,\lambda[\kappa,\lambda\in\mathrm{Ord}\to\exists X[X=\{\alpha<\kappa\mid\mathrm{cf}(\alpha)=\lambda\}]]$ or something like this. Maybe I am just to unexperienced and maybe too careful because I do not want to lose the sight on how to translate my proof into an absolutely formal version if necessary. Every non-formal notation should be translatable one-to-one until the proof is completely formal. And I have no clue how to do this for something like $\{x\mid x\in A\}$. May 17, 2017 at 11:30
• But you are not defining a class. You are writing a closed sentence. May 17, 2017 at 12:00
• You can think about classes as "functions" from parameters to collections of objects in the universe using the "parameters assignment" function. Yes. May 17, 2017 at 12:30