Proof of the Class Existence Theorem in NBG

139 Views Asked by At

I'm trying to follow the proof of the NBG Class Existence Theorem:

Let $\phi(x_1,x_2,...,x_n)$ be a primitive formula. Then $\exists A(\langle x_1,x_2,...,x_n\rangle\in A\leftrightarrow \phi(x_1,x_2,...,x_n))$.

I'm reading through Gödel's proof in his The Consistency of the Axiom of Choice and of the Generalized Continuum-Hypothesis and the similar proof here (Wikipedia).

My question is with what the Wikipedia proof calls the "Expansion Lemma" which states that for any relation $R(x_i,x_j)$ if there is a class $P\supseteq\{\langle x_i,x_j\rangle\ |\ R(x_i,x_j)\}$, then the class $Q=\{\langle x_1,...,x_n\rangle\ |\ R(x_i,x_j)\}$ also exists. The proof of this lemma is an algorithm that uses the axioms to prove the existence of a $P_3\supseteq\{\langle x_1,...,x_n\rangle\ |\ R(x_i,x_j)\}$ and then says that $Q=P_3\cap V^n$. But won't this just take all $n$-tuples of $P_3$? How does this get rid of $n$-tuples that don't satisfy $R$? As an example, if $P=V^2$, then surely $P\supseteq\{\langle x_i,x_j\rangle\ |\ R(x_i,x_j)\}$ for any $R$. But then won't this algorithm generate $Q=\{\langle x_1,...,x_n\rangle\ |\ \langle x_i,x_j\rangle\in V^2\}$, not $\{\langle x_1,...,x_n\rangle\ |\ R(x_i,x_j)\}$.

Gödel's proof does something similar, I think it's his theorem 2.41 or 2.6 but I'm not familiar with his logical notation (he doesn't use $\subseteq$?). Any help would be appreciated!