フォン・ノイマン＝ベルナイス＝ゲーデル集合論
ゲーデルは、クラス存在定理は「メタ定理(英語版)である。すなわち、システム(NBG)に関する定理であり、システム内の定理でではない...」と指摘した。 NBG 論理式の帰納によるメタ理論の中で証明されるため、クラス存在定理は NBG に関する定理である。また、その証明は、有限個の NBG 公理を持ち出す代わりに、与えられた論理式を満たすクラスを構築するためのNBG 公理の使い方を帰納的に表現する。すべての論理式に対して、こうした表現は NBG 内の存在の構成的証明に変えられる。したがって、このメタ理論で NBG のクラス存在定理の使い方を置き換えた NBG の証明を作ることができる。
再帰的なコンピュータプログラムで、与えられた論理式からクラスを簡単に構成することができる。このプログラムの定義はクラス存在定理の証明によらない。しかし、プログラムによって構成されるクラスが与えられた論理式を満たし、公理から構成されたかを確認するには、定理の証明が必要である。このプログラムのPascal形式のcase文を用いた擬似コードを以下に示す。
φ {\displaystyle \phi } を 例 2 の論理式とする。関数呼び出し A = C l a s s ( φ , 1 ) {\displaystyle A=Class(\phi ,1)} でクラス A {\displaystyle A} を作成するが、以下で φ {\displaystyle \phi } と比較する。クラス A {\displaystyle A} の構成は、それを定義する論理式 φ {\displaystyle \phi } の構成を反転することがわかる。
たとえば、帰属公理から、クラス E {\displaystyle E} が順序対ではない元を含むが、共通部分 E ∩ V 2 {\displaystyle E\cap V^{2}} は E {\displaystyle E} の順序対のみからなるようにクラス E {\displaystyle E} を構成できる。
巡回置換公理と転置公理はクラス B {\displaystyle B} の 3-組であることのみを規定するため、ただ一つのクラスの存在を含意しない。 3-組を規定することで、これらの公理は n ≥ 4 {\displaystyle n\geq 4} に対して n {\displaystyle n} -組についても規定する。なぜならば:
対に関する公理と領域公理は以下の補題を含意する。この補題はクラス存在定理の証明に用いる。
組の補題 ―
∀ A ∃ B 1 ∀ x ∀ y ∀ z [ ( z , x , y ) ∈ B 1 ⟺ ( x , y ) ∈ A ] {\displaystyle \forall A\,\exists B_{1}\,\forall x\,\forall y\,\forall z\,[(z,x,y)\in B_{1}\iff (x,y)\in A]}
∀ A ∃ B 2 ∀ x ∀ y ∀ z [ ( x , z , y ) ∈ B 2 ⟺ ( x , y ) ∈ A ] {\displaystyle \forall A\,\exists B_{2}\,\forall x\,\forall y\,\forall z\,[(x,z,y)\in B_{2}\iff (x,y)\in A]}
ZFCの言葉にクラスが加えられれば、ZFCをクラス付きの集合論に変換するのが容易になる。まず、クラス解釈の公理型を加える。この公理型は以下の通り:量化子の範囲を集合に限定したすべての論理式 φ ( x 1 , ... , x n ) {\displaystyle \phi (x_{1},\ldots ,x_{n})} に対して、論理式を満たす n {\displaystyle n} -組からなるクラス A {\displaystyle A} が存在する—すなわち、 ∀ x 1 ⋯ ∀ x n [ ( x 1 , ... , x n ) ∈ A ⟺ φ ( x 1 , ... , x n ) ] {\displaystyle \forall x_{1}\cdots \,\forall x_{n}[(x_{1},\ldots ,x_{n})\in A\iff \phi (x_{1},\ldots ,x_{n})]} である。
この定理の証明は 2 ステップからなる:
与えられた論理式 φ {\displaystyle \phi } を証明の帰納部分を簡略化する等価な(英語版)論理式に変換するため、変換規則を用いる。例えば、帰納部分で 3 ケースの論理記号のみを扱うため、変換後の論理式に用いる論理記号は ¬ {\displaystyle \neg } , ∧ {\displaystyle \land } , ∃ {\displaystyle \exists } のみとする。
変換後の論理式に対して、クラス存在定理を帰納的に証明する。変換後の論理式の構造を用い、クラス存在公理から論理式を満たす唯一の n {\displaystyle n} -組を構成する。
変換規則. 以下の規則 1 と 2 において、 Δ {\displaystyle \Delta } と Γ {\displaystyle \Gamma } はそれぞれ集合とクラスの変数を表す。これらの 2 つの規則で ∈ {\displaystyle \in } の前のすべてのクラス変数とすべての等号を除去する。規則 1 や 2 をサブ論理式に適用する際は、 z i {\displaystyle z_{i}} が論理式中の他の変数と異なるように i {\displaystyle i} を選ぶ。3 つの規則はサブ論理式に適用できなくなるまで適用を繰り返す。これによって、 ¬ {\displaystyle \neg } , ∧ {\displaystyle \land } , ∃ {\displaystyle \exists } , ∈ {\displaystyle \in } 、 集合変数、 ∈ {\displaystyle \in } の前に現れないクラス変数 Y k {\displaystyle Y_{k}} 論理式のみからなる論理式を構成する。
, x n , Y → ) {\displaystyle \phi (x_{1},\ldots ,x_{n},{\vec {Y}})=\neg \psi (x_{1},\ldots ,x_{n},{\vec {Y}})} のとき、 ψ {\displaystyle \psi } は k − 1 {\displaystyle k-1} 個の論理記号を含むため、帰納仮説は以下を満たす n {\displaystyle n} -組のクラス A {\displaystyle A} がただ一つ存在することを含意する:
補修号の公理より、 ∀ u [ u ∈ ∁ A ⟺ ¬ ( u ∈ A ) ] {\displaystyle \forall u\,[u\in \complement A\iff \neg (u\in A)]} となるクラス ∁ A {\displaystyle \complement A} が存在する。しかし、 ∁ A {\displaystyle \complement A} は n > 1 {\displaystyle n>1} のとき n {\displaystyle n} -組以外の元を含む。 ∁ V n A = {\displaystyle \complement _{V^{n}}A=\,} ∁ A ∩ V n = {\displaystyle \complement A\cap V^{n}=\,} V n ∖ A {\displaystyle V^{n}\setminus A} を用いて、この元を消去する。これはすべての n {\displaystyle n} -組のクラス V n {\displaystyle V^{n}} の相対補集合である。すると、外延性の公理から ∁ V n A {\displaystyle \complement _{V^{n}}A} は以下を満たす n {\displaystyle n} -組の唯一のクラスである: