So, NBG can not prove that first order set theory has a satisfication class. However, it is consistent with NBG that such a class exists. My question is if it is consistent with NBG that two such classes exist.

We will use $\in, =, \lor, \exists, \lnot,$ as the main symbols in our language for first order set theory. We say that a class $S$ is a satisfaction class if $(s,v) \in S$ iff $s$ is a formula, $v$ is a function from variables to sets, and one of the following is true (for some variables $x$ and $y$ and formulas $\phi, \psi$):

  • s = $x$ "$\in$" $y$ and $v(x) \in v(y)$
  • s = $x$ "$=$" y and $v(x) = v(y)$
  • s = $\phi$ "$\lor$" $\psi$ and either $(\phi, v) \in S$ or $(\psi, v) \in S$
  • s = "$\exists$" $x$ $\phi$ and there exists some set $\chi$ such that ($\phi$, $v'$), where $v'$ is $v$ with $x$ assigned to $\chi$
  • s = "$\lnot$" $\phi$ and $(\phi, v) \notin S$

Is the statement "There exists proper classes $S$ and $S'$ such that $S$ and $S'$ are satisfaction classes and $S \neq S'$" consistent with NBG?

One thing to note is that for any statement $\phi$ we have that $(\phi, \emptyset) \in S \iff (\phi, \emptyset) \in S'$. We can prove that there is a proof of this by using induction on formula length in the meta-theory. However, I can not find anything wrong with $S$ and $S'$ disagreeing on other elements, such as ones where the variable assignment is non-empty, or where $\phi$ has a nonstandard length (assuming we are talking about a model, and that model has nonstandard naturals).


NBG can prove the following theorem by straightforward induction on the structure of $\varphi$: Suppose $S$ and $S'$ are satisfaction classes. Then for all formulas $\varphi$, we have that for all variable assignments $v$, $(\varphi,v)\in S\iff (\varphi,v)\in S'$. It follows that $S = S'$.

Edit: As Andreas Blass points out, this is not quite as straightforward as I made it sound. Let me try to spell it out more explicitly. NBG defines a set $\mathcal{F}$ of formulas in the language of set theory, together with a relation $<$ on $\mathcal{F}$, where $\varphi<\psi$ iff $\varphi$ is a proper subformula of $\psi$. NBG proves that $(\mathcal{F},<)$ is a well-founded poset, and hence can carry out induction on $(\mathcal{F},<)$: for any set $X\subseteq \mathcal{F}$, if $\psi\in X$ whenever $\varphi\in X$ for all $\varphi < \psi$, then $X = \mathcal{F}$.

Now NBG proves that for all classes $S$ and $S'$, by class comprehension using $S$ and $S'$ are parameters, we have a class $X = \{\varphi\in \mathcal{F}\mid (\forall v\, (\varphi,v)\in S\leftrightarrow (\varphi,v)\in S')\}$. Note that the comprehension condition only quantifies over sets, not classes, since a function from variables to sets is a set. Of course, $X$ is a set, since it's a subset of $\mathcal{F}$.

Finally, NBG proves that for all classes $S$ and $S'$, if $S$ and $S'$ are satisfaction classes, then $X$ satisfies the induction criterion, so $X = \mathcal{F}$. That is, $\forall \varphi\in \mathcal{F} \forall v ((\varphi,v)\in S\leftrightarrow (\varphi,v)\in S'))$, i.e. $S = S'$.

You write:

One thing to note is that for any statement $\varphi$, we have that $(\varphi,\emptyset)\in S \iff (\varphi,\emptyset)\in S'$. We can prove that there is a proof of this by using induction on formula length in the meta-theory.

For one thing, I'm not sure what induction you have in mind that will only apply to sentences with no free variables. If $\varphi$ is $\exists x\, \psi$, then in order to use the definition of $(\exists x\, \psi,\emptyset)\in S$, you're going to have to think about elements $(\psi,v)\in S$ where $v$ is nonempty!

But more importantly, there's absolutely no reason to do induction in the meta-theory here. The set of first-order formulas has an inductive structure, and NBG proves that the induction principle over the set of formulas is valid. The fact that there are models of NBG containing formulas of non-standard length is irrelevant, just like the fact that there are non-standard models of PA doesn't stop us from doing proofs by induction in PA. I think this is the crux of the confusion in your question.

Edit: One more comment. You could imagine that in some model of NBG with formulas of nonstandard length, there are two satisfaction classes $S$ and $S'$ which agree on all the formulas of standard length, but start disagreeing afterward. What the proof above shows is that in this situation, we could use $S$ and $S'$ to find a subset of $\mathcal{F}$ with no minimal element. And since NBG proves that $\mathcal{F}$ is well-founded, such a set cannot exist in any model of NBG (even in a model in which we can see externally that $\mathcal{F}$ is not well-founded).

  • $\begingroup$ Is it assumed that $S$ and $S'$ are definable without quantifying over proper classes? Or is NBG being extended by adding comprehension axioms for formulas involving (predicate symbols for ) $S$ and $S'$? Without something like that, I don't see how to do the induction. (This is similar to the fact that ordinary induction for natural numbers won't work in NBG if the statement to be proved by induction involves quantification over proper classes.) $\endgroup$ – Andreas Blass Mar 8 '19 at 16:03
  • $\begingroup$ @AndreasBlass Oh, yikes, I guess I didn't think about this carefully enough. What's an example of the kind of failure of induction of induction over $\omega$ you're referring to? $\endgroup$ – Alex Kruckman Mar 8 '19 at 16:15
  • $\begingroup$ Using quantification over proper classes, you can formulate in NBG a definition of "truth in the universe" (for formulas of ZFC). It's the same definition as in MK, since NBG and MK have the same language. But, unlike MK, NBG can't carry out the induction showing that everything provable in ZFC is true, and so NBG can't formalize the natural proof that ZFC is consistent (which is a good thing, since NBG (including set-choice) is a conservative extension of ZFC). $\endgroup$ – Andreas Blass Mar 8 '19 at 16:31
  • $\begingroup$ @AndreasBlass Ok, I think I understand the issue now. But it seems to me that the induction in my answer isn't actually quantifying over classes, just using the classes $S$ and $S'$ as parameters - and I was under the impression that this was covered by the class existence axioms in NBG. More precisely, doesn't NBG prove that for all $S$ and $S'$, there exists a class consisting of all formulas $\varphi$ such that there exists a $v$ such that $(\varphi,v)\in S\not\leftrightarrow (\varphi,v)\in S'$? If not, then there's a subtlety about class existence in NBG that I've misunderstood. $\endgroup$ – Alex Kruckman Mar 8 '19 at 16:31
  • $\begingroup$ I think you're right. If $S$ and $S'$ are classes (not just predicates), then NBG gives you the comprehension and therefore the induction that you need. $\endgroup$ – Andreas Blass Mar 8 '19 at 16:35

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.