フォン・ノイマン＝ベルナイズ＝ゲーデル集合論

NBGでは、クラスにはいくつかの用途があります。

• これらは集合論の有限な公理化を生み出す。^{[ 4 ]}
• これらは「選択公理の非常に強い形式」^{[ 5 ]}、すなわち大域的選択公理、すなわち「大域的選択関数が存在する」を述べるために用いられる。${\displaystyle G}$すべての空でない集合のクラスで定義され、${\displaystyle G(x)\in x}$空でないすべての集合に対して${\displaystyle x.}$これはZFCの選択公理よりも強力です。すべての集合に対して${\displaystyle s}$空でない集合の選択肢関数が存在する${\displaystyle f}$定義済み${\displaystyle s}$そのため${\displaystyle f(x)\in x}$すべての人々のために${\displaystyle x\in s.}$^{[ a ]}
• 集合論のパラドックスは、一部のクラスが集合になり得ないことを認識することで解決される。例えば、クラスが${\displaystyle Ord}$すべての順序数の集合は、${\displaystyle Ord}$は、​​​${\displaystyle \in }$定義上、${\displaystyle Ord}$は序数です。したがって、${\displaystyle Ord\in Ord}$これは矛盾する${\displaystyle \in }$整然とした${\displaystyle Ord.}$したがって、${\displaystyle Ord}$は集合ではありません。集合ではないクラスは、真クラスと呼ばれます。${\displaystyle Ord}$は適切なクラスです。^{[ 6 ]}
• 適切なクラスは構成において有用である。ゲーデルは、大域選択公理と一般化連続体仮説の相対的無矛盾性の証明において、適切なクラスを用いて構成可能な宇宙を構築した。彼は、すべての順序数のクラス上に、各順序数に対して、既に構築された集合に集合構築演算を適用することによって構成可能な集合を構築する関数を構築した。構成可能な宇宙は、この関数の像である。^{[ 7 ]}

ZFC言語にクラスが追加されると、ZFCをクラスを持つ集合論に変換するのは容易になります。まず、クラス内包表記の公理スキーマを追加します。この公理スキーマは次のように記述します。すべての式に対して$\displaystyle \phi (x_{1},\ldots ,x_{n})$集合のみを量化するクラスが存在する${\displaystyle A}$から構成される${\displaystyle n}$-式を満たすタプル、つまり、${\displaystyle \forall x_{1}\cdots \,\forall x_{n}[(x_{1},\ldots ,x_{n})\in A\iff \phi (x_{1},\ldots ,x_{n})].}$次に、置換の公理図式は、クラスを使用する単一の公理に置き換えられます。最後に、ZFC の外延性の公理がクラスを扱うように変更されます。2 つのクラスが同じ要素を持つ場合、それらは同一です。ZFC の他の公理は変更されません。^{[ 8 ]}

この理論は有限個の公理で構成されているわけではない。ZFCの置換スキーマは単一の公理に置き換えられたが、クラス内包表記の公理スキーマが導入された。

有限個の公理を持つ理論を生成するために、まずクラス内包の公理図式を有限個のクラス存在公理に置き換えます。次に、これらの公理を使用して、公理図式のすべてのインスタンスを含意するクラス存在定理を証明します。^{[ 8 ]}この定理の証明には、式の構成をその式を満たすクラスの構成に変換するために使用される 7 つのクラス存在公理のみが必要です。

NBGにはクラスとセットという2種類のオブジェクトがあります。直感的には、すべてのセットはクラスでもあります。これを公理化する方法には2つあります。ベルネイズは、クラスとセットという2つのソートを用いた多ソート論理を使用しました。 ^{[ 2 ]}ゲーデルは、原始述語を導入することでソートを回避しました。${\displaystyle {\mathfrak {Cls}}(A)}$のために "${\displaystyle A}$「クラス」であり、${\displaystyle {\mathfrak {M}}(A)}$のために "${\displaystyle A}$は集合である（ドイツ語で「集合」はMenge）。彼はまた、すべての集合はクラスであり、クラスであれば${\displaystyle A}$クラスのメンバーである場合、${\displaystyle A}$は集合である。^{[ 9 ]}述語を用いるのは、ソートを排除する標準的な方法である。エリオット・メンデルソンは、すべてをクラスとし、集合述語を定義することで、ゲーデルのアプローチを修正した。${\displaystyle M(A)}$として${\displaystyle \exists C(A\in C).}$^{[ 10 ]}この修正により、ゲーデルのクラス述語と彼の2つの公理が削除されます。

バーネイズの2ソートアプローチは、最初はより自然に思えるかもしれないが、より複雑な理論を生み出す。^{[ b ]}バーネイズの理論では、すべての集合は2つの表現を持つ。1つは集合として、もう1つはクラスとしてである。また、2つのメンバーシップ関係がある。1つ目は「∈」で表され、2つの集合間の関係であり、2つ目は「η」で表され、集合とクラス間の関係である。^{[ 2 ]}この冗長性は、異なるソートの変数が議論領域の互いに素な部分領域に及ぶため、多ソート論理で必要とされる。

これら2つのアプローチの違いは、証明できる内容には影響しないが、命題の書き方には影響する。ゲーデルのアプローチでは、${\displaystyle A\in C}$どこ${\displaystyle A}$そして${\displaystyle C}$「クラスである」は有効な記述です。バーネイズのアプローチでは、この記述は意味を持ちません。しかし、${\displaystyle A}$は集合であり、同等の文が存在する: 「集合」を定義する${\displaystyle a}$クラスを表す${\displaystyle A}$「メンバーとして同じセットを持っている場合、つまり、${\displaystyle \forall x(x\in a\iff x\;\eta \;A).}$声明${\displaystyle a\;\eta \;C}$設定${\displaystyle a}$クラスを表す${\displaystyle A}$ゲーデルの${\displaystyle A\in C.}$^{[ 2 ]}

本稿で採用するアプローチは、ゲーデルのアプローチにメンデルソンの修正を加えたものである。つまり、NBGは等号を含む一階述語論理の公理系であり、その基本概念はクラスとメンバーシップ関係のみである。

セットとは、少なくとも1つのクラスに属するクラスのことです。${\displaystyle A}$集合であるのは、${\displaystyle \exists C(A\in C)}$集合ではないクラスは、適切なクラスと呼ばれます。${\displaystyle A}$適切なクラスであるのは、${\displaystyle \forall C(A\notin C)}$[ ^{12 ]したがって、すべてのクラスは} 集合か真クラスのどちらかであり、両方であるクラスは存在しない。

ゲーデルは、大文字の変数はクラスを、小文字の変数は集合を表すという慣習を導入した。^{[ 9 ]}ゲーデルはまた、すべての集合のクラスで定義された関数や関係など、特定のクラスを表すために大文字で始まる名前を使用した。この記事ではゲーデルの慣習を採用する。これにより、次のように記述できる。

クラス存在定理の証明には、以下の公理と定義が必要となる。

外延性の公理。2つのクラスが同じ要素を持つならば、それらは同一である。

${\displaystyle \forall A\,\forall B\,[\forall x(x\in A\iff x\in B)\implies A=B]}$^{[ 13 ]}

この公理は、ZFCの外延性公理をクラスに一般化したものである。

ペアリングの公理。${\displaystyle x}$そして${\displaystyle y}$集合であるならば、集合が存在する。${\displaystyle p}$その唯一のメンバーは${\displaystyle x}$そして${\displaystyle y}$。

${\displaystyle \forall x\,\forall y\,\exists p\,\forall z\,[z\in p\iff (z=x\,\lor \,z=y)]}$^{[ 14 ]}

ZFCと同様に、外延性の公理は集合の一意性を意味する。${\displaystyle p}$これにより、表記法を導入することができます。${\displaystyle \{x,y\}.}$

順序対は次のように定義されます。

${\displaystyle (x,y)=\{\{x\},\{x,y\}\}}$

タプルは順序対を用いて帰納的に定義される。

${\displaystyle (x_{1})=x_{1},}$

${\displaystyle {\text{For }}n>1\!:(x_{1},\ldots ,x_{n-1},x_{n})=((x_{1},\ldots ,x_{n-1}),x_{n}).}$^{[ c ]}

クラス存在公理を用いてクラス存在定理を証明する：すべての式に対して${\displaystyle n}$集合のみを量化する自由集合変数のクラスが存在する${\displaystyle n}$-それを満たすタプル。次の例では、関数である 2 つのクラスから始めて、複合関数を構築します。この例は、クラス存在定理を証明するために必要な手法を示しており、それによって必要なクラス存在公理が得られます。

クラス存在公理は、言語プリミティブを扱う公理とタプルを扱う公理の2つのグループに分けられます。最初のグループには4つの公理があり、2番目のグループには3つの公理があります。^{[ d ]}

言語プリミティブを扱うための公理：

メンバーシップ。クラスが存在する${\displaystyle E}$最初の要素が2番目の要素の要素であるすべての順序対を含む。

${\displaystyle \exists E\,\forall x\,\forall y\,[(x,y)\in E\iff x\in y]\!}$^{[ 18 ]}

交差（結合）。任意の2つのクラスについて${\displaystyle A}$そして${\displaystyle B}$クラスがあります${\displaystyle C}$両方に属する集合から正確に構成される${\displaystyle A}$そして${\displaystyle B}$。

${\displaystyle \forall A\,\forall B\,\exists C\,\forall x\,[x\in C\iff (x\in A\,\land \,x\in B)]}$^{[ 19 ]}

補数（否定）。任意のクラスに対して${\displaystyle A}$クラスがあります${\displaystyle B}$正確には、に属さない集合から成る${\displaystyle A}$。

${\displaystyle \forall A\,\exists B\,\forall x\,[x\in B\iff \neg (x\in A)]}$^{[ 20 ]}

ドメイン（存在量化子）。任意のクラスに対して${\displaystyle A}$クラスがあります${\displaystyle B}$順序対の最初の要素のみで構成される${\displaystyle A}$。

${\displaystyle \forall A\,\exists B\,\forall x\,[x\in B\iff \exists y((x,y)\in A)]}$^{[ 21 ]}

外延性の公理により、クラス${\displaystyle C}$交差公理とクラスにおいて${\displaystyle B}$補集合と定義域の公理は一意である。それらは以下のように表される。${\displaystyle A\cap B,}$${\displaystyle \complement (A),}$そして${\displaystyle Dom(A),}$それぞれ。^{[ e ]}

最初の３つの公理は、空のクラスとすべての集合のクラスの存在を意味する。メンバーシップ公理は、クラスの存在を意味する。${\displaystyle E.}$交差と補集合の公理は、${\displaystyle E\cap \complement (E)}$これは空である。外延性の公理により、このクラスは一意であり、で表される。${\displaystyle \emptyset .}$補数${\displaystyle \emptyset }$クラスは${\displaystyle V}$すべての集合の中で、外延性によっても一意である。集合述語${\displaystyle M(A)}$これは次のように定義されました${\displaystyle \exists C(A\in C)}$は、現在次のように再定義されています。${\displaystyle A\in V}$クラスをまたいで定量化することを避けるため。

タプルを扱うための公理：

製品​${\displaystyle V}$どのクラスでも${\displaystyle A}$クラスがあります${\displaystyle B}$最初の成分が${\displaystyle A}$。

${\displaystyle \forall A\,\exists B\,\forall u\,[u\in B\iff \exists x\,\exists y\,(u=(x,y)\land x\in A)]}$^{[ 23 ]}

円順列。任意のクラスに対して${\displaystyle A}$クラスがあります${\displaystyle B}$その3タプルは、円順列を適用することによって得られる。${\displaystyle (y,z,x)\mapsto (x,y,z)}$3タプルへ${\displaystyle A}$。

${\displaystyle \forall A\,\exists B\,\forall x\,\forall y\,\forall z\,[(x,y,z)\in B\iff (y,z,x)\in A]}$^{[ 24 ]}

転置。任意のクラスに対して${\displaystyle A}$クラスがあります${\displaystyle B}$その 3タプルは、 の3タプルの最後の 2 つのコンポーネントを転置することによって得られる。${\displaystyle A}$。

${\displaystyle \forall A\,\exists B\,\forall x\,\forall y\,\forall z\,[(x,y,z)\in B\iff (x,z,y)\in A]}$^{[ 25 ]}

外延性により、${\displaystyle V}$公理は、一意のクラスの存在を意味し、それは次のように表される。${\displaystyle A\times V.}$この公理はクラスを定義するために使用されます${\displaystyle V^{n}}$すべての${\displaystyle n}$-タプル:${\displaystyle V^{1}=V}$そして${\displaystyle V^{n+1}=V^{n}\times V.\,}$もし${\displaystyle A}$クラスであるということは、外延性は${\displaystyle A\cap V^{n}}$は、${\displaystyle n}$-タプル${\displaystyle A.}$例えば、メンバーシップ公理はクラスを生成する${\displaystyle E}$順序対ではない要素を含む可能性がある一方、交差部分は${\displaystyle E\cap V^{2}}$順序対のみを含む${\displaystyle E}$。

円順列と転置の公理は、クラスの 3 タプルのみを指定するため、一意のクラスの存在を意味しません。${\displaystyle B.}$3 タプルを指定することで、これらの公理は、${\displaystyle n}$-タプル${\displaystyle n\geq 4}$以来：$${\displaystyle (x_{1},\ldots ,x_{n-2},x_{n-1},x_{n})=((x_{1},\ldots ,x_{n-2}),x_{n-1},x_{n}).}$$タプルを扱うための公理と領域公理は、クラス存在定理の証明で使用される次の補題を導きます。

クラス存在定理を証明するには、もう1つの公理、すなわち正則性の公理が必要です。空クラスの存在は既に証明されているので、この公理の通常の記述を以下に示します。^{[ f ]}

正則性の公理。空でない集合はすべて、少なくとも１つの共通要素を持たない要素を持つ。 $${\displaystyle \forall a\,[a\neq \emptyset \implies \exists u(u\in a\land u\cap a=\emptyset )].}$$

この公理は、集合がそれ自身に属することはできないことを示唆している。${\displaystyle x\in x}$そして${\displaystyle a=\{x\}.}$それから${\displaystyle x\cap a\neq \emptyset }$以来${\displaystyle x\in x\cap a.}$これは規則性の公理に矛盾する。${\displaystyle x}$は唯一の要素です${\displaystyle a.}$したがって、${\displaystyle x\notin x.}$正則性の公理は、集合の無限降順のメンバーシップ列も禁止する。$${\displaystyle \cdots \in x_{n+1}\in x_{n}\in \cdots \in x_{1}\in x_{0}.}$$

ゲーデルは、1938年に行われた講義に基づいて1940年に発表したモノグラフの中で、集合ではなくクラスの正則性を述べた。 ^{[ 26 ]} 1939年には、集合の正則性がクラスの正則性を意味することを証明した。^{[ 27 ]}

この定理の証明は2つのステップで行います。

1. 変換ルールは、与えられた式を変換するために使用されます。${\displaystyle \phi }$証明の帰納部分を簡略化する同等の式に変換します。たとえば、変換後の式に含まれる論理記号は、${\displaystyle \neg }$、${\displaystyle \land }$、 そして${\displaystyle \exists }$したがって、帰納法は論理記号をわずか3つの場合で扱います。
2. クラス存在定理は、変換された式に対して帰納的に証明される。変換された式の構造に導かれて、クラス存在公理を使用して、一意のクラスを生成する。${\displaystyle n}$式を満たすタプル。

変換ルール。以下のルール1と2では、${\displaystyle \Delta }$そして${\displaystyle \Gamma }$セットまたはクラス変数を表します。これらの 2 つのルールは、クラス変数のすべての出現を、${\displaystyle \in }$等号のすべての出現箇所。ルール 1 または 2 がサブ式に適用されるたびに、${\displaystyle i}$選ばれるのは、${\displaystyle z_{i}}$現在の式内の他の変数と異なる。3 つのルールは、適用できるサブ式がなくなるまで繰り返される。これにより、のみで構成される式が生成される。${\displaystyle \neg }$、${\displaystyle \land }$、${\displaystyle \exists }$、${\displaystyle \in }$変数、クラス変数${\displaystyle Y_{k}}$どこ${\displaystyle Y_{k}}$前に現れない${\displaystyle \in }$。

1. ${\displaystyle \,Y_{k}\in \Gamma }$に変化する${\displaystyle \exists z_{i}(z_{i}=Y_{k}\,\land \,z_{i}\in \Gamma ).}$
2. 外延性は変換するために用いられる${\displaystyle \Delta =\Gamma }$の中へ${\displaystyle \forall z_{i}(z_{i}\in \Delta \iff z_{i}\in \Gamma ).}$
3. 論理的恒等式は、以下の部分式を変換するために使用されます。${\displaystyle \lor ,\implies ,\iff ,}$そして${\displaystyle \forall }$サブフォーミュラのみを使用する${\displaystyle \neg ,\land ,}$そして${\displaystyle \exists .}$

変換ルール：束縛変数。例1の合成関数式を考え、その自由集合変数を次のように置き換えます。${\displaystyle x_{1}}$そして${\displaystyle x_{2}}$:${\displaystyle \exists t[(x_{1},t)\in F\,\land \,(t,x_{2})\in G].}$帰納的証明は${\displaystyle \exists t}$それによって次の式が得られる${\displaystyle (x_{1},t)\in F\land (t,x_{2})\in G.}$しかし、クラス存在定理は添え字付き変数に対して述べられているため、この式は帰納法の仮説が期待する形式とは異なっている。この問題は変数を置き換えることで解決される。${\displaystyle t}$と${\displaystyle x_{3}.}$入れ子になった量化子内の束縛変数は、量化子が続くごとに添え字を1ずつ増やすことで処理されます。これにより規則4が得られますが、規則1と規則2は量化変数を生成するため、規則4は他の規則の後に適用される必要があります。

4. 式に自由セット変数が含まれない場合、${\displaystyle x_{1},\dots ,x_{n},}$次に、その中にネストされたバインド変数${\displaystyle q}$量指定子は${\displaystyle x_{n+q}}$これらの変数は（量化子）のネスト深度を持つ${\displaystyle q}$。

クラス存在定理の証明。証明は、与えられた式に変換規則を適用して変換後の式を生成することから始まります。この式は与えられた式と等価であるため、変換後の式に対するクラス存在定理を証明することで証明が完了します。

ゲーデルは、クラス存在定理は「メタ定理、つまりシステム[NBG]に関する定理であって、システム内の定理ではない」と指摘した^{[ 30 ]}。NBGに関する定理であるのは、メタ理論においてNBG式への帰納によって証明されるからである。また、その証明は、有限個のNBG公理を呼び出す代わりに、与えられた式を満たすクラスを構成するためにNBG公理をどのように使用するかを帰納的に記述する。すべての式について、この記述はNBG内の構成的存在証明に変換できる。したがって、このメタ定理は、NBGのクラス存在定理の使用を置き換えるNBG証明を生成できる。

再帰的なコンピュータプログラムは、与えられた式からクラスを構築する過程を簡潔に表現します。このプログラムの定義は、クラス存在定理の証明に依存しません。ただし、プログラムによって構築されたクラスが与えられた式を満たし、公理を用いて構築されていることを証明するには、その証明が必要です。このプログラムは、Pascalスタイルのcase 文を用いた擬似コードで記述されています。^{[ i ]}$${\displaystyle {\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{ は }}\psi で自由です ;{\text{ Class}}(\psi ,\,n+1)\\&\ &&{\text{// }}(n+1){\text{-タプル}}のクラスを返します\end{alignedat}}\\\quad \mathbf {end} \\\mathbf {end} \end{array}}}

させて${\displaystyle \phi }$例2の式とする。関数呼び出し${\displaystyle A=Class(\phi ,1)}$クラスを生成する${\displaystyle A,}$以下で比較するもの${\displaystyle \phi .}$これは、クラスの構築が${\displaystyle A}$その定義式の構造を反映している${\displaystyle \phi .}$

$${\displaystyle {\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}}}$$