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:
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).