数学基礎論において、フォン・ノイマン＝ベルナイス＝ゲーデル集合論 (NBG) とはツェルメロ＝フレンケル集合論＋選択公理 (ZFC)の保存拡大である公理的集合論である。NBGでは、量化子の範囲を集合に限定した論理式によって定義される集合の集まりとして、クラスの概念を導入する。NBGは、すべての集合というクラスやすべての順序数というクラスといった、集合よりも大きいクラスを定義できる。モース＝ケリー集合論 (MK) は量化子の範囲がクラスである論理式によるクラスの定義を許容する。NBGは有限公理化できる一方、ZFCやMKではできない。
NBGのキーとなる定理はクラスの存在定理である。クラスの存在定理は、量化子の範囲を集合に限定した論理式それぞれに対して、論理式を満たす集合からなるクラスの存在を述べる。クラスは、クラスの論理式を一つずつ構築することで構成される。すべての集合論的な論理式は2種類の原子論理式（所属関係と等式）と有限個の論理記号から構築されるため、論理式を満足するクラスを構築するには有限個の公理があればよい。NBGが有限公理化できるのは、こうした理由による。クラスは他の概念の構築にも用いられ、集合論的パラドックスへの対処や、ZFCの選択公理より強いの説明に用いられる。
ジョン・フォン・ノイマンは1925年に集合論にクラスを導入した。彼の理論の原始概念は関数と引数であった。これらの概念を用いて、フォン・ノイマンはクラスと集合を定義した。; English translation: . パウル・ベルナイスはクラスと集合を原始概念とすることで、フォン・ノイマンの理論を再定式化した。, pp. 66–67. クルト・ゲーデルは、選択公理の相対的無矛盾性の証明と一般連続体仮説を用いてベルナイスの理論を単純化した。.
集合論におけるクラス
クラスの使用例 NBGにおいてクラスはいくつかの使用例がある：
クラスによって集合論を有限公理化する。. "非常に強い形の選択公理"を表現するのに用いられる。.—すなわち、のことである。大域選択公理の内容は以下の通り：すべての空でない集合 に対して である、すべての空でない集合のクラス上に定義された大域選択関数 が存在する。大域選択公理はZFCの選択公理よりも強い。ZFCの選択公理の内容は以下の通り：任意の空でない集合の集合 について、すべての に対して である 上の が存在する。 集合でないクラスが存在することを認めると、集合論的パラドックスは解決される。例えば、すべての順序数のクラス を集合であると仮定する。すると、 は で整列された推移的集合となる。すなわち、定義から は順序数である。したがって、 であるが、これは が で整列されていることに矛盾する。したがって、 は集合ではない。集合ではないクラスを真のクラスと呼ぶため、 は真のクラスである。. 真のクラスは集合などの作成に便利である。 大域選択公理と一般連続体仮説の相対的非矛盾性の証明において、ゲーデルは構成可能集合を作るのに真のクラスを用いた。ゲーデルはすべての順序数のクラス上の関数を構成した。すなわち、各順序数について、構成済の集合に対して集合を作る処理を適用することで構成可能集合を作った。構成可能集合はこの関数の像である。.
公理図式とクラス存在定理 ZFCの言葉にクラスが加えられれば、ZFCをクラス付きの集合論に変換するのが容易になる。まず、クラス解釈の公理図式を加える。この公理図式は以下の通り：量化子の範囲を集合に限定したすべての論理式 に対して、論理式を満たす -組からなるクラス が存在する—すなわち、 である。すると置換公理はクラスを用いる一つの公理で置き換えられる。最後に、ZFCの外延性の公理はクラスを扱う形に修正される：2つのクラスが持つ元が同じならば、それらのクラスは等しい。ほかのZFCの公理は修正されない。
以上の理論は有限公理化されていない。ZFCの置換公理図式は一つの公理で置き換えられる代わりに、クラス解釈の公理図式が導入されるからである。
この理論を有限個の公理で構築するには、まずクラス解釈の公理を有限個のクラス存在公理で置き換える。するとこれらの公理により、どの公理図式にもそれを満たすクラスが存在するというクラス存在定理が証明される。 この定理の証明には 7 つのクラス存在公理があれば十分である。これらのクラス存在公理は、論理式の構成から論理式を満たすクラスの構成へ変換するのに用いられる。
NBGの公理化
クラスと集合 NBGにはクラスと集合という 2 種類の対象がある。直感的には、どの集合も同時にクラスである。これを公理化する方法は 2 通り存在する。ベルナイスは 2 ソートの多ソート論理を用いた。, pp. 66–67. ゲーデルはソートの代わりに原始述語を用いた： を「 はクラスである」ことを、 を「 は集合である」ことを表す述語とする（ドイツ語では集合は Menge である)。ゲーデルは「すべての集合はクラスである」という公理と、「クラス がクラスの元であれば、 は集合である」という公理を導入した。. 述語はソートの回避のためによく使われる。 エリオット・メンデルソン (Elliott Mendelson) はゲーデルの考え方を元に、全てをクラスとした上で、 を表す述語 で集合を表すことで修正した。. この修正によって、ゲーデルのクラス述語と 2 つの公理は不要になる。
ベルナイスの 2 ソートのアプローチのほうが最初は自然に見えるかもしれないが、こちらは複雑な理論になる。 ベルナイスの理論では、どの集合も 2 種類の表現を持つ：一つは集合として、もう一つはクラスとしてである。同時に、2 つの 帰属関係がある：一つは "∈" で表される 2 つの集合間の関係、もう一つは "η" で表される集合とクラスの間の関係である。, pp. 66–67. 異なるソートの変数は議論領域中で互いに素な部分領域の元となるため、この冗長性は多ソート論理に必要になる。
これらの 2 つのアプローチで証明できるものは変わらないが、証明の書かれ方は変わってくる。ゲーデルのアプローチでは、 と がクラスであるとき は有効な表現である。ベルナイスのアプローチではこの表現は意味をなさない。しかし、 が集合であれば、等価な表現が存在する： 集合とクラスが同じ集合を元に持つならば、「集合 はクラス を代表する」と定義する。—すなわち、 。集合 がクラス を代表するという表現 は、ゲーデルの と等価である。, pp. 66–67.
本記事ではゲーデルのアプローチのメンデルソンによる修正版を用いて説明する。これは、NBG は等式を含む一階述語論理における公理系であることを意味し、原始概念はクラスと帰属関係のみであることを意味する。
外延性の公理と対の公理の定義 集合は、少なくとも 1 つのクラスに属するクラスである： のとき、かつそのときに限り は集合である。 集合でないクラスは真のクラスと呼ぶ： のとき、かつそのときに限り は真のクラスである。. したがって、どのクラスも集合または真のクラスであり、両方同時に当てはまることはない。
ゲーデルは大文字の変数をクラス上の変数、小文字の変数を集合上の変数とした。. また、ゲーデルは、すべての集合からなるクラス上に定義された関数や関係を含む特定のクラスは、大文字から始まる名前で表した。本記事ではゲーデルのこの表記法に従う。すると以下のように書ける： の代わりに の代わりに 以下の公理と定義はクラス存在定理の証明に必要である。
外延性の公理. 2 つのクラスが同じ元を持っていれば、それらは等しい。
Gödel's axiom A3 ().
この公理はZFCの外延性の公理をクラスに一般化したものである。
対の公理. と が集合であれば、元が と のみである集合 が存在する。
Gödel's axiom A4 ().
ZFCのように、外延性の公理は集合 がただ一つであることを含意する。これによって という表記ができる。
順序対は以下のように定義される。
対は順序対を使って再帰的に定義される：
クラス存在公理と正則性公理 クラス存在公理はクラス存在定理を証明するのに用いる：集合のみを量化する 個の集合の自由変数に関するすべての論理式について、その論理式を満たす -組のクラスが存在する。以下の例は、関数のクラスと合成関数を構築するクラスの 2 つのクラスから始める。この例はクラス存在定理を証明するのに必要な、クラス存在公理を導出する手法を説明する。
{| class="wikitable" |- style="text-align: left; vertical-align: top; style="background: white" |例 1: クラス と が関数であるならば、合成関数 は以下の論理式で定義される： この論理式は 2 つの集合に関する自由変数 と を持つため、クラス存在定理から以下の順序対のクラスの存在が導かれる：
この論理式は論理積 と存在記号 を使って簡潔に構築されているので、簡潔な論理式を表すクラスを使って と を含む論理式を表すクラスを生成するクラス演算が必要である。の論理式を表すクラスを作るには、であることから共通部分を用いる。の論理式を表すクラスを作るには、であることから領域を用いる
共通部分を求める前に、 と にそれぞれ含まれる組において、共通した変数を持つように他の要素が必要になる。元 を の組に、 元 を の組に加える：
の定義において、変数 は で制限されないため、 の定義域はすべての集合のクラス 上になる。同様に、 の定義において、変数 の定義域も 上になる。ここで与えられたクラスの組に（上の）追加の元を加える公理が必要になる。
次に、共通部分をとる準備として、変数を同じ順序で並べる：
から および から へは、2 種類の巡回が必要になる。ゆえに、組の元の巡回を扱う公理が必要になる。
と の共通部分は を表現する：
は として定義されるので、 の領域は で表現され、合成関数を生成する：
したがって、共通部分および領域の公理が必要である。
クラス存在公理は 2 つのグループに分かれる：述語に関する公理と、対に関する公理である。前者のグループには 4 つの公理が、後者のグループには 3 つの公理が含まれる。
述語に関する公理：
帰属. 1番めの要素が 2 番めの要素の元になるような順序対すべてを含むクラス が存在する。
Gödel's axiom B1 ().
共通部分（連言）. 任意の 2 つのクラス と に対して、 と にそれぞれ属する集合のみからなるクラス が存在する。
Gödel's axiom B2 ().
補集合（否定）. 任意のクラス に対して、 に属さない集合のみからなるクラス が存在する。
Gödel's axiom B3 ().
領域（存在量化子）. 任意のクラス に対して、 の順序対の最初の要素からなるクラス が存在する。
Gödel's axiom B4 ().
外延性の公理より、共通部分公理におけるクラス と補集合公理および領域公理におけるクラス はそれぞれただ一つ定まる。これらはそれぞれ以下のように表現される： and 一方、帰属公理はクラス 上の順序対の集合のみを規定するため、外延性の公理は帰属公理におけるクラス には適用できない。
最初 3 つの公理は空クラスおよびすべての集合のクラスの存在を含意する：帰属公理はクラス の存在を含意する。共通部分公理および補集合公理は、空クラスである の存在を含意する。外延性の公理により、このクラスはただ一つ定まり、これを で表す。 の補集合はすべての集合のクラス であり、これも外延性の公理からただ一つ定まる。すると、 を表す集合述語 は、クラスを量化することなく と再定義される。
対に関する公理：
との直積. 任意のクラス に対して、最初の要素が に属する順序対からなるクラス が存在する。
Bernays' axiom b(3) ().
巡回置換. 任意のクラス に対して、 の 3-組に巡回置換 を適用して得られる 3-組からなるクラス が存在する。
Gödel's axiom B7 ().
転置. 任意のクラス に対して、 の 3-組の後ろ 2 要素を入れ替えて得られる 3-組からなるクラス が存在する。
Gödel's axiom B8 ().
外延性から、 の直積公理は で表されるただ一つのクラスの存在を含意する。この公理はすべての -組に対してクラス を定義するのにも用いる： そして 。 がクラスならば、外延性は が の -組からなるただ一つのクラスであることを含意する。たとえば、帰属公理から、クラス が順序対ではない元を含むが、共通部分 は の順序対のみからなるようにクラス を構成できる。
巡回置換公理と転置公理はクラス の 3-組であることのみを規定するため、ただ一つのクラスの存在を含意しない。 3-組を規定することで、これらの公理は に対して -組についても規定する。なぜならば： 対に関する公理と領域公理は以下の補題を含意する。この補題はクラス存在定理の証明に用いる。
クラス存在定理の証明にはもう一つの公理、正則性公理が必要である。空クラスの存在が証明されるため、この公理のふつうの言明を用いる。
正則性公理. 空でないどの集合も、共通部分の要素が空となる元を少なくとも 1 つ持つ。
この公理は集合が自分自身に属さないことを含意する： と仮定して と置く。すると であるので である。これは が の唯一の元であることから、正則性公理と矛盾する。したがって、 である。また、正則性公理は集合の無限降下関係列の存在を禁止する：ゲーデルは、自身の1940年のモノグラフで、集合ではなくクラスに関して正則性公理を述べた。これは1938年の講義に基づいたものである。; . 1939年、ゲーデルは集合の正則性公理がクラスの正則性公理を含意することを証明した。; . 両文献ともにゲーデルの集合を含むが、カナモリのもののほうが現代的な用語を用いる分読みやすい。
クラス存在定理
この定理の証明は 2 ステップからなる：
与えられた論理式 を証明の帰納部分を簡略化する論理式に変換するため、変換規則を用いる。例えば、帰納部分で 3 ケースの論理記号のみを扱うため、変換後の論理式に用いる論理記号は , , のみとする。 変換後の論理式に対して、クラス存在定理を帰納的に証明する。変換後の論理式の構造を用い、クラス存在公理から論理式を満たす唯一の -組を構成する。
変換規則. 以下の規則 1 と 2 において、 と はそれぞれ集合とクラスの変数を表す。これらの 2 つの規則で の前のすべてのクラス変数とすべての等号を除去する。規則 1 や 2 をサブ論理式に適用する際は、 が論理式中の他の変数と異なるように を選ぶ。3 つの規則はサブ論理式に適用できなくなるまで適用を繰り返す。これによって、 , , , 、 集合変数、 の前に現れないクラス変数 論理式のみからなる論理式を構成する。
を に変換する。 外延性公理を用いて、 を に変換する。 論理的同一性を用いて、 and が含まれるサブ論理式を のみが含まれるサブ論理式に変換する。
変換規則：束縛変数. 例 1の合成関数論理式について、集合の自由変数を と に置き換えることを考える： 。帰納的証明で論理式 をなす が取り除かれる。しかし、クラス存在定理は添字つき変数を使って表されているため、この論理式は帰納法における仮定として期待される形式にならない。この問題は変数 を で置き換えることで解決できる。ネストされた量化子内の束縛変数を扱うには、量化子ごとに添字の数字を 1 ずつ増やしていけば良い。これによって規則 4 が導出される。規則 1 と 2 で量化された変数が増えるため、規則 4 はほかの規則よりもあとに適用しなければならない。
論理式に 以外の自由変数が含まれなければ、 個の量化子内にネストされた束縛変数を に置き換える。これらの変数は (量化子)ネスト深さ である。
{| class="wikitable" |- style="text-align: left; vertical-align: top; style="background: white" |例 2: の形のすべての集合からなるクラスを定義する論理式 に規則 4 を適用する。すなわち、少なくとも を含む集合と を含む集合— 例えば、 （ここで は集合である）。
が唯一の自由変数であるため、 である。量化された変数 がネスト深さ 2 の で 2 回現れる。 であるので、この下付き添字は 3 である。2 つの量化子の範囲が同じネスト深さの場合、それらは同一か互いに素である。 の 2 回の出現は量化子の範囲が互いに素であるためで、それゆえ互いに干渉することはない。
クラス存在定理の証明. 証明は与えられた論理式に変換規則を適用して、論理式を変換することから始める。この論理式は与えられた論理式と等価であるので、変換済みの論理式を証明すればクラス存在定理の証明が完了する。
ゲーデルは、クラス存在定理は「である。すなわち、システム（NBG）に関する定理であり、システム内の定理でではない…」と指摘した。 . NBG 論理式の帰納によるメタ理論の中で証明されるため、クラス存在定理は NBG に関する定理である。また、その証明は、有限個の NBG 公理を持ち出す代わりに、与えられた論理式を満たすクラスを構築するためのNBG 公理の使い方を帰納的に表現する。すべての論理式に対して、こうした表現は NBG 内の存在の構成的証明に変えられる。したがって、このメタ理論で NBG のクラス存在定理の使い方を置き換えた NBG の証明を作ることができる。
再帰的なコンピュータプログラムで、与えられた論理式からクラスを簡単に構成することができる。このプログラムの定義はクラス存在定理の証明によらない。しかし、プログラムによって構成されるクラスが与えられた論理式を満たし、公理から構成されたかを確認するには、定理の証明が必要である。このプログラムのPascal形式のcase文を用いた擬似コードを以下に示す。
を 例 2 の論理式とする。関数呼び出し でクラス を作成するが、以下で と比較する。クラス の構成は、それを定義する論理式 の構成を反転することがわかる。
クラス存在定理の拡張 ゲーデルはクラス存在定理を、クラスの関係（例えば や単項関係 ）、特別なクラス（例えば ）、演算（例えば や ）を含む論理式 に拡張した。. クラス存在定理を拡張するには、関係、特別なクラス、演算を定義する論理式が集合上で量化されていなければならない。すると はクラス存在定理の仮説を満たす等価な論理式に変換される。
以下の定義は論理式での関係、特別なクラス、演算の定義方法を特定する。
関係 を以下のように定義する： 特別なクラス を以下のように定義する： 演算 を以下のように定義する：
は以下のように定義される：
変数と特別なクラスは項である。 が 変数の演算でかつ が項であるならば、 は項である。
以下の変換規則は、関係、特別なクラス、演算を消去する。規則 2b, 3b, 4 をサブ論理式に適用する際は、 が論理式中の他の変数と異なるように を選ぶ。規則はサブ論理式に適用できなくなるまで適用を繰り返す。 は項を表すものとする。
関係 を定義論理式 で置き換える。 を特別なクラス の定義論理式とする。 を演算 の定義論理式とする。 外延性の公理を用いて、 を に変換する。
{| class="wikitable" |- style="text-align: left; vertical-align: top; style="background: white" |例 3: を変換する。
{| class="wikitable" |- style="text-align: left; vertical-align: top; style="background: white" |例 4: を変換する。
この例は各規則がどのように演算を消去するのか示すものである。
集合公理 クラス存在定理に必要だった対の公理と正則性公理は、上記の通り与えられている。NBG はほかに 4 つの集合公理を含む。このうち 3 つは集合に適用されるクラス演算として扱われる。
定義.以下が成り立てば は関数である集合論において、関数を定義する際に始域と終域を特定する必要はない（関数（集合論）を参照）。NBG の関数の定義では、 ZFC の定義のうち、順序類の集合を順序対のクラスに一般化したものになる。
ZFC における像、和集合、冪集合といった集合演算の定義もクラス演算に一般化される。 によるクラス の像は である。 この定義は を必要としない。クラス の和は となる。クラス の冪集合は となる。クラス存在定理の拡張版はこれらのクラスの存在を含意する。置換、和集合、冪集合の各公理は、これらの操作が集合に適用したときに集合となることを含意する。.
置換公理. が関数で が集合であるならば、 による の像 は集合である。
の定義に条件 は必要ないことは、以下の証明に用いる強い形の置換公理となる。
和集合の公理. が集合であるならば、 を含む集合が存在する。
冪集合公理. が集合であるならば、 を含む集合が存在する。
無限公理. のすべての元 に対して、 が の真部分集合である の元 が存在するような、空でない集合 が存在する。
無限公理と置換公理から空集合の存在が導かれる。クラス存在公理に関する議論において、空クラス の存在は示されている。ここで が集合であることを示そう。関数 と、無限公理で与えられる集合 を仮定する。置換公理より、 による の像は、 と等しい集合である。
NBG の無限公理は ZFC の無限公理から含意される： 。 であるため、 ZFC 公理の論理積の第1項、つまり が NBG 公理の論理積の第1項を含意する。ZFC 公理の論理積の第2項、すなわち が NBG 公理の論理積の第2項を含意する。 NBG の無限公理から ZFC の無限公理を証明するには、ほかの NBG 公理が必要である（弱い選択公理を参照）。
大域選択公理 クラスの概念により、NBG では ZFC より強い選択公理が許容される。 選択関数は、空でない集合の集合 上の関数 であり、 で を満たすものとして定義される。ZFC の選択公理は、すべての空でない集合の集合に対する選択関数が存在することを述べる。 大域選択関数はすべての空でない集合のクラス上で定義された関数 であり、すべての空でない集合 に対して を満たすものとして定義される。大域選択公理は大域選択関数が存在することを述べる。この公理は ZFC の選択公理を含意する。なぜならば空でない集合のすべての集合 に対して、 （ の への制限）は の選択関数となるからである。1964年、ウィリアム・B・イーストン (William B. Easton) は強制法を使い、選択公理と NBG の大域選択公理以外のすべての公理を満たすモデルを構築することによって、大域選択公理が選択公理よりも強いことを証明した。. ZFC の選択公理がどの集合も整列可能であることと等価であるのと同様に、大域選択公理はどのクラスも整列可能であることと等価である。
大域選択公理. すべての空でない集合から 1 つずつ元を選択できる関数が存在する。
歴史 代替文=refer to caption|サムネイル|491x491ピクセル|NBG 集合論を導いた手法の変遷
フォン・ノイマンの1925年の公理系 フォン・ノイマンは自身の公理系に関する入門的な論文を1925年に発行した。1928年、彼は公理系の詳細な説明を与えた。, . フォン・ノイマンの公理系は、関数と引数という原始概念の 2 領域に基づく。これらの領域は重複する—両方の領域に属するものは引数関数と呼ばれる。関数が NBG におけるクラスに対応し、引数関数が集合に対応する。フォン・ノイマンの原始的演算は、a(x) ではなく [a, x] で表される関数適用である。ここで a は関数、 x は引数を表す。この演算から引数が生成される。フォン・ノイマンはクラスと集合を、A と B の2値の引数関数を使って定義した。また、 [a, x] ≠ A ならば x ∈ a であると定義した。; English translation: .
集合論におけるフォン・ノイマンの仕事はゲオルグ・カントールの論文やエルンスト・ツェルメロの1908年の集合論公理、アドルフ・フレンケルとトアルフ・スコーレムによって独立に発表された1922年のツェルメロ集合論への批評によって広められた。 フレンケルとスコーレムはいずれも、ツェルメロの公理は集合 {Z0, Z1, Z2, ...} の存在を証明できないと指摘していた。ここで、 Z0 は自然数の集合であり、 Zn+1 は Zn の冪集合である。そして彼らはそのような集合の存在を保証する置換公理を導入した。. しかし、彼らはこの公理を適用しようとは思わなかった：フレンケルは「置換公理は『一般集合論』には強すぎる」とする一方、「スコーレムだけは置換公理を『導入できうる』と書いていた」と述べている。.
フォン・ノイマンはツェルメロ集合論の問題点に対処し、解決策を与えた：
順序数の理論 問題点：ツェルメロ集合論に置換公理が不足しているため、カントールの順序数の理論をツェルメロ集合論内で展開できない。 解決策： フォン・ノイマンは ∈-で整列可能な集合を用いて順序数を定義することで、カントールの理論を復活させ、 そしてキーとなる定理、すなわちすべての順序付け可能な集合が順序数についてであるような順序数に関する定理を、置換公理を用いて証明した。 フレンケルとスコーレムとは対照的に、フォン・ノイマンは集合論における置換公理の重要性を強調していた：「実際、この公理なしに順序数の理論は不可能だと思う」 (footnote); English translation: . 集合としては大きすぎるクラスを特定する基準 問題点：ツェルメロはそのような基準を示していなかった。ツェルメロ集合論では、パラドックスを引き起こす大きなクラスが排除されていたが、フレンケルとスコーレムが指摘したような、多くの集合が除外されていた。 解決策：フォン・ノイマンは基準を導入した：クラスが集合として大きすぎるのは、クラスからすべての集合のクラス V への全射が存在するときで、かつそのときに限る。フォン・ノイマンはこのような大きなクラスを元に持つ任意のクラスを許可しないことで、集合論的パラドックスを回避できることを知っていた。この制限と彼の基準を組み合わせることで、サイズ制限公理を得た： クラス C はどのクラスの元でもないのは、 C から V への全射が存在するとき、またそのときに限る。. 有限公理化 問題点：ツェルメロは彼の分出公理において、「定値命題関数」の不正確な概念を用いていた。 解決策：スコーレムはのちに ZFC で用いられる分出公理図式を導入し、フレンケルは等価な解決策を用いた。Fraenkel, Historical Introduction in . しかし、ツェルメロは「彼自身の観点では、集合論の土台となる自然数の概念をも暗に巻き込む部分があるため」いずれの方法も拒否した。 フォン・ノイマンは「定値命題関数」の概念を有限個の公理から構築できる関数で定式化することにより、公理図式を除外した。これによって、フォン・ノイマンの理論は有限公理化できるようになった。; English translation: . 1961年、リチャード・モンタギューは ZFC が有限公理化できないことを証明した。. 正則性公理