フォン・ノイマン＝ベルナイス＝ゲーデル集合論
ゆえに、 NBG はより表現的であるものの、 ZFC と無矛盾性同値なのである。この結果とフォン・ノイマンの1929年の相対的無矛盾性の証明を合わせると、彼の1925年の公理系にサイズ制限公理を加えたものが ZFC と無矛盾性同値であることが含意される。ZFCはカントール集合論のフレームワークに含まれるため、この事実は完全にこの強力な公理の相対的無矛盾性に関するフォン・ノイマンの懸念を払拭するものである。
NBG は ZFC の保存拡大であるものの、定理は NBG のほうが ZFC より短くエレガントに証明可能である(逆もしかり)。この側面について知られている結果の調査結果は Pudlák 1998 を参照。
モース=ケリー集合論は、量化子の範囲がクラスである論理式を含む理解の公理型を有する。MK は NBG の無矛盾性を証明できるため、 NBG より強力な理論である一方、ゲーデルの第二不完全定理から NBG は NBG自身の無矛盾性を証明できない。
NBG に関する存在論的な議論や哲学的な問題、特に ZFC と MK との比較については、Potter 2004の Appendix C を参照。
帰納的証明で論理式 ( x 1 , t ) ∈ F ∧ ( t , x 2 ) ∈ G {\displaystyle (x_{1},t)\in F\land (t,x_{2})\in G} をなす ∃ t {\displaystyle \exists t} が取り除かれる。しかし、クラス存在定理は添字つき変数を使って表されているため、この論理式は帰納法における仮定として期待される形式にならない。この問題は変数 t {\displaystyle t} を x 3 {\displaystyle x_{3}} で置き換えることで解決できる。ネストされた量化子内の束縛変数を扱うには、量化子ごとに添字の数字を 1 ずつ増やしていけば良い。これによって規則 4 が導出される。規則 1 と 2 で量化された変数が増えるため、規則 4 はほかの規則よりもあとに適用しなければならない。
論理式に x 1 , ... , x n {\displaystyle x_{1},\dots ,x_{n}} 以外の自由変数が含まれなければ、 q {\displaystyle q} 個の量化子内にネストされた束縛変数を x n + q {\displaystyle x_{n+q}} に置き換える。これらの変数は (量化子)ネスト深さ q {\displaystyle q} である。
クラス存在定理の証明. 証明は与えられた論理式に変換規則を適用して、論理式を変換することから始める。
1931年、ベルナイスは自身の集合論に関してクルト・ゲーデルに手紙を送った。ゲーデルはベルナイスの理論を、集合をすべてクラスで置き換え、1ソートで1つの原始概念(帰属関係)からなる理論に簡略化した。ゲーデルはまた、ベルナイスの公理のいくつかを弱め、フォン・ノイマンの選択公理を大域選択公理と等価なものに置き換えた。 ゲーデルは、1940年の大域選択と一般連続体仮説の相対的無矛盾性に関するモノグラフの中で、自身の公理系を使った。
ゲーデルが自身のモノグラフの中で NBG を用いた理由はいくつか考えられる:
ゲーデルは数学的理由を与えた—NBGの大域選択公理から、より強い無矛盾な定理が導かれる:「この強い形式の(選択)公理は、他の公理に対して無矛盾であれば、当然弱い形式についての無矛盾性を含意する。」
ロバート・ソロヴェイ(英語版)は以下のように予想した:「私が思うに、彼(ゲーデル)は公理的集合論内でモデル理論の基本を発展させることに関連する、細部の議論を避けたかった。」
ケネス・キューネンはゲーデルが議論を避けた理由を以下のように考えている:「L (構成可能集合)に関する組み合わせ論的アプローチもたくさんある、例えば .
∀ x φ ( x ) {\displaystyle \forall x\,\phi (x)} 、 ∀ x ( ∃ C ( x ∈ C ) ⟹ φ ( x ) ) {\displaystyle \forall x{\bigl (}\exists C(x\in C)\implies \phi (x){\bigr )}} の代わりに。
以下の公理と定義はクラス存在定理の証明に必要である。
外延性の公理. 2 つのクラスが同じ元を持っていれば、それらは等しい。
∀ A ∀ B [ ∀ x ( x ∈ A ⟺ x ∈ B ) ⟹ A = B ] {\displaystyle \forall A\,\forall B\,[\forall x(x\in A\iff x\in B)\implies A=B]}
この公理はZFCの外延性の公理をクラスに一般化したものである。
対の公理. x {\displaystyle x} と y {\displaystyle y} が集合であれば、元が x {\displaystyle x} と y {\displaystyle y} のみである集合 p {\displaystyle p} が存在する。