フォン・ノイマン＝ベルナイス＝ゲーデル集合論
NBGの公理化 > クラス存在定理

クラス存在定理 ―  \phi (x_{1},\dots ,x_{n},Y_{1},\dots ,Y_{m})を、集合を量化する論理式とする。この論理式は  x_{1},\dots ,x_{n},Y_{1},\dots ,Y_{m} 以外に自由変数をもたないものとする（必ずしも  x_{1},\dots ,x_{n},Y_{1},\dots ,Y_{m} すべてが自由変数でなくてもよい）。すると、すべての  Y_{1},\dots ,Y_{m} に対して、以下を満たす  n-組のクラス  A がただ一つ定まる：  \forall x_{1}\cdots \,\forall x_{n}[(x_{1},\dots ,x_{n})\in A\iff \phi (x_{1},\dots ,x_{n},Y_{1},\dots ,Y_{m})]. クラス  A は  \{(x_{1},\dots ,x_{n}):\phi (x_{1},\dots ,x_{n},Y_{1},\dots ,Y_{m})\} で表すことができる。
この定理の証明は 2 ステップからなる：
与えられた論理式  \phi  を証明の帰納部分を簡略化する等価な（英語版）論理式に変換するため、変換規則を用いる。例えば、帰納部分で 3 ケースの論理記号のみを扱うため、変換後の論理式に用いる論理記号は  \neg ,  \land ,  \exists  のみとする。
変換後の論理式に対して、クラス存在定理を帰納的に証明する。変換後の論理式の構造を用い、クラス存在公理から論理式を満たす唯一の  n-組を構成する。
変換規則.  以下の規則 1 と 2 において、  \Delta  と  \Gamma  はそれぞれ集合とクラスの変数を表す。これらの 2 つの規則で  \in  の前のすべてのクラス変数とすべての等号を除去する。規則 1 や 2 をサブ論理式に適用する際は、  z_{i} が論理式中の他の変数と異なるように  i を選ぶ。3 つの規則はサブ論理式に適用できなくなるまで適用を繰り返す。これによって、  \neg ,  \land ,  \exists ,  \in 、 集合変数、  \in  の前に現れないクラス変数  Y_{k}論理式のみからなる論理式を構成する。
\,Y_{k}\in \Gamma  を  \exists z_{i}(z_{i}=Y_{k}\,\land \,z_{i}\in \Gamma ) に変換する。
外延性公理を用いて、  \Delta =\Gamma  を  \forall z_{i}(z_{i}\in \Delta \iff z_{i}\in \Gamma ) に変換する。
論理的同一性を用いて、 \lor ,\implies ,\iff , and  \forall  が含まれるサブ論理式を  \neg ,\land ,\exists  のみが含まれるサブ論理式に変換する。
変換規則：束縛変数.  例 1の合成関数論理式について、集合の自由変数を  x_{1} と  x_{2} に置き換えることを考える：  \exists t[(x_{1},t)\in F\,\land \,(t,x_{2})\in G]。帰納的証明で論理式  (x_{1},t)\in F\land (t,x_{2})\in G をなす  \exists t が取り除かれる。しかし、クラス存在定理は添字つき変数を使って表されているため、この論理式は帰納法における仮定として期待される形式にならない。この問題は変数  t を  x_{3} で置き換えることで解決できる。ネストされた量化子内の束縛変数を扱うには、量化子ごとに添字の数字を 1 ずつ増やしていけば良い。これによって規則 4 が導出される。規則 1 と 2 で量化された変数が増えるため、規則 4 はほかの規則よりもあとに適用しなければならない。
論理式に  x_{1},\dots ,x_{n} 以外の自由変数が含まれなければ、  q 個の量化子内にネストされた束縛変数を  x_{n+q} に置き換える。これらの変数は (量化子)ネスト深さ  q である。
クラス存在定理の証明.  証明は与えられた論理式に変換規則を適用して、論理式を変換することから始める。この論理式は与えられた論理式と等価であるので、変換済みの論理式を証明すればクラス存在定理の証明が完了する。
変換後の論理式に対するクラス存在定理の証明 — 
以下の補題を証明の中で用いる。
拡大の補題 ―  1\leq i<j\leq n と置き、  P を、  R(x_{i},x_{j}). を満たすすべての順序対  (x_{i},x_{j}) を含むクラスとする。すなわち、  P\supseteq \{(x_{i},x_{j}):R(x_{i},x_{j})\} である。すると  P は  R(x_{i},x_{j}) を満たす  n-組の唯一のクラス  Q に拡張することができる。すなわち、  Q=\{(x_{1},\ldots ,x_{n}):R(x_{i},x_{j})\} である。
証明：
i=1 のとき、  P_{1}=P とする。 i>1のとき、 x_{i}の前に成分が追加される：組の補題の言明 1 を  P with  z=(x_{1},\dots ,x_{i-1}) に適用する。この操作により、 R(x_{i},x_{j}) を満たすすべての  (i+1)-組  ((x_{1},\dots ,x_{i-1}),x_{i},x_{j})=(x_{1},\dots ,x_{i-1},x_{i},x_{j}) を含むクラス  P_{1} が生成される。
j=i+1 のとき、  P_{2}=P_{1} とする。 j>i+1 のとき、 x_{i} と  x_{j} の間に成分が追加される：組の補題の言明 2 を用いて  x_{i+1},\dots ,x_{j-1} を一つずつ追加する。この操作により、 R(x_{i},x_{j}). を満たすすべての  j-組  (((\cdots ((x_{1},\dots ,x_{i}),x_{i+1}),\cdots ),x_{j-1}),x_{j})=(x_{1},\dots ,x_{j}) を含むクラス  P_{2} が生成される。
j=n のとき、  P_{3}=P_{2}とする。  j<n のとき、 x_{j}のあとに成分が追加される：組の補題の言明 3 を用いて  x_{j+1},\dots ,x_{n} を一つずつ追加する。この操作により、  R(x_{i},x_{j}). を満たすすべての  n-組  ((\cdots ((x_{1},\dots ,x_{j}),x_{j+1}),\cdots ),x_{n})=(x_{1},\dots ,x_{n}) を含むクラス  P_{3} が生成される。
Q=P_{3}\cap V^{n} とする。外延性の公理から、  Q が  R(x_{i},x_{j}). を満たす  n-組の唯一のクラスであることが導かれる。
変換後の論理式に対するクラス存在定理 ―  \phi (x_{1},\ldots ,x_{n},Y_{1},\ldots ,Y_{m}) を、以下を満たす論理式とする：
x_{1},\ldots ,x_{n},Y_{1},\ldots ,Y_{m} 以外に自由変数を持たない。
\in 、  \neg 、  \land 、  \exists 、 集合変数、クラス変数  Y_{k} のみからなる。ここで  Y_{k} は  \in  より前には現れない。
集合変数  x_{n+q} のみを量化する。ここで  q は変数の、量化子ネスト深さを表す。
すると、すべての  Y_{1},\dots ,Y_{m} に対して、以下を満たす  n-組のクラス  A がただ一つ存在する：
 \forall x_{1}\cdots \,\forall x_{n}[(x_{1},\ldots ,x_{n})\in A\iff \phi (x_{1},\ldots ,x_{n},Y_{1},\ldots ,Y_{m})].
証明：基礎ステップ： \phi  は論理記号を含まない。定理の仮説は  \phi  が  x_{i}\in x_{j} または  x_{i}\in Y_{k} の形の原子論理式であることを含意する。
Case 1:  \phi  が  x_{i}\in x_{j} のとき、 x_{i}\in x_{j}. を満たす  n-組の唯一のクラス  E_{i,j,n}=\{(x_{1},\ldots ,x_{n}):x_{i}\in x_{j}\} を構成する。
Case a:  \phi  が  x_{i}\in x_{j}（ i<j）のとき、帰属の公理より、  x_{i}\in x_{j} を満たすすべての順序対  (x_{i},x_{j}) を含むクラス  P を生成する。拡張の補題を  P に適用することで、  E_{i,j,n}=\{(x_{1},\ldots ,x_{n}):x_{i}\in x_{j}\} を得る。
Case b:  \phi  が  x_{i}\in x_{j}（ i>j）のとき、帰属の公理より、  x_{i}\in x_{j} を満たすすべての順序対  (x_{i},x_{j}) を含むクラス  P を生成する。組の補題の言明 4 を  P に適用することで、  x_{i}\in x_{j} を満たすすべての順序対  (x_{j},x_{i}) を含むクラス  P' を生成する。拡大の公理を  P' に適用することで、  E_{i,j,n}=\{(x_{1},\ldots ,x_{n}):x_{i}\in x_{j}\} を得る。
Case c:  \phi  が  x_{i}\in x_{j} （ i=j）のとき、正則性の公理よりこの論理式は偽であるため、これを満たす  n-組は存在せず、ゆえに  E_{i,j,n}=\emptyset  である。
Case 2:  \phi  が  x_{i}\in Y_{k} のとき、  x_{i}\in Y_{k}. を満たす  n-組の唯一のクラス  E_{i,Y_{k},n}=\{(x_{1},\ldots ,x_{n}):x_{i}\in Y_{k}\} を構成する。
Case a:  \phi  が  x_{i}\in Y_{k}（ i<n）のとき、  V の直積公理を  Y_{k} に適用してクラス  P=Y_{k}\times V=\{(x_{i},x_{i+1}):x_{i}\in Y_{k}\} を得る。拡大の補題を  P に適用して  E_{i,Y_{k},n}=\{(x_{1},\ldots ,x_{n}):x_{i}\in Y_{k}\} を得る。
Case b:  \phi  が  x_{i}\in Y_{k}（ i=n>1）のとき、  V の直積公理を  Y_{k} に適用してクラス  P=Y_{k}\times V=\{(x_{i},x_{i-1}):x_{i}\in Y_{k}\} を得る。組の補題の言明 4 を  P に適用して  P'=V\times Y_{k}=\{(x_{i-1},x_{i}):x_{i}\in Y_{k}\} を得る。拡大の補題を  P' に適用して  E_{i,Y_{k},n}=\{(x_{1},\ldots ,x_{n}):x_{i}\in Y_{k}\} を得る。
Case c:  \phi  が  x_{i}\in Y_{k}（ i=n=1）のとき、  E_{i,Y_{k},n}=Y_{k} である。
帰納ステップ： \phi  は  k(>0) 個の論理記号を含む。「 k 未満の個数の論理記号を含むすべての  \psi  に対して、定理が真である」という、帰納の仮説を仮定する。この条件下で、  k 個の論理記号を含む  \phi  に対して、定理が真であることを証明する。この証明において、クラス変数  Y_{1},\dots ,Y_{m} を  {\vec {Y}} で略記する。すると例えば論理式  \phi (x_{1},\dots ,x_{n},Y_{1},\dots ,Y_{m}) は  \phi (x_{1},\dots ,x_{n},{\vec {Y}}) のように書ける。
Case 1:  \phi (x_{1},\ldots ,x_{n},{\vec {Y}})=\neg \psi (x_{1},\ldots ,x_{n},{\vec {Y}}) のとき、  \psi  は  k-1 個の論理記号を含むため、帰納仮説は以下を満たす n-組のクラス  A がただ一つ存在することを含意する：
 \quad (x_{1},\ldots ,x_{n})\in A\iff \psi (x_{1},\ldots ,x_{n},{\vec {Y}}).
補修号の公理より、  \forall u\,[u\in \complement A\iff \neg (u\in A)] となるクラス  \complement A が存在する。しかし、  \complement A は  n>1 のとき  n-組以外の元を含む。 \complement _{V^{n}}A=\, \complement A\cap V^{n}=\, V^{n}\setminus A を用いて、この元を消去する。これはすべての  n-組のクラス  V^{n} の相対補集合である。すると、外延性の公理から  \complement _{V^{n}}A は以下を満たす n-組の唯一のクラスである： 
 {\begin{alignedat}{2}\quad &(x_{1},\ldots ,x_{n})\in \complement _{V^{n}}A&&\iff \neg [(x_{1},\ldots ,x_{n})\in A]\\&&&\iff \neg \psi (x_{1},\ldots ,x_{n},{\vec {Y}})\\&&&\iff \phi (x_{1},\ldots ,x_{n},{\vec {Y}}).\end{alignedat}}
Case 2:  \phi (x_{1},\ldots ,x_{n},{\vec {Y}})=\psi _{1}(x_{1},\ldots ,x_{n},{\vec {Y}})\land \psi _{2}(x_{1},\ldots ,x_{n},{\vec {Y}})のとき、  \psi _{1} と  \psi _{2} はいずれも  k 未満の個数の論理記号を含むため、帰納仮説は以下を満たす n-組のクラス  A がただ一つ存在することを含意する：
共通部分および外延性の公理から、  A_{1}\cap A_{2} は以下を満たす  n-組の唯一のクラスである：
 {\begin{alignedat}{2}\quad &(x_{1},\ldots ,x_{n})\in A_{1}\cap A_{2}&&\iff (x_{1},\ldots ,x_{n})\in A_{1}\land (x_{1},\ldots ,x_{n})\in A_{2}\\&&&\iff \psi _{1}(x_{1},\ldots ,x_{n},{\vec {Y}})\land \psi _{2}(x_{1},\ldots ,x_{n},{\vec {Y}})\\&&&\iff \phi (x_{1},\ldots ,x_{n},{\vec {Y}}).\end{alignedat}}
Case 3:  \phi (x_{1},\ldots ,x_{n},{\vec {Y}})=\exists x_{n+1}\psi (x_{1},\ldots ,x_{n},x_{n+1},{\vec {Y}}) のとき、  \psi  は  \phi  と比べると、量化子ネスト深さが 1 大きく、自由変数  x_{n+1} が多い。  \psi  は  k-1 個の論理記号を含むため、、帰納仮説は以下を満たす n-組のクラス  A がただ一つ存在することを含意する：
 \quad (x_{1},\ldots ,x_{n},x_{n+1})\in A\iff \psi (x_{1},\ldots ,x_{n},x_{n+1},{\vec {Y}}).
領域および外延性の公理から、  Dom(A) は以下を満たす  n-組の唯一のクラスである：
 {\begin{alignedat}{2}\quad &(x_{1},\ldots ,x_{n})\in Dom(A)&&\iff \exists x_{n+1}[((x_{1},\ldots ,x_{n}),x_{n+1})\in A]\\&&&\iff \exists x_{n+1}[(x_{1},\ldots ,x_{n},x_{n+1})\in A]\\&&&\iff \exists x_{n+1}\,\psi (x_{1},\ldots ,x_{n},x_{n+1},{\vec {Y}})\\&&&\iff \phi (x_{1},\ldots ,x_{n},{\vec {Y}}).\end{alignedat}}
ゲーデルは、クラス存在定理は「メタ定理（英語版）である。すなわち、システム（NBG）に関する定理であり、システム内の定理でではない…」と指摘した。  NBG 論理式の帰納によるメタ理論の中で証明されるため、クラス存在定理は NBG に関する定理である。また、その証明は、有限個の NBG 公理を持ち出す代わりに、与えられた論理式を満たすクラスを構築するためのNBG 公理の使い方を帰納的に表現する。すべての論理式に対して、こうした表現は NBG 内の存在の構成的証明に変えられる。したがって、このメタ理論で NBG のクラス存在定理の使い方を置き換えた NBG の証明を作ることができる。
再帰的なコンピュータプログラムで、与えられた論理式からクラスを簡単に構成することができる。このプログラムの定義はクラス存在定理の証明によらない。しかし、プログラムによって構成されるクラスが与えられた論理式を満たし、公理から構成されたかを確認するには、定理の証明が必要である。このプログラムのPascal形式のcase文を用いた擬似コードを以下に示す。 {\begin{array}{l}\mathbf {function} \;{\text{Class}}(\phi ,\,n)\\\quad {\begin{array}{rl}\mathbf {input} \!:\;\,&\phi {\text{ is a transformed formula of the form }}\phi (x_{1},\ldots ,x_{n},Y_{1},\ldots ,Y_{m});\\&n{\text{ specifies that a class of }}n{\text{-tuples is returned.}}\\\;\;\;\;\mathbf {output} \!:\;\,&{\text{class }}A{\text{ of }}n{\text{-tuples satisfying }}\\&\,\forall x_{1}\cdots \,\forall x_{n}[(x_{1},\ldots ,x_{n})\in A\iff \phi (x_{1},\ldots ,x_{n},Y_{1},\ldots ,Y_{m})].\end{array}}\\\mathbf {begin} \\\quad \mathbf {case} \;\phi \;\mathbf {of} \\\qquad {\begin{alignedat}{2}x_{i}\in x_{j}:\;\;&\mathbf {return} \;\,E_{i,j,n};&&{\text{// }}E_{i,j,n}\;\,=\{(x_{1},\dots ,x_{n}):x_{i}\in x_{j}\}\\x_{i}\in Y_{k}:\;\;&\mathbf {return} \;\,E_{i,Y_{k},n};&&{\text{// }}E_{i,Y_{k},n}=\{(x_{1},\dots ,x_{n}):x_{i}\in Y_{k}\}\\\neg \psi :\;\;&\mathbf {return} \;\,\complement _{V^{n}}{\text{Class}}(\psi ,\,n);&&{\text{// }}\complement _{V^{n}}{\text{Class}}(\psi ,\,n)=V^{n}\setminus {\text{Class}}(\psi ,\,n)\\\psi _{1}\land \psi _{2}:\;\;&\mathbf {return} \;\,{\text{Class}}(\psi _{1},\,n)\cap {\text{Class}}(\psi _{2},\,n);&&\\\;\;\;\;\,\exists x_{n+1}(\psi ):\;\;&\mathbf {return} \;\,Dom({\text{Class}}(\psi ,\,n+1));&&{\text{// }}x_{n+1}{\text{ is free in }}\psi ;{\text{ Class}}(\psi ,\,n+1)\\&\ &&{\text{// returns a class of }}(n+1){\text{-tuples}}\end{alignedat}}\\\quad \mathbf {end} \\\mathbf {end} \end{array}}
\phi  を 例 2 の論理式とする。関数呼び出し  A=Class(\phi ,1) でクラス  A を作成するが、以下で  \phi  と比較する。クラス  A の構成は、それを定義する論理式  \phi  の構成を反転することがわかる。
{\begin{alignedat}{2}&\phi \;&&=\;\;\exists x_{2}\,(x_{2}\!\in \!x_{1}\land \;\;\neg \;\;\;\;\exists x_{3}\;(x_{3}\!\in \!x_{2}))\,\land \;\;\,\exists x_{2}\,(x_{2}\!\in \!x_{1}\land \;\;\,\exists x_{3}\,(x_{3}\!\in \!x_{2}\,\land \;\;\neg \;\;\;\;\exists x_{4}\;(x_{4}\!\in \!x_{3})))\\&A\;&&=Dom\,(\;E_{2,1,2}\;\cap \;\complement _{V^{2}}\,Dom\,(\;E_{3,2,3}\;))\,\cap \,Dom\,(\;E_{2,1,2}\;\cap \,Dom\,(\;\,E_{3,2,3}\;\cap \;\complement _{V^{3}}\,Dom\,(\;E_{4,3,4}\;)))\end{alignedat}}