# First-order logic and NBG

I know that NBG set theory can be viewed as an interpretation of the first-order logic with equality. However, I do not really understand how do I get this interpretation.

As I see it: I call variables "classes" and add the class membership relation $\in$. I call a class $x$ a "set" if $\exists y \ (x \in y)$.

But what do I do with constants? Also, there is an empty set and the universal class, and I do not know how to represent them in the form $\emptyset = \dots$ and $V = \dots$

The language of NBG has a single binary relation, "$\in$," and no constants or functions. So there's no need to interpret those (any more than we would demand that a ring understand what "$<$" means, say). As to $\emptyset$ and $V$, those aren't constant symbols, but rather definable elements - e.g. NBG proves that there is a unique $x$ satisfying $\forall y(y\not\in x)$, and a unique $z$ satisfying $\forall w(\exists u(w\in u)\implies w\in z)$. We refer to these as "$\emptyset$" and "$V$," but this is done outside the formal language.
• Thank you! But I have two more questions: 1. If $\varphi(A_1, ..., A_n, x)$ is a formula, then we have the following axiom $$(\forall A_1)\dots(\forall A_n)(\exists B)(\forall x)[x \in B \Leftrightarrow \varphi(A_1,... A_n, x)]$$ But what do we mean when we write $S = \{x : \varphi(A_1,... A_n, x)\}$? One of those classes $B$? 2. What do we mean by saying that we fix some class? Oct 31, 2016 at 15:13
• @user379994 Re: your first question - actually, you can prove that there is exactly one $B$ with that property (remember that the only elements of classes are sets, and we have Extensionality). So there's no choice between "one of those" classes that needs to be made. Re: your second question, I'm not sure - where are you seeing this? Oct 31, 2016 at 15:16
• @GeorgyDunaev While there is no symbol for the emptyset in the language of ZFC, it is still "safe to use": adding symbols for defined entities isn't going to change what theorems you can prove (see e.g. "expansion by definitions"). Precisely, suppose $T$ is a theory in the language $\Sigma$ and $\varphi(x)$ is a formula in $\Sigma$ such that $T\vdash\exists x\varphi(x)$. Then let $T'=T\cup\{\varphi(c)\}$ in the expanded language $\Sigma\sqcup\{c\}$; we can show that $T'$ is conservative over $T$, that is, that for all $\Sigma$-sentences $\psi$, $T'$ proves $\psi$ iff $T$ proves $\psi$. Mar 20, 2017 at 5:59
• In fact, this is true in a very strong way: any model $M$ of $T$ can be expanded to a model $M'$ of $T'$. So for example, ZFC proves "$\exists x(\forall y(y\not\in x))$", that is, "There is an empty set." We can add a symbol "$\emptyset$" to our language to denote such a set, and add to ZFC an axiom "$\forall y(y\not\in\emptyset)$" describing its behavior; the resulting theory ZFC' will prove example the same sentences in the language of set theory as ZFC. So while definable elements need not have symbols in the original language, such symbols can always be added in a benign way. Mar 20, 2017 at 6:03
• (And, in fact, we can give an easy if tedious procedure for converting any proof from $T'$ (of a sentence in the original language $\Sigma$) to a proof from $T$, and verify the correctness of this procedure in an extremely weak theory; so this is all as constructive as could be wanted.) Mar 20, 2017 at 6:05