数学基礎論 において、フォン・ノイマン＝ベルナイス＝ゲーデル集合論 (NBG ) とはツェルメロ＝フレンケル集合論＋選択公理 (ZFC)の保存拡大 である公理的集合論 である。NBGでは、量化子 の範囲を集合に限定した論理式 によって定義される集合 の集まりとして、クラス の概念を導入する。NBGは、すべての集合というクラスやすべての順序数 というクラスといった、集合よりも大きいクラスを定義できる。モース＝ケリー集合論 (MK) は量化子の範囲がクラスである論理式によるクラスの定義を許容する。NBGは有限公理化できる一方、ZFCやMKではできない。
NBGのキーとなる定理はクラスの存在定理である。クラスの存在定理は、量化子の範囲を集合に限定した論理式それぞれに対して、論理式を満たす集合からなるクラスの存在を述べる。クラスは、クラスの論理式を一つずつ構築することで構成される。すべての集合論的な論理式は2種類の原子論理式 （所属関係 と等式 ）と有限個の論理記号 から構築されるため、論理式を満足するクラスを構築するには有限個の公理 があればよい。NBGが有限公理化できるのは、こうした理由による。クラスは他の概念の構築にも用いられ、集合論的パラドックス への対処や、ZFCの選択公理 より強い大域選択公理 （英語版 ）
ジョン・フォン・ノイマン は1925年に集合論にクラスを導入した。彼の理論の原始概念 （英語版 ） 関数 と引数であった。これらの概念を用いて、フォン・ノイマンはクラスと集合を定義した。[1] パウル・ベルナイス はクラスと集合を原始概念とすることで、フォン・ノイマンの理論を再定式化した。[2] クルト・ゲーデル は、選択公理 の相対的無矛盾性 の証明と一般連続体仮説 を用いてベルナイスの理論を単純化した。[3]
集合論におけるクラス [ 編集 ] クラスの使用例 [ 編集 ] NBGにおいてクラスはいくつかの使用例がある：
クラスによって集合論を有限公理化する。[4]
"非常に強い形の選択公理 "を表現するのに用いられる。[5] 大域選択公理 （英語版 ）
x
{\displaystyle x}
G
(
x
)
∈
x
{\displaystyle G(x)\in x}
G
{\displaystyle G}
s
{\displaystyle s}
x
∈
s
{\displaystyle x\in s}
f
(
x
)
∈
x
{\displaystyle f(x)\in x}
s
{\displaystyle s}
選択関数 （英語版 ）
f
{\displaystyle f}
[注釈 1]
集合でないクラスが存在することを認めると、集合論的パラドックス は解決される。例えば、すべての順序数 のクラス
O
r
d
{\displaystyle Ord}
O
r
d
{\displaystyle Ord}
∈
{\displaystyle \in }
整列された 推移的集合 となる。すなわち、定義から
O
r
d
{\displaystyle Ord}
O
r
d
∈
O
r
d
{\displaystyle Ord\in Ord}
O
r
d
{\displaystyle Ord}
∈
{\displaystyle \in }
O
r
d
{\displaystyle Ord}
真のクラス と呼ぶため、
O
r
d
{\displaystyle Ord}
[6]
一般連続体仮説 の相対的非矛盾性の証明において、ゲーデルは構成可能集合 を作るのに真のクラスを用いた。ゲーデルはすべての順序数のクラス上の関数を構成した。すなわち、各順序数について、構成済の集合に対して集合を作る処理を適用することで構成可能集合を作った。構成可能集合はこの関数の像 である。[7] 公理型とクラス存在定理 [ 編集 ] 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})]}
置換公理 はクラスを用いる一つの公理で置き換えられる。最後に、ZFCの外延性の公理 はクラスを扱う形に修正される：2 つのクラスが同じ元を持つならば、それらのクラスは等しい。ほかのZFCの公理は修正されない。[8]
この理論は有限公理化されない。ZFCの置換公理型は一つの公理で置き換えられるが、クラス解釈の公理はZFCに導入されていないからである。
この理論を有限個の公理で構築するには、まずクラス解釈の公理を有限個のクラス外延性の公理 で置き換える。するとこれらの公理は、公理系中のどの公理をも含意するクラス存在定理に用いられる。[8] この理論の証明 には 7 つのクラス存在公理があれば十分である。これらのクラス存在公理は、論理式の構成から論理式を満たすクラスの構成へ変換するのに用いられる。
NBGの公理化 [ 編集 ] クラスと集合 [ 編集 ] NBGにはクラスと集合という 2 種類の対象がある。直感的には、どの集合も同時にクラスである。これを公理化する方法は 2 通り存在する。ベルナイスは 2 ソートの多ソート論理 を用いた。[2]
C
l
s
(
A
)
{\displaystyle {\mathfrak {Cls}}(A)}
A
{\displaystyle A}
M
(
A
)
{\displaystyle {\mathfrak {M}}(A)}
A
{\displaystyle A}
Menge である)。ゲーデルは「すべての集合はクラスである」という公理と、「クラス
A
{\displaystyle A}
A
{\displaystyle A}
[9]
∃
C
(
A
∈
C
)
{\displaystyle \exists C(A\in C)}
M
(
A
)
{\displaystyle M(A)}
[10]
ベルナイスの 2 ソートのアプローチのほうが最初は自然に見えるかもしれないが、こちらは複雑な理論になる。[注釈 2] 帰属関係 がある：一つは "∈" で表される 2 つの集合間の関係、もう一つは "η" で表される集合とクラスの間の関係である。[2] 議論領域 中で互いに素な部分領域の元となるため、この冗長性は多ソート論理に必要になる。
これらの 2 つのアプローチで証明できるものは変わらないが、証明の書かれ方は変わってくる。ゲーデルのアプローチでは、
A
{\displaystyle A}
C
{\displaystyle C}
A
∈
C
{\displaystyle A\in C}
A
{\displaystyle A}
a
{\displaystyle a}
A
{\displaystyle A}
∀
x
(
x
∈
a
⟺
x
η
A
)
{\displaystyle \forall x(x\in a\iff x\;\eta \;A)}
a
{\displaystyle a}
A
{\displaystyle A}
a
η
C
{\displaystyle a\;\eta \;C}
A
∈
C
{\displaystyle A\in C}
[2]
本記事ではゲーデルのアプローチのメンデルソンによる修正版を用いて説明する。これは、NBG は等式 を含む一階述語論理 における公理系 であることを意味し、原始概念 （英語版 ）
外延性の公理と対の公理の定義 [ 編集 ] 集合は、少なくとも 1 つのクラスに属するクラスである：
∃
C
(
A
∈
C
)
{\displaystyle \exists C(A\in C)}
A
{\displaystyle A}
∀
C
(
A
∉
C
)
{\displaystyle \forall C(A\notin C)}
A
{\displaystyle A}
[12]
ゲーデルは大文字の変数をクラス上の変数、小文字の変数を集合上の変数とした。[9]
∃
x
ϕ
(
x
)
{\displaystyle \exists x\,\phi (x)}
∃
x
(
∃
C
(
x
∈
C
)
∧
ϕ
(
x
)
)
{\displaystyle \exists x{\bigl (}\exists C(x\in C)\land \phi (x){\bigr )}}
∀
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]}
[13] この公理はZFCの外延性の公理 をクラスに一般化したものである。
対の公理 .
x
{\displaystyle x}
y
{\displaystyle y}
x
{\displaystyle x}
y
{\displaystyle y}
p
{\displaystyle p}
∀
x
∀
y
∃
p
∀
z
[
z
∈
p
⟺
(
z
=
x
∨
z
=
y
)
]
{\displaystyle \forall x\,\forall y\,\exists p\,\forall z\,[z\in p\iff (z=x\,\lor \,z=y)]}
[14] ZFCのように、外延性の公理は集合
p
{\displaystyle p}
{
x
,
y
}
{\displaystyle \{x,y\}}
順序対 は以下のように定義される。
(
x
,
y
)
=
{
{
x
}
,
{
x
,
y
}
}
{\displaystyle (x,y)=\{\{x\},\{x,y\}\}}
対は順序対を使って再帰的に定義 される：
(
x
1
)
=
x
1
,
{\displaystyle (x_{1})=x_{1},}
For
n
>
1
:
(
x
1
,
…
,
x
n
−
1
,
x
n
)
=
(
(
x
1
,
…
,
x
n
−
1
)
,
x
n
)
.
{\displaystyle {\text{For }}n>1\!:(x_{1},\ldots ,x_{n-1},x_{n})=((x_{1},\ldots ,x_{n-1}),x_{n}).}
[注釈 3]
クラス存在公理と正則性公理 [ 編集 ] クラス存在公理はクラス存在定理を証明するのに用いる：集合のみを量化する
n
{\displaystyle n}
自由変数 に関するすべての論理式について、その論理式を満たす
n
{\displaystyle n}
関数 のクラスと合成関数 を構築するクラスの 2 つのクラスから始める。この例はクラス存在定理を証明するのに必要な、クラス存在公理を導出する手法を説明する。
例 1: クラス
F
{\displaystyle F}
G
{\displaystyle G}
G
∘
F
{\displaystyle G\circ F}
∃
t
[
(
x
,
t
)
∈
F
∧
(
t
,
y
)
∈
G
]
.
{\displaystyle \exists t[(x,t)\in F\,\land \,(t,y)\in G].}
x
{\displaystyle x}
y
{\displaystyle y}
G
∘
F
=
{
(
x
,
y
)
:
∃
t
[
(
x
,
t
)
∈
F
∧
(
t
,
y
)
∈
G
]
}
.
{\displaystyle G\circ F\,=\,\{(x,y):\exists t[(x,t)\in F\,\land \,(t,y)\in G]\}.}
この論理式は論理積
∧
{\displaystyle \land }
存在記号
∃
{\displaystyle \exists }
∧
{\displaystyle \land }
∃
{\displaystyle \exists }
演算 が必要である。
∧
{\displaystyle \land }
x
∈
A
∩
B
⟺
x
∈
A
∧
x
∈
B
{\displaystyle x\in A\cap B\iff x\in A\land x\in B}
共通部分 を用いる。
∃
{\displaystyle \exists }
x
∈
D
o
m
(
A
)
⟺
∃
t
[
(
x
,
t
)
∈
A
]
.
{\displaystyle x\in Dom(A)\iff \exists t[(x,t)\in A].}
領域 を用いる
共通部分を求める前に、
F
{\displaystyle F}
G
{\displaystyle G}
y
{\displaystyle y}
F
{\displaystyle F}
x
{\displaystyle x}
G
{\displaystyle G}
F
′
=
{
(
x
,
t
,
y
)
:
(
x
,
t
)
∈
F
}
{\displaystyle F'=\{(x,t,y):(x,t)\in F\}\,}
G
′
=
{
(
t
,
y
,
x
)
:
(
t
,
y
)
∈
G
}
{\displaystyle \,G'=\{(t,y,x):(t,y)\in G\}}
F
′
{\displaystyle F'}
y
{\displaystyle y}
(
x
,
t
)
∈
F
{\displaystyle (x,t)\in F}
y
{\displaystyle y}
V
{\displaystyle V}
G
′
{\displaystyle G'}
x
{\displaystyle x}
V
{\displaystyle V}
V
{\displaystyle V}
次に、共通部分をとる準備として、変数を同じ順序で並べる：
F
″
=
{
(
x
,
y
,
t
)
:
(
x
,
t
)
∈
F
}
{\displaystyle F''=\{(x,y,t):(x,t)\in F\}\,}
G
″
=
{
(
x
,
y
,
t
)
:
(
t
,
y
)
∈
G
}
{\displaystyle \,G''=\{(x,y,t):(t,y)\in G\}}
F
′
{\displaystyle F'}
F
″
{\displaystyle F''}
G
′
{\displaystyle G'}
G
″
{\displaystyle G''}
巡回 が必要になる。ゆえに、組の元の巡回を扱う公理が必要になる。
F
″
{\displaystyle F''}
G
″
{\displaystyle G''}
∧
{\displaystyle \land }
F
″
∩
G
″
=
{
(
x
,
y
,
t
)
:
(
x
,
t
)
∈
F
∧
(
t
,
y
)
∈
G
}
{\displaystyle F''\cap G''=\{(x,y,t):(x,t)\in F\,\land \,(t,y)\in G\}}
(
x
,
y
,
t
)
{\displaystyle (x,y,t)}
(
(
x
,
y
)
,
t
)
{\displaystyle ((x,y),t)}
F
″
∩
G
″
{\displaystyle F''\cap G''}
∃
t
{\displaystyle \exists t}
G
∘
F
=
D
o
m
(
F
″
∩
G
″
)
=
{
(
x
,
y
)
:
∃
t
(
(
x
,
t
)
∈
F
∧
(
t
,
y
)
∈
G
)
}
{\displaystyle G\circ F=Dom(F''\cap G'')=\{(x,y):\exists t((x,t)\in F\,\land \,(t,y)\in G)\}}
クラス存在公理は 2 つのグループに分かれる：述語に関する公理と、対に関する公理である。前者のグループには 4 つの公理が、後者のグループには 3 つの公理が含まれる。[注釈 4]
述語に関する公理：
帰属. 1番めの要素が 2 番めの要素の元になるような順序対すべてを含むクラス
E
{\displaystyle E}
∃
E
∀
x
∀
y
[
(
x
,
y
)
∈
E
⟺
x
∈
y
]
{\displaystyle \exists E\,\forall x\,\forall y\,[(x,y)\in E\iff x\in y]\!}
[18] 共通部分（連言）. 任意の 2 つのクラス
A
{\displaystyle A}
B
{\displaystyle B}
A
{\displaystyle A}
B
{\displaystyle B}
C
{\displaystyle C}
∀
A
∀
B
∃
C
∀
x
[
x
∈
C
⟺
(
x
∈
A
∧
x
∈
B
)
]
{\displaystyle \forall A\,\forall B\,\exists C\,\forall x\,[x\in C\iff (x\in A\,\land \,x\in B)]}
[19] 補集合 （否定）.
A
{\displaystyle A}
A
{\displaystyle A}
B
{\displaystyle B}
∀
A
∃
B
∀
x
[
x
∈
B
⟺
¬
(
x
∈
A
)
]
{\displaystyle \forall A\,\exists B\,\forall x\,[x\in B\iff \neg (x\in A)]}
[20] 領域（存在量化子）. 任意のクラス
A
{\displaystyle A}
A
{\displaystyle A}
B
{\displaystyle B}
∀
A
∃
B
∀
x
[
x
∈
B
⟺
∃
y
(
(
x
,
y
)
∈
A
)
]
{\displaystyle \forall A\,\exists B\,\forall x\,[x\in B\iff \exists y((x,y)\in A)]}
[21] 外延性の公理より、共通部分公理におけるクラス
C
{\displaystyle C}
B
{\displaystyle B}
A
∩
B
,
{\displaystyle A\cap B,}
∁
A
,
{\displaystyle \complement A,}
D
o
m
(
A
)
.
{\displaystyle Dom(A).}
[注釈 5]
E
{\displaystyle E}
E
{\displaystyle E}
E
{\displaystyle E}
E
∩
∁
E
{\displaystyle E\cap \complement E}
∅
{\displaystyle \emptyset }
∅
{\displaystyle \emptyset }
V
{\displaystyle V}
∃
C
(
A
∈
C
)
{\displaystyle \exists C(A\in C)}
M
(
A
)
{\displaystyle M(A)}
A
∈
V
{\displaystyle A\in V}
対に関する公理：
V
{\displaystyle V}
直積 .
A
{\displaystyle A}
A
{\displaystyle A}
B
{\displaystyle B}
∀
A
∃
B
∀
u
[
u
∈
B
⟺
∃
x
∃
y
(
u
=
(
x
,
y
)
∧
x
∈
A
)
]
{\displaystyle \forall A\,\exists B\,\forall u\,[u\in B\iff \exists x\,\exists y\,(u=(x,y)\land x\in A)]}
[23] 巡回置換 .
A
{\displaystyle A}
A
{\displaystyle A}
(
y
,
z
,
x
)
↦
(
x
,
y
,
z
)
{\displaystyle (y,z,x)\mapsto (x,y,z)}
B
{\displaystyle B}
∀
A
∃
B
∀
x
∀
y
∀
z
[
(
x
,
y
,
z
)
∈
B
⟺
(
y
,
z
,
x
)
∈
A
]
{\displaystyle \forall A\,\exists B\,\forall x\,\forall y\,\forall z\,[(x,y,z)\in B\iff (y,z,x)\in A]}
[24] 転置 .
A
{\displaystyle A}
A
{\displaystyle A}
B
{\displaystyle B}
∀
A
∃
B
∀
x
∀
y
∀
z
[
(
x
,
y
,
z
)
∈
B
⟺
(
x
,
z
,
y
)
∈
A
]
{\displaystyle \forall A\,\exists B\,\forall x\,\forall y\,\forall z\,[(x,y,z)\in B\iff (x,z,y)\in A]}
[25] 外延性から、
V
{\displaystyle V}
A
×
V
{\displaystyle A\times V}
n
{\displaystyle n}
V
n
{\displaystyle V^{n}}
V
1
=
V
{\displaystyle V^{1}=V}
V
n
+
1
=
V
n
×
V
{\displaystyle V^{n+1}=V^{n}\times V}
A
{\displaystyle A}
A
∩
V
n
{\displaystyle A\cap V^{n}}
A
{\displaystyle A}
n
{\displaystyle n}
E
{\displaystyle E}
E
∩
V
2
{\displaystyle E\cap V^{2}}
E
{\displaystyle E}
E
{\displaystyle E}
巡回置換公理と転置公理はクラス
B
{\displaystyle B}
n
≥
4
{\displaystyle n\geq 4}
n
{\displaystyle n}
(
x
1
,
…
,
x
n
−
2
,
x
n
−
1
,
x
n
)
=
(
(
x
1
,
…
,
x
n
−
2
)
,
x
n
−
1
,
x
n
)
.
{\displaystyle (x_{1},\ldots ,x_{n-2},x_{n-1},x_{n})=((x_{1},\ldots ,x_{n-2}),x_{n-1},x_{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]}
∀
A
∃
B
3
∀
x
∀
y
∀
z
[
(
x
,
y
,
z
)
∈
B
3
⟺
(
x
,
y
)
∈
A
]
{\displaystyle \forall A\,\exists B_{3}\,\forall x\,\forall y\,\forall z\,[(x,y,z)\in B_{3}\iff (x,y)\in A]}
∀
A
∃
B
4
∀
x
∀
y
∀
z
[
(
y
,
x
)
∈
B
4
⟺
(
x
,
y
)
∈
A
]
{\displaystyle \forall A\,\exists B_{4}\,\forall x\,\forall y\,\forall z\,[(y,x)\in B_{4}\iff (x,y)\in A]}
クラス存在定理の証明にはもう一つの公理、正則性公理 が必要である。空クラスの存在が証明されるため、この公理のふつうの言明を用いる。[注釈 6]
正則性公理 .
∀
a
[
a
≠
∅
⟹
∃
u
(
u
∈
a
∧
u
∩
a
=
∅
)
]
.
{\displaystyle \forall a\,[a\neq \emptyset \implies \exists u(u\in a\land u\cap a=\emptyset )].}
この公理は集合が自分自身に属さないことを含意する：
x
∈
x
{\displaystyle x\in x}
a
=
{
x
}
{\displaystyle a=\{x\}}
x
∈
x
∩
a
{\displaystyle x\in x\cap a}
x
∩
a
≠
∅
{\displaystyle x\cap a\neq \emptyset }
x
{\displaystyle x}
a
{\displaystyle a}
x
∉
x
{\displaystyle x\notin x}
⋯
∈
x
n
+
1
∈
x
n
∈
⋯
∈
x
1
∈
x
0
.
{\displaystyle \cdots \in x_{n+1}\in x_{n}\in \cdots \in x_{1}\in x_{0}.}
ゲーデルは、自身の1940年のモノグラフで、集合ではなくクラスに関して正則性公理を述べた。これは1938年の講義に基づいたものである。
[26] 1939年、ゲーデルは集合の正則性公理がクラスの正則性公理を含意することを証明した。
[27] クラス存在定理 [ 編集 ]
クラス存在定理 ―
ϕ
(
x
1
,
…
,
x
n
,
Y
1
,
…
,
Y
m
)
{\displaystyle \phi (x_{1},\dots ,x_{n},Y_{1},\dots ,Y_{m})}
x
1
,
…
,
x
n
,
Y
1
,
…
,
Y
m
{\displaystyle x_{1},\dots ,x_{n},Y_{1},\dots ,Y_{m}}
自由変数 をもたないものとする（必ずしも
x
1
,
…
,
x
n
,
Y
1
,
…
,
Y
m
{\displaystyle x_{1},\dots ,x_{n},Y_{1},\dots ,Y_{m}}
Y
1
,
…
,
Y
m
{\displaystyle Y_{1},\dots ,Y_{m}}
n
{\displaystyle n}
A
{\displaystyle A}
∀
x
1
⋯
∀
x
n
[
(
x
1
,
…
,
x
n
)
∈
A
⟺
ϕ
(
x
1
,
…
,
x
n
,
Y
1
,
…
,
Y
m
)
]
.
{\displaystyle \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
{\displaystyle A}
は
{
(
x
1
,
…
,
x
n
)
:
ϕ
(
x
1
,
…
,
x
n
,
Y
1
,
…
,
Y
m
)
}
{\displaystyle \{(x_{1},\dots ,x_{n}):\phi (x_{1},\dots ,x_{n},Y_{1},\dots ,Y_{m})\}}
で表すことができる。
[注釈 7]
この定理の証明は 2 ステップからなる：
与えられた論理式
ϕ
{\displaystyle \phi }
帰納 部分を簡略化する等価な （英語版 ）
¬
{\displaystyle \neg }
∧
{\displaystyle \land }
∃
{\displaystyle \exists }
変換後の論理式に対して、クラス存在定理を帰納的に証明する。変換後の論理式の構造を用い、クラス存在公理から論理式を満たす唯一の
n
{\displaystyle n}
変換規則. 以下の規則 1 と 2 において、
Δ
{\displaystyle \Delta }
Γ
{\displaystyle \Gamma }
∈
{\displaystyle \in }
z
i
{\displaystyle z_{i}}
i
{\displaystyle i}
¬
{\displaystyle \neg }
∧
{\displaystyle \land }
∃
{\displaystyle \exists }
∈
{\displaystyle \in }
∈
{\displaystyle \in }
Y
k
{\displaystyle Y_{k}}
Y
k
∈
Γ
{\displaystyle \,Y_{k}\in \Gamma }
∃
z
i
(
z
i
=
Y
k
∧
z
i
∈
Γ
)
{\displaystyle \exists z_{i}(z_{i}=Y_{k}\,\land \,z_{i}\in \Gamma )}
外延性公理を用いて、
Δ
=
Γ
{\displaystyle \Delta =\Gamma }
∀
z
i
(
z
i
∈
Δ
⟺
z
i
∈
Γ
)
{\displaystyle \forall z_{i}(z_{i}\in \Delta \iff z_{i}\in \Gamma )}
論理的同一性を用いて、
∨
,
⟹
,
⟺
,
{\displaystyle \lor ,\implies ,\iff ,}
∀
{\displaystyle \forall }
¬
,
∧
,
∃
{\displaystyle \neg ,\land ,\exists }
変換規則：束縛変数 . 例 1の合成関数論理式について、集合の自由変数を
x
1
{\displaystyle x_{1}}
x
2
{\displaystyle x_{2}}
∃
t
[
(
x
1
,
t
)
∈
F
∧
(
t
,
x
2
)
∈
G
]
{\displaystyle \exists t[(x_{1},t)\in F\,\land \,(t,x_{2})\in G]}
(
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}}
論理式に
x
1
,
…
,
x
n
{\displaystyle x_{1},\dots ,x_{n}}
q
{\displaystyle q}
x
n
+
q
{\displaystyle x_{n+q}}
(量化子)ネスト深さ
q
{\displaystyle q}
例 2:
{
∅
,
{
∅
,
…
}
,
…
}
{\displaystyle \{\emptyset ,\{\emptyset ,\dots \},\dots \}}
ϕ
(
x
1
)
{\displaystyle \phi (x_{1})}
∅
{\displaystyle \emptyset }
∅
{\displaystyle \emptyset }
{
∅
,
{
∅
,
a
,
b
,
c
}
,
d
,
e
}
{\displaystyle \{\emptyset ,\{\emptyset ,a,b,c\},d,e\}}
a
,
b
,
c
,
d
,
e
{\displaystyle a,b,c,d,e}
ϕ
(
x
1
)
=
∃
u
[
u
∈
x
1
∧
¬
∃
v
(
v
∈
u
)
]
∧
∃
w
(
w
∈
x
1
∧
∃
y
[
(
y
∈
w
∧
¬
∃
z
(
z
∈
y
)
]
)
ϕ
r
(
x
1
)
=
∃
x
2
[
x
2
∈
x
1
∧
¬
∃
x
3
(
x
3
∈
x
2
)
]
∧
∃
x
2
(
x
2
∈
x
1
∧
∃
x
3
[
(
x
3
∈
x
2
∧
¬
∃
x
4
(
x
4
∈
x
3
)
]
)
{\displaystyle {\begin{aligned}\phi (x_{1})\,&=\,\exists u\;\,[\,u\in x_{1}\,\land \,\neg \exists v\;\,(\;v\,\in \,u\,)]\,\land \,\,\exists w\;{\bigl (}w\in x_{1}\,\land \,\exists y\;\,[(\;y\,\in w\;\land \;\neg \exists z\;\,(\;z\,\in \,y\,)]{\bigr )}\\\phi _{r}(x_{1})\,&=\,\exists x_{2}[x_{2}\!\in \!x_{1}\,\land \,\neg \exists x_{3}(x_{3}\!\in \!x_{2})]\,\land \,\,\exists x_{2}{\bigl (}x_{2}\!\in \!x_{1}\,\land \,\exists x_{3}[(x_{3}\!\in \!x_{2}\,\land \,\neg \exists x_{4}(x_{4}\!\in \!x_{3})]{\bigr )}\end{aligned}}}
x
1
{\displaystyle x_{1}}
n
=
1
{\displaystyle n=1}
x
3
{\displaystyle x_{3}}
x
3
∈
x
2
{\displaystyle x_{3}\in x_{2}}
n
+
q
=
1
+
2
=
3
{\displaystyle n+q=1+2=3}
x
3
{\displaystyle x_{3}}
クラス存在定理の証明. 証明は与えられた論理式に変換規則を適用して、論理式を変換することから始める。この論理式は与えられた論理式と等価であるので、変換済みの論理式を証明すればクラス存在定理の証明が完了する。
変換後の論理式に対するクラス存在定理の証明 —
拡大の補題 ―
1
≤
i
<
j
≤
n
{\displaystyle 1\leq i<j\leq n}
P
{\displaystyle P}
R
(
x
i
,
x
j
)
.
{\displaystyle R(x_{i},x_{j}).}
(
x
i
,
x
j
)
{\displaystyle (x_{i},x_{j})}
P
⊇
{
(
x
i
,
x
j
)
:
R
(
x
i
,
x
j
)
}
{\displaystyle P\supseteq \{(x_{i},x_{j}):R(x_{i},x_{j})\}}
P
{\displaystyle P}
R
(
x
i
,
x
j
)
{\displaystyle R(x_{i},x_{j})}
n
{\displaystyle n}
Q
{\displaystyle Q}
Q
=
{
(
x
1
,
…
,
x
n
)
:
R
(
x
i
,
x
j
)
}
{\displaystyle Q=\{(x_{1},\ldots ,x_{n}):R(x_{i},x_{j})\}}
証明：
i
=
1
{\displaystyle i=1}
P
1
=
P
{\displaystyle P_{1}=P}
i
>
1
{\displaystyle i>1}
x
i
{\displaystyle x_{i}}
組の補題 の言明 1 を
P
{\displaystyle P}
z
=
(
x
1
,
…
,
x
i
−
1
)
{\displaystyle z=(x_{1},\dots ,x_{i-1})}
R
(
x
i
,
x
j
)
{\displaystyle R(x_{i},x_{j})}
(
i
+
1
)
{\displaystyle (i+1)}
(
(
x
1
,
…
,
x
i
−
1
)
,
x
i
,
x
j
)
=
(
x
1
,
…
,
x
i
−
1
,
x
i
,
x
j
)
{\displaystyle ((x_{1},\dots ,x_{i-1}),x_{i},x_{j})=(x_{1},\dots ,x_{i-1},x_{i},x_{j})}
P
1
{\displaystyle P_{1}}
j
=
i
+
1
{\displaystyle j=i+1}
P
2
=
P
1
{\displaystyle P_{2}=P_{1}}
j
>
i
+
1
{\displaystyle j>i+1}
x
i
{\displaystyle x_{i}}
x
j
{\displaystyle x_{j}}
x
i
+
1
,
…
,
x
j
−
1
{\displaystyle x_{i+1},\dots ,x_{j-1}}
R
(
x
i
,
x
j
)
.
{\displaystyle R(x_{i},x_{j}).}
j
{\displaystyle j}
(
(
(
⋯
(
(
x
1
,
…
,
x
i
)
,
x
i
+
1
)
,
⋯
)
,
x
j
−
1
)
,
x
j
)
=
(
x
1
,
…
,
x
j
)
{\displaystyle (((\cdots ((x_{1},\dots ,x_{i}),x_{i+1}),\cdots ),x_{j-1}),x_{j})=(x_{1},\dots ,x_{j})}
P
2
{\displaystyle P_{2}}
j
=
n
{\displaystyle j=n}
P
3
=
P
2
{\displaystyle P_{3}=P_{2}}
j
<
n
{\displaystyle j<n}
x
j
{\displaystyle x_{j}}
x
j
+
1
,
…
,
x
n
{\displaystyle x_{j+1},\dots ,x_{n}}
R
(
x
i
,
x
j
)
.
{\displaystyle R(x_{i},x_{j}).}
n
{\displaystyle n}
(
(
⋯
(
(
x
1
,
…
,
x
j
)
,
x
j
+
1
)
,
⋯
)
,
x
n
)
=
(
x
1
,
…
,
x
n
)
{\displaystyle ((\cdots ((x_{1},\dots ,x_{j}),x_{j+1}),\cdots ),x_{n})=(x_{1},\dots ,x_{n})}
P
3
{\displaystyle P_{3}}
Q
=
P
3
∩
V
n
{\displaystyle Q=P_{3}\cap V^{n}}
Q
{\displaystyle Q}
R
(
x
i
,
x
j
)
.
{\displaystyle R(x_{i},x_{j}).}
n
{\displaystyle n}
変換後の論理式に対するクラス存在定理 ―
ϕ
(
x
1
,
…
,
x
n
,
Y
1
,
…
,
Y
m
)
{\displaystyle \phi (x_{1},\ldots ,x_{n},Y_{1},\ldots ,Y_{m})}
x
1
,
…
,
x
n
,
Y
1
,
…
,
Y
m
{\displaystyle x_{1},\ldots ,x_{n},Y_{1},\ldots ,Y_{m}}
∈
{\displaystyle \in }
¬
{\displaystyle \neg }
∧
{\displaystyle \land }
∃
{\displaystyle \exists }
Y
k
{\displaystyle Y_{k}}
Y
k
{\displaystyle Y_{k}}
∈
{\displaystyle \in }
集合変数
x
n
+
q
{\displaystyle x_{n+q}}
q
{\displaystyle q}
すると、すべての
Y
1
,
…
,
Y
m
{\displaystyle Y_{1},\dots ,Y_{m}}
n
{\displaystyle n}
A
{\displaystyle A}
∀
x
1
⋯
∀
x
n
[
(
x
1
,
…
,
x
n
)
∈
A
⟺
ϕ
(
x
1
,
…
,
x
n
,
Y
1
,
…
,
Y
m
)
]
.
{\displaystyle \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})].}
証明：基礎ステップ：
ϕ
{\displaystyle \phi }
ϕ
{\displaystyle \phi }
x
i
∈
x
j
{\displaystyle x_{i}\in x_{j}}
x
i
∈
Y
k
{\displaystyle x_{i}\in Y_{k}}
Case 1:
ϕ
{\displaystyle \phi }
x
i
∈
x
j
{\displaystyle x_{i}\in x_{j}}
x
i
∈
x
j
.
{\displaystyle x_{i}\in x_{j}.}
n
{\displaystyle n}
E
i
,
j
,
n
=
{
(
x
1
,
…
,
x
n
)
:
x
i
∈
x
j
}
{\displaystyle E_{i,j,n}=\{(x_{1},\ldots ,x_{n}):x_{i}\in x_{j}\}}
Case a:
ϕ
{\displaystyle \phi }
x
i
∈
x
j
{\displaystyle x_{i}\in x_{j}}
i
<
j
{\displaystyle i<j}
x
i
∈
x
j
{\displaystyle x_{i}\in x_{j}}
(
x
i
,
x
j
)
{\displaystyle (x_{i},x_{j})}
P
{\displaystyle P}
P
{\displaystyle P}
E
i
,
j
,
n
=
{
(
x
1
,
…
,
x
n
)
:
x
i
∈
x
j
}
{\displaystyle E_{i,j,n}=\{(x_{1},\ldots ,x_{n}):x_{i}\in x_{j}\}}
Case b:
ϕ
{\displaystyle \phi }
x
i
∈
x
j
{\displaystyle x_{i}\in x_{j}}
i
>
j
{\displaystyle i>j}
x
i
∈
x
j
{\displaystyle x_{i}\in x_{j}}
(
x
i
,
x
j
)
{\displaystyle (x_{i},x_{j})}
P
{\displaystyle P}
P
{\displaystyle P}
x
i
∈
x
j
{\displaystyle x_{i}\in x_{j}}
(
x
j
,
x
i
)
{\displaystyle (x_{j},x_{i})}
P
′
{\displaystyle P'}
P
′
{\displaystyle P'}
E
i
,
j
,
n
=
{
(
x
1
,
…
,
x
n
)
:
x
i
∈
x
j
}
{\displaystyle E_{i,j,n}=\{(x_{1},\ldots ,x_{n}):x_{i}\in x_{j}\}}
Case c:
ϕ
{\displaystyle \phi }
x
i
∈
x
j
{\displaystyle x_{i}\in x_{j}}
i
=
j
{\displaystyle i=j}
正則性の公理 よりこの論理式は偽であるため、これを満たす
n
{\displaystyle n}
E
i
,
j
,
n
=
∅
{\displaystyle E_{i,j,n}=\emptyset }
Case 2:
ϕ
{\displaystyle \phi }
x
i
∈
Y
k
{\displaystyle x_{i}\in Y_{k}}
x
i
∈
Y
k
.
{\displaystyle x_{i}\in Y_{k}.}
n
{\displaystyle n}
E
i
,
Y
k
,
n
=
{
(
x
1
,
…
,
x
n
)
:
x
i
∈
Y
k
}
{\displaystyle E_{i,Y_{k},n}=\{(x_{1},\ldots ,x_{n}):x_{i}\in Y_{k}\}}
Case a:
ϕ
{\displaystyle \phi }
x
i
∈
Y
k
{\displaystyle x_{i}\in Y_{k}}
i
<
n
{\displaystyle i<n}
V
{\displaystyle V}
Y
k
{\displaystyle Y_{k}}
P
=
Y
k
×
V
=
{
(
x
i
,
x
i
+
1
)
:
x
i
∈
Y
k
}
{\displaystyle P=Y_{k}\times V=\{(x_{i},x_{i+1}):x_{i}\in Y_{k}\}}
P
{\displaystyle P}
E
i
,
Y
k
,
n
=
{
(
x
1
,
…
,
x
n
)
:
x
i
∈
Y
k
}
{\displaystyle E_{i,Y_{k},n}=\{(x_{1},\ldots ,x_{n}):x_{i}\in Y_{k}\}}
Case b:
ϕ
{\displaystyle \phi }
x
i
∈
Y
k
{\displaystyle x_{i}\in Y_{k}}
i
=
n
>
1
{\displaystyle i=n>1}
V
{\displaystyle V}
Y
k
{\displaystyle Y_{k}}
P
=
Y
k
×
V
=
{
(
x
i
,
x
i
−
1
)
:
x
i
∈
Y
k
}
{\displaystyle P=Y_{k}\times V=\{(x_{i},x_{i-1}):x_{i}\in Y_{k}\}}
P
{\displaystyle P}
P
′
=
V
×
Y
k
=
{
(
x
i
−
1
,
x
i
)
:
x
i
∈
Y
k
}
{\displaystyle P'=V\times Y_{k}=\{(x_{i-1},x_{i}):x_{i}\in Y_{k}\}}
P
′
{\displaystyle P'}
E
i
,
Y
k
,
n
=
{
(
x
1
,
…
,
x
n
)
:
x
i
∈
Y
k
}
{\displaystyle E_{i,Y_{k},n}=\{(x_{1},\ldots ,x_{n}):x_{i}\in Y_{k}\}}
Case c:
ϕ
{\displaystyle \phi }
x
i
∈
Y
k
{\displaystyle x_{i}\in Y_{k}}
i
=
n
=
1
{\displaystyle i=n=1}
E
i
,
Y
k
,
n
=
Y
k
{\displaystyle E_{i,Y_{k},n}=Y_{k}}
帰納ステップ：
ϕ
{\displaystyle \phi }
k
(
>
0
)
{\displaystyle k(>0)}
k
{\displaystyle k}
ψ
{\displaystyle \psi }
k
{\displaystyle k}
ϕ
{\displaystyle \phi }
Y
1
,
…
,
Y
m
{\displaystyle Y_{1},\dots ,Y_{m}}
Y
→
{\displaystyle {\vec {Y}}}
ϕ
(
x
1
,
…
,
x
n
,
Y
1
,
…
,
Y
m
)
{\displaystyle \phi (x_{1},\dots ,x_{n},Y_{1},\dots ,Y_{m})}
ϕ
(
x
1
,
…
,
x
n
,
Y
→
)
{\displaystyle \phi (x_{1},\dots ,x_{n},{\vec {Y}})}
Case 1:
ϕ
(
x
1
,
…
,
x
n
,
Y
→
)
=
¬
ψ
(
x
1
,
…
,
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}
(
x
1
,
…
,
x
n
)
∈
A
⟺
ψ
(
x
1
,
…
,
x
n
,
Y
→
)
.
{\displaystyle \quad (x_{1},\ldots ,x_{n})\in A\iff \psi (x_{1},\ldots ,x_{n},{\vec {Y}}).}
補修号の公理より、
∀
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}}
の相対補集合である
[注釈 5] 。すると、外延性の公理から
∁
V
n
A
{\displaystyle \complement _{V^{n}}A}
は以下を満たす
n
{\displaystyle n}
-組の唯一のクラスである：
(
x
1
,
…
,
x
n
)
∈
∁
V
n
A
⟺
¬
[
(
x
1
,
…
,
x
n
)
∈
A
]
⟺
¬
ψ
(
x
1
,
…
,
x
n
,
Y
→
)
⟺
ϕ
(
x
1
,
…
,
x
n
,
Y
→
)
.
{\displaystyle {\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:
ϕ
(
x
1
,
…
,
x
n
,
Y
→
)
=
ψ
1
(
x
1
,
…
,
x
n
,
Y
→
)
∧
ψ
2
(
x
1
,
…
,
x
n
,
Y
→
)
{\displaystyle \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}})}
ψ
1
{\displaystyle \psi _{1}}
ψ
2
{\displaystyle \psi _{2}}
k
{\displaystyle k}
n
{\displaystyle n}
A
{\displaystyle A}
(
x
1
,
…
,
x
n
)
∈
A
1
⟺
ψ
1
(
x
1
,
…
,
x
n
,
Y
→
)
.
(
x
1
,
…
,
x
n
)
∈
A
2
⟺
ψ
2
(
x
1
,
…
,
x
n
,
Y
→
)
.
{\displaystyle {\begin{aligned}\quad &(x_{1},\ldots ,x_{n})\in A_{1}\iff \psi _{1}(x_{1},\ldots ,x_{n},{\vec {Y}}).\\&(x_{1},\ldots ,x_{n})\in A_{2}\iff \psi _{2}(x_{1},\ldots ,x_{n},{\vec {Y}}).\end{aligned}}}
共通部分および外延性の公理から、
A
1
∩
A
2
{\displaystyle A_{1}\cap A_{2}}
n
{\displaystyle n}
(
x
1
,
…
,
x
n
)
∈
A
1
∩
A
2
⟺
(
x
1
,
…
,
x
n
)
∈
A
1
∧
(
x
1
,
…
,
x
n
)
∈
A
2
⟺
ψ
1
(
x
1
,
…
,
x
n
,
Y
→
)
∧
ψ
2
(
x
1
,
…
,
x
n
,
Y
→
)
⟺
ϕ
(
x
1
,
…
,
x
n
,
Y
→
)
.
{\displaystyle {\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:
ϕ
(
x
1
,
…
,
x
n
,
Y
→
)
=
∃
x
n
+
1
ψ
(
x
1
,
…
,
x
n
,
x
n
+
1
,
Y
→
)
{\displaystyle \phi (x_{1},\ldots ,x_{n},{\vec {Y}})=\exists x_{n+1}\psi (x_{1},\ldots ,x_{n},x_{n+1},{\vec {Y}})}
ψ
{\displaystyle \psi }
ϕ
{\displaystyle \phi }
x
n
+
1
{\displaystyle x_{n+1}}
ψ
{\displaystyle \psi }
k
−
1
{\displaystyle k-1}
n
{\displaystyle n}
A
{\displaystyle A}
(
x
1
,
…
,
x
n
,
x
n
+
1
)
∈
A
⟺
ψ
(
x
1
,
…
,
x
n
,
x
n
+
1
,
Y
→
)
.
{\displaystyle \quad (x_{1},\ldots ,x_{n},x_{n+1})\in A\iff \psi (x_{1},\ldots ,x_{n},x_{n+1},{\vec {Y}}).}
領域および外延性の公理から、
D
o
m
(
A
)
{\displaystyle Dom(A)}
は以下を満たす
n
{\displaystyle n}
-組の唯一のクラスである：
[注釈 8]
(
x
1
,
…
,
x
n
)
∈
D
o
m
(
A
)
⟺
∃
x
n
+
1
[
(
(
x
1
,
…
,
x
n
)
,
x
n
+
1
)
∈
A
]
⟺
∃
x
n
+
1
[
(
x
1
,
…
,
x
n
,
x
n
+
1
)
∈
A
]
⟺
∃
x
n
+
1
ψ
(
x
1
,
…
,
x
n
,
x
n
+
1
,
Y
→
)
⟺
ϕ
(
x
1
,
…
,
x
n
,
Y
→
)
.
{\displaystyle {\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}}}
ゲーデルは、クラス存在定理は「メタ定理 （英語版 ） [30] メタ理論 の中で証明されるため、クラス存在定理は NBG に関する定理である。また、その証明は、有限個の NBG 公理を持ち出す代わりに、与えられた論理式を満たすクラスを構築するためのNBG 公理の使い方を帰納的に表現する。すべての論理式に対して、こうした表現は NBG 内の存在の構成的証明に変えられる。したがって、このメタ理論で NBG のクラス存在定理の使い方を置き換えた NBG の証明を作ることができる。
再帰 的なコンピュータプログラム で、与えられた論理式からクラスを簡単に構成することができる。このプログラムの定義はクラス存在定理の証明によらない。しかし、プログラムによって構成されるクラスが与えられた論理式を満たし、公理から構成されたかを確認するには、定理の証明が必要である。このプログラムのPascal 形式のcase文 を用いた擬似コード を以下に示す。[注釈 9]
f
u
n
c
t
i
o
n
Class
(
ϕ
,
n
)
i
n
p
u
t
:
ϕ
is a transformed formula of the form
ϕ
(
x
1
,
…
,
x
n
,
Y
1
,
…
,
Y
m
)
;
n
specifies that a class of
n
-tuples is returned.
o
u
t
p
u
t
:
class
A
of
n
-tuples satisfying
∀
x
1
⋯
∀
x
n
[
(
x
1
,
…
,
x
n
)
∈
A
⟺
ϕ
(
x
1
,
…
,
x
n
,
Y
1
,
…
,
Y
m
)
]
.
b
e
g
i
n
c
a
s
e
ϕ
o
f
x
i
∈
x
j
:
r
e
t
u
r
n
E
i
,
j
,
n
;
//
E
i
,
j
,
n
=
{
(
x
1
,
…
,
x
n
)
:
x
i
∈
x
j
}
x
i
∈
Y
k
:
r
e
t
u
r
n
E
i
,
Y
k
,
n
;
//
E
i
,
Y
k
,
n
=
{
(
x
1
,
…
,
x
n
)
:
x
i
∈
Y
k
}
¬
ψ
:
r
e
t
u
r
n
∁
V
n
Class
(
ψ
,
n
)
;
//
∁
V
n
Class
(
ψ
,
n
)
=
V
n
∖
Class
(
ψ
,
n
)
ψ
1
∧
ψ
2
:
r
e
t
u
r
n
Class
(
ψ
1
,
n
)
∩
Class
(
ψ
2
,
n
)
;
∃
x
n
+
1
(
ψ
)
:
r
e
t
u
r
n
D
o
m
(
Class
(
ψ
,
n
+
1
)
)
;
//
x
n
+
1
is free in
ψ
;
Class
(
ψ
,
n
+
1
)
// returns a class of
(
n
+
1
)
-tuples
e
n
d
e
n
d
{\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{ 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}}}
ϕ
{\displaystyle \phi }
A
=
C
l
a
s
s
(
ϕ
,
1
)
{\displaystyle A=Class(\phi ,1)}
A
{\displaystyle A}
ϕ
{\displaystyle \phi }
A
{\displaystyle A}
ϕ
{\displaystyle \phi }
ϕ
=
∃
x
2
(
x
2
∈
x
1
∧
¬
∃
x
3
(
x
3
∈
x
2
)
)
∧
∃
x
2
(
x
2
∈
x
1
∧
∃
x
3
(
x
3
∈
x
2
∧
¬
∃
x
4
(
x
4
∈
x
3
)
)
)
A
=
D
o
m
(
E
2
,
1
,
2
∩
∁
V
2
D
o
m
(
E
3
,
2
,
3
)
)
∩
D
o
m
(
E
2
,
1
,
2
∩
D
o
m
(
E
3
,
2
,
3
∩
∁
V
3
D
o
m
(
E
4
,
3
,
4
)
)
)
{\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}}}
クラス存在定理の拡張 [ 編集 ] ゲーデルはクラス存在定理を、クラスの関係 （例えば
Y
1
⊆
Y
2
{\displaystyle Y_{1}\subseteq Y_{2}}
単項関係
M
(
Y
1
)
{\displaystyle M(Y_{1})}
O
r
d
{\displaystyle Ord}
演算 （例えば
(
x
1
,
x
2
)
{\displaystyle (x_{1},x_{2})}
x
1
∩
Y
1
{\displaystyle x_{1}\cap Y_{1}}
ϕ
{\displaystyle \phi }
[32]
ϕ
{\displaystyle \phi }
クラス存在定理の仮説 を満たす等価な論理式に変換される。
以下の定義は論理式での関係、特別なクラス、演算の定義方法を特定する。
関係
R
{\displaystyle R}
R
(
Z
1
,
…
,
Z
k
)
⟺
ψ
R
(
Z
1
,
…
,
Z
k
)
.
{\displaystyle R(Z_{1},\dots ,Z_{k})\iff \psi _{R}(Z_{1},\dots ,Z_{k}).}
特別なクラス
C
{\displaystyle C}
u
∈
C
⟺
ψ
C
(
u
)
.
{\displaystyle u\in C\iff \psi _{C}(u).}
演算
P
{\displaystyle P}
u
∈
P
(
Z
1
,
…
,
Z
k
)
⟺
ψ
P
(
u
,
Z
1
,
…
,
Z
k
)
.
{\displaystyle u\in P(Z_{1},\dots ,Z_{k})\iff \psi _{P}(u,Z_{1},\dots ,Z_{k}).}
項 （en:Term (logic) ）
変数と特別なクラスは項である。
P
{\displaystyle P}
k
{\displaystyle k}
Γ
1
,
…
,
Γ
k
{\displaystyle \Gamma _{1},\dots ,\Gamma _{k}}
P
(
Γ
1
,
…
,
Γ
k
)
{\displaystyle P(\Gamma _{1},\dots ,\Gamma _{k})}
以下の変換規則は、関係、特別なクラス、演算を消去する。規則 2b, 3b, 4 をサブ論理式に適用する際は、
z
i
{\displaystyle z_{i}}
i
{\displaystyle i}
Γ
1
,
…
,
Γ
k
,
Γ
,
{\displaystyle \,\Gamma _{1},\dots ,\Gamma _{k},\Gamma ,}
Δ
{\displaystyle \Delta }
関係
R
(
Z
1
,
…
,
Z
k
)
{\displaystyle R(Z_{1},\dots ,Z_{k})}
ψ
R
(
Z
1
,
…
,
Z
k
)
{\displaystyle \psi _{R}(Z_{1},\dots ,Z_{k})}
ψ
C
(
u
)
{\displaystyle \psi _{C}(u)}
C
{\displaystyle C}
Δ
∈
C
{\displaystyle \Delta \in C}
ψ
C
(
Δ
)
{\displaystyle \psi _{C}(\Delta )}
C
∈
Δ
{\displaystyle C\in \Delta }
∃
z
i
[
z
i
=
C
∧
z
i
∈
Δ
]
{\displaystyle \exists z_{i}[z_{i}=C\land z_{i}\in \Delta ]}
ψ
P
(
u
,
Z
1
,
…
,
Z
k
)
{\displaystyle \psi _{P}(u,Z_{1},\dots ,Z_{k})}
P
(
Z
1
,
…
,
Z
k
)
{\displaystyle P(Z_{1},\dots ,Z_{k})}
Δ
∈
P
(
Γ
1
,
…
,
Γ
k
)
{\displaystyle \Delta \in P(\Gamma _{1},\dots ,\Gamma _{k})}
ψ
P
(
Δ
,
Γ
1
,
…
,
Γ
k
)
{\displaystyle \psi _{P}(\Delta ,\Gamma _{1},\dots ,\Gamma _{k})}
P
(
Γ
1
,
…
,
Γ
k
)
∈
Δ
{\displaystyle P(\Gamma _{1},\dots ,\Gamma _{k})\in \Delta }
∃
z
i
[
z
i
=
P
(
Γ
1
,
…
,
Γ
k
)
∧
z
i
∈
Δ
]
{\displaystyle \exists z_{i}[z_{i}=P(\Gamma _{1},\dots ,\Gamma _{k})\land z_{i}\in \Delta ]}
外延性の公理を用いて、
Δ
=
Γ
{\displaystyle \Delta =\Gamma }
∀
z
i
(
z
i
∈
Δ
⟺
z
i
∈
Γ
)
{\displaystyle \forall z_{i}(z_{i}\in \Delta \iff z_{i}\in \Gamma )}
例 3:
Y
1
⊆
Y
2
{\displaystyle Y_{1}\subseteq Y_{2}}
Y
1
⊆
Y
2
⟺
∀
z
1
(
z
1
∈
Y
1
⟹
z
1
∈
Y
2
)
(rule 1)
{\displaystyle Y_{1}\subseteq Y_{2}\iff \forall z_{1}(z_{1}\in Y_{1}\implies z_{1}\in Y_{2})\quad {\text{(rule 1)}}}
例 4:
x
1
∩
Y
1
∈
x
2
{\displaystyle x_{1}\cap Y_{1}\in x_{2}}
x
1
∩
Y
1
∈
x
2
⟺
∃
z
1
[
z
1
=
x
1
∩
Y
1
∧
z
1
∈
x
2
]
(rule 3b)
⟺
∃
z
1
[
∀
z
2
(
z
2
∈
z
1
⟺
z
2
∈
x
1
∩
Y
1
)
∧
z
1
∈
x
2
]
(rule 4)
⟺
∃
z
1
[
∀
z
2
(
z
2
∈
z
1
⟺
z
2
∈
x
1
∧
z
2
∈
Y
1
)
∧
z
1
∈
x
2
]
(rule 3a)
{\displaystyle {\begin{alignedat}{2}x_{1}\cap Y_{1}\in x_{2}&\iff \exists z_{1}[z_{1}=x_{1}\cap Y_{1}\,\land \,z_{1}\in x_{2}]&&{\text{(rule 3b)}}\\&\iff \exists z_{1}[\forall z_{2}(z_{2}\in z_{1}\iff z_{2}\in x_{1}\cap Y_{1})\,\land \,z_{1}\in x_{2}]&&{\text{(rule 4)}}\\&\iff \exists z_{1}[\forall z_{2}(z_{2}\in z_{1}\iff z_{2}\in x_{1}\land z_{2}\in Y_{1})\,\land \,z_{1}\in x_{2}]\quad &&{\text{(rule 3a)}}\\\end{alignedat}}}
この例は各規則がどのように演算を消去するのか示すものである。
定理 ―
ϕ
(
x
1
,
…
,
x
n
,
Y
1
,
…
,
Y
m
)
{\displaystyle \phi (x_{1},\dots ,x_{n},Y_{1},\dots ,Y_{m})}
x
1
,
…
,
x
n
,
Y
1
,
…
,
Y
m
{\displaystyle x_{1},\dots ,x_{n},Y_{1},\dots ,Y_{m}}
Y
1
,
…
,
Y
m
,
{\displaystyle Y_{1},\dots ,Y_{m},}
n
{\displaystyle n}
A
{\displaystyle A}
∀
x
1
⋯
∀
x
n
[
(
x
1
,
…
,
x
n
)
∈
A
⟺
ϕ
(
x
1
,
…
,
x
n
,
Y
1
,
…
,
Y
m
)
]
.
{\displaystyle \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})].}
[注釈 10]
証明 —
ϕ
{\displaystyle \phi }
Y
1
,
…
,
Y
m
,
{\displaystyle Y_{1},\dots ,Y_{m},}
n
{\displaystyle n}
∀
x
1
⋯
∀
x
n
[
(
x
1
,
…
,
x
n
)
∈
A
⟺
ϕ
(
x
1
,
…
,
x
n
,
Y
1
,
…
,
Y
m
)
]
.
{\displaystyle \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})].}
集合公理 [ 編集 ] クラス存在定理に必要だった対の公理と正則性公理は、上記の通り与えられている。NBG はほかに 4 つの集合公理を含む。このうち 3 つは集合に適用されるクラス演算として扱われる。
定義. 以下が成り立てば
F
{\displaystyle F}
関数 である
F
⊆
V
2
∧
∀
x
∀
y
∀
z
[
(
x
,
y
)
∈
F
∧
(
x
,
z
)
∈
F
⟹
y
=
z
]
.
{\displaystyle F\subseteq V^{2}\land \forall x\,\forall y\,\forall z\,[(x,y)\in F\,\land \,(x,z)\in F\implies y=z].}
集合論において、関数を定義する際に始域と終域を特定する必要はない（
関数（集合論） を参照）。NBG の関数の定義では、 ZFC の定義のうち、順序類の集合を順序対のクラスに一般化したものになる。
ZFC における像 、和集合 、冪集合 といった集合演算の定義もクラス演算に一般化される。
F
{\displaystyle F}
A
{\displaystyle A}
F
[
A
]
=
{
y
:
∃
x
(
x
∈
A
∧
(
x
,
y
)
∈
F
)
}
{\displaystyle F[A]=\{y:\exists x(x\in A\,\land \,(x,y)\in F)\}}
A
⊆
D
o
m
(
F
)
{\displaystyle A\subseteq Dom(F)}
A
{\displaystyle A}
∪
A
=
{
x
:
∃
y
(
x
∈
y
∧
y
∈
A
)
}
{\displaystyle \cup A=\{x:\exists y(x\in y\,\,\land \,y\in A)\}}
A
{\displaystyle A}
P
(
A
)
=
{
x
:
x
⊆
A
}
{\displaystyle {\mathcal {P}}(A)=\{x:x\subseteq A\}}
和集合 、冪集合 の各公理は、これらの操作が集合に適用したときに集合となることを含意する。[34]
置換公理.
F
{\displaystyle F}
a
{\displaystyle a}
F
{\displaystyle F}
a
{\displaystyle a}
像
F
[
a
]
{\displaystyle F[a]}
∀
F
∀
a
[
F
is a function
⟹
∃
b
∀
y
(
y
∈
b
⟺
∃
x
(
x
∈
a
∧
(
x
,
y
)
∈
F
)
)
]
.
{\displaystyle \forall F\,\forall a\,[F{\text{ is a function}}\implies \exists b\,\forall y\,(y\in b\iff \exists x(x\in a\,\land \,(x,y)\in F))].}
F
[
A
]
{\displaystyle F[A]}
A
⊆
D
o
m
(
F
)
{\displaystyle A\subseteq Dom(F)}
和集合の公理.
a
{\displaystyle a}
∪
a
{\displaystyle \cup a}
∀
a
∃
b
∀
x
[
∃
y
(
x
∈
y
∧
y
∈
a
)
⟹
x
∈
b
]
.
{\displaystyle \forall a\,\exists b\,\forall x\,[\,\exists y(x\in y\,\,\land \,y\in a)\implies x\in b\,].}
冪集合公理.
a
{\displaystyle a}
P
(
a
)
{\displaystyle {\mathcal {P}}(a)}
∀
a
∃
b
∀
x
(
x
⊆
a
⟹
x
∈
b
)
.
{\displaystyle \forall a\,\exists b\,\forall x\,(x\subseteq a\implies x\in b).}
[注釈 11]
無限公理.
a
{\displaystyle a}
x
{\displaystyle x}
x
{\displaystyle x}
y
{\displaystyle y}
a
{\displaystyle a}
y
{\displaystyle y}
a
{\displaystyle a}
無限公理と置換公理から空集合 の存在が導かれる。クラス存在公理に関する議論 において、空クラス
∅
{\displaystyle \emptyset }
∅
{\displaystyle \emptyset }
F
=
∅
{\displaystyle F=\emptyset }
a
{\displaystyle a}
F
{\displaystyle F}
a
{\displaystyle a}
∅
{\displaystyle \emptyset }
NBG の無限公理は ZFC の無限公理 から含意される：
∃
a
[
∅
∈
a
∧
∀
x
(
x
∈
a
⟹
x
∪
{
x
}
∈
a
)
]
{\displaystyle \,\exists a\,[\emptyset \in a\,\land \,\forall x(x\in a\implies x\cup \{x\}\in a)]}
x
⊂
x
∪
{
x
}
{\displaystyle x\subset x\cup \{x\}}
論理積 の第1項、つまり
∅
∈
a
{\displaystyle \emptyset \in a}
∀
x
(
x
∈
a
⟹
x
∪
{
x
}
∈
a
)
{\displaystyle \forall x(x\in a\implies x\cup \{x\}\in a)}
弱い選択公理 を参照）。[注釈 12]
大域選択公理 [ 編集 ] クラスの概念により、NBG では ZFC より強い選択公理が許容される。 選択関数は、空でない集合の集合
s
{\displaystyle s}
f
{\displaystyle f}
x
∈
s
{\displaystyle x\in s}
f
(
x
)
∈
x
{\displaystyle f(x)\in x}
G
{\displaystyle G}
x
{\displaystyle x}
G
(
x
)
∈
x
{\displaystyle G(x)\in x}
s
{\displaystyle s}
G
|
s
{\displaystyle G\vert _{s}}
G
{\displaystyle G}
s
{\displaystyle s}
制限 ）は
s
{\displaystyle s}
強制法 を使い、選択公理と NBG の大域選択公理以外のすべての公理を満たすモデルを構築することによって、大域選択公理が選択公理よりも強いことを証明した。[38] [注釈 13]
大域選択公理. すべての空でない集合から 1 つずつ元を選択できる関数が存在する。
∃
G
[
G
is a function
∧
∀
x
(
x
≠
∅
⟹
∃
y
(
y
∈
x
∧
(
x
,
y
)
∈
G
)
)
]
.
{\displaystyle \exists G\,[G{\text{ is a function}}\,\land \forall x(x\neq \emptyset \implies \exists y(y\in x\land (x,y)\in G))].}
NBG 集合論を導いた手法の変遷 フォン・ノイマンの1925年の公理系 [ 編集 ] フォン・ノイマンは自身の公理系に関する入門的な論文を1925年に発行した。1928年、彼は公理系の詳細な説明を与えた。[39] 原始概念 （英語版 ） a (x ) ではなく [a , x ] で表される関数適用である。ここで a は関数、 x は引数を表す。この演算から引数が生成される。フォン・ノイマンはクラスと集合を、A と B の2値の引数関数を使って定義した。また、 [a , x ] ≠ A ならば x ∈ a であると定義した。[1]
集合論におけるフォン・ノイマンの仕事はゲオルグ・カントール の論文やエルンスト・ツェルメロ の1908年の集合論公理 、アドルフ・フレンケル とトアルフ・スコーレム によって独立に発表された1922年のツェルメロ集合論 への批評によって広められた。 フレンケルとスコーレムはいずれも、ツェルメロの公理は集合 {Z 0 , Z 1 , Z 2 , ...} の存在を証明できないと指摘していた。ここで、 Z 0 は自然数 の集合であり、 Z n +1Z n 冪集合 である。そして彼らはそのような集合の存在を保証する置換公理を導入した。[40] [注釈 14] [42]
フォン・ノイマンはツェルメロ集合論の問題点に対処し、解決策を与えた：
順序数の理論
問題点：ツェルメロ集合論に置換公理が不足しているため、カントールの順序数 の理論をツェルメロ集合論内で展開できない。[注釈 15]
解決策： フォン・ノイマンは ∈-で整列可能な集合 を用いて順序数を定義することで、カントールの理論を復活させ、[注釈 16] 順序同型 （英語版 ） [注釈 15] [45] 集合としては大きすぎるクラスを特定する基準
問題点：ツェルメロはそのような基準を示していなかった。ツェルメロ集合論では、パラドックス を引き起こす大きなクラスが排除されていたが、フレンケルとスコーレムが指摘したような、多くの集合が除外されていた。[注釈 17]
解決策：フォン・ノイマンは基準を導入した：クラスが集合として大きすぎるのは、クラスからすべての集合のクラス V への全射 が存在するときで、かつそのときに限る。フォン・ノイマンはこのような大きなクラスを元に持つ任意のクラスを許可しないことで、集合論的パラドックスを回避できることを知っていた。この制限と彼の基準を組み合わせることで、サイズ制限公理を得た： クラス C はどのクラスの元でもないのは、 C から V への全射が存在するとき、またそのときに限る。[48] [注釈 18] 有限公理化
問題点：ツェルメロは彼の分出公理において、「定値命題関数 」の不正確な概念を用いていた。
解決策：スコーレムはのちに ZFC で用いられる分離の公理型を導入し、フレンケルは等価な解決策を用いた。[50] [注釈 19] 公理型 を除外した。これによって、フォン・ノイマンの理論は有限公理化できるようになった。[51] リチャード・モンタギュー は ZFC が有限公理化できないことを証明した。[52] 正則性公理
問題点：ツェルメロ集合論は空集合と無限集合から議論を始め、対の公理の反復、和集合、冪集合、分出公理、選択公理によって新たな集合を得る。しかし、この集合論では集合をこれらの形に制限していない。例えば、集合 x が x ∈ x を満たすような、整礎 でない集合の存在が許容される。[注釈 20]
解決策：フレンケルはこうした集合を除外するために公理を導入した。フォン・ノイマンはフレンケルの公理を分析し、「厳密な定式化」がなされていないと大雑把に指摘した：「集合に加えて ... その存在は公理に対して絶対必要になる、これ以上に集合はなく。」[54] [注釈 21] フォン・ノイマンの1929年の公理系 [ 編集 ] ジョン・フォン・ノイマン 1929年、フォン・ノイマンは NBG につながる公理を含む論文を発表した。濃度 が V より小さいどのクラスも集合であることをも含意する。フォン・ノイマンは後者について、カントール集合論を越えたと考え、以下のように結論づけた：「ゆえに（公理の）無矛盾性は、それが問題にならないかだけではなく、必須となるカントールのフレームワークを越えない集合論の公理化となるかを議論しなければならない。」[57]
フォン・ノイマンは無矛盾性の調査を1929年の公理系を導入することで始めた。この公理系はサイズ制限公理以外は1925年の公理系すべてを含む。彼は、サイズ制限公理は、そこから得られる 2 つの結果である、置換公理と選択公理に置き換えた。フォン・ノイマンの選択公理は以下の通り：「どの関係 R も、 R と同じ定義域の写像を部分クラスとしてもつ。」[58]
S をフォン・ノイマンの1929年の公理系とする。フォン・ノイマンは公理系 S + Regularity （S と正則性公理からなる）を導入し、自身の1925年の公理系が S と相対的に無矛盾 であることを示した。また、以下を証明した：
S が無矛盾であれば、 S + Regularity は無矛盾である。S + Regularity はサイズ制限公理を含意する。Since これは1925年の公理系のうち S + Regularity にない唯一のものであるため、 S + Regularity は自身の1925年の公理系の公理すべてを含意する。これらの結果は以下の内容を含意する： S が無矛盾であれば、フォン・ノイマンの1925年の公理系は無矛盾である。証明： S が無矛盾であれば、 S + Regularity は無矛盾である（結果 1）。背理法 を用いて、1925年の公理系が矛盾である、つまり1925年の公理系が矛盾を含意すると仮定する。 S + Regularity は1925年の公理系を含意する（結果 2）ので、 S + Regularity も矛盾を含意する。しかし、これは S + Regularity の無矛盾性に反する。したがって、 S が無矛盾であれば、フォン・ノイマンの1925年の公理系も無矛盾である。
S は彼の1929年の公理系であるので、フォン・ノイマンの1925年の公理系は（カントール集合論に近い）1929年のものと相対的に無矛盾である。カントール集合論と1929年の公理系の大きな違いは、クラスとフォン・ノイマンの選択公理である。公理系 S + Regularity はベルナイスとゲーデルによって修正され、NBG と等価な公理系となっていった。
ベルナイスの公理系 [ 編集 ] パウル・ベルナイス 1929年、パウル・ベルナイス はフォン・ノイマンの新しい公理系を、クラスと集合を原始概念とすることで修正し始めた。ベルナイスは自身の仕事を 1937年から1954年にかけて、一連の論文として発表した。[59]
ベルナイスは集合とクラスを2-ソート論理 で扱い、2 つの原始的帰属概念を導入した：一つは集合の関係で、もう一つはクラスの関係である。これらの原始概念によって、ベルナイスはフォン・ノイマンの1929年の公理系を簡略化した。ベルナイスはまた、その公理系に正則性公理を導入した。[61]
ゲーデルの公理系 (NBG) [ 編集 ] クルト・ゲーデル、1926年頃 1931年、ベルナイスは自身の集合論に関してクルト・ゲーデル に手紙を送った。ゲーデルはベルナイスの理論を、集合をすべてクラスで置き換え、1ソートで1つの原始概念（帰属関係）からなる理論に簡略化した。ゲーデルはまた、ベルナイスの公理のいくつかを弱め、フォン・ノイマンの選択公理を大域選択公理と等価なものに置き換えた。[62] [注釈 22] [63]
ゲーデルが自身のモノグラフの中で NBG を用いた理由はいくつか考えられる：[注釈 23]
ゲーデルは数学的理由を与えた—NBGの大域選択公理から、より強い無矛盾な定理が導かれる：「この強い形式の（選択）公理は、他の公理に対して無矛盾であれば、当然弱い形式についての無矛盾性を含意する。」[5]
ロバート・ソロヴェイ （英語版 ） モデル理論 の基本を発展させることに関連する、細部の議論を避けたかった。」[67] [注釈 24] ケネス・キューネン はゲーデルが議論を避けた理由を以下のように考えている：「L （構成可能集合 ）に関する組み合わせ論的アプローチもたくさんある、例えば ... （1940年のモノローグの中でゲーデルは）論理学者以外に説明することを試みていた。 ... このアプローチは L を扱う際に、論理の痕跡を残さないというメリットがある。」[68] チャールズ・パーソンズ (Charles Prsons) はゲーデルの選択に哲学的理由を考えた：「この（「集合の特徴」が集合論の原始概念であるという）見方は、ゲーデルの（モノグラフのように）クラス変数をフレームワークとする理論の選択に反映されているかもしれない。」[69] ゲーデルの成果と詳細な説明により、その後20年間にわたって NBG が発展した。[70] ポール・コーエン はZFの独立性を証明した。[71] 強制法 を扱うには追加の仕事が必要だったためである。[72] [73] [注釈 25] [注釈 26]
NBG, ZFC, MK [ 編集 ] NBG は論理的に ZFC と等価ではない。なぜなら、NBG の言葉は表現的であるからである。NBG ではクラスに関して表現できる一方、ZFC ではできない。しかし集合に関しては、 NBG も ZFC で同じ内容の表現を含意する。したがって、NBG は ZFC の保存拡大 である。 NBG は ZFC が含意しない定理を含意するが、 NBG は保存拡大であるため、これらの定理は真のクラスに関するものでなければならない。例えば、大域選択公理は 真のクラス V は整列可能であり、どの真のクラスも V と一対一対応することを含意するが、これは NBG の定理である。[注釈 27]
保存拡大の帰結の一つは、 ZFC と NBG が無矛盾性同値であることである。 この証明には爆発原理（矛盾 からは、何でも証明可能である）を用いる。 ZFC か NBG のいずれかが無矛盾でないと仮定する。すると無矛盾でない理論は集合に関する、矛盾 する表現 ∅ = ∅ かつ ∅ ≠ ∅ を含意する。保存拡大の特性から、もう一方の理論もこれらの表現を含意する。したがって、こちらも無矛盾ではない。ゆえに、 NBG はより表現的であるものの、 ZFC と無矛盾性同値なのである。この結果とフォン・ノイマンの1929年の相対的無矛盾性の証明を合わせると、彼の1925年の公理系にサイズ制限公理を加えたものが ZFC と無矛盾性同値であることが含意される。ZFCはカントール集合論のフレームワークに含まれるため、この事実は完全にこの強力な公理の相対的無矛盾性に関するフォン・ノイマンの懸念 を払拭するものである。
NBG は ZFC の保存拡大であるものの、定理は NBG のほうが ZFC より短くエレガントに証明可能である（逆もしかり）。この側面について知られている結果の調査結果は Pudlák 1998 を参照。
モース＝ケリー集合論 は、量化子の範囲がクラスである論理式を含む理解の公理型を有する。MK は NBG の無矛盾性を証明できるため、 NBG より強力な理論である一方、[76] ゲーデルの第二不完全定理 から NBG は NBG自身の無矛盾性を証明できない。
NBG に関する存在論 的な議論や哲学的な問題、特に ZFC と MK との比較については、Potter 2004 の Appendix C を参照。
モデル [ 編集 ] ZFC、NBG、MKは累積的階層 Vα および 構成可能階層 Lα の言葉で表現可能なモデル を持つ。 V は到達不能基数 κ を含み、 X が X ⊆ Vκ であると仮定して、 Def(X ) は X のパラメータによる1次の定義可能部分集合 のクラスを表すとする。記号として "
(
X
,
∈
)
{\displaystyle (X,\in )}
X
{\displaystyle X}
∈
{\displaystyle \in }
⊨
{\displaystyle \models }
en:Structure_(mathematical_logic)#Satisfaction_relation ）を表すものとする：
Def
(
X
)
:=
{
{
x
∣
x
∈
X
and
(
X
,
∈
)
⊨
ϕ
(
x
,
y
1
,
…
,
y
n
)
}
:
ϕ
is a first-order formula and
y
1
,
…
,
y
n
∈
X
}
.
{\displaystyle \operatorname {Def} (X):={\Bigl \{}\{x\mid x\in X{\text{ and }}(X,\in )\models \phi (x,y_{1},\ldots ,y_{n})\}:\phi {\text{ is a first-order formula and }}y_{1},\ldots ,y_{n}\in X{\Bigr \}}.}
このとき：
(V κ , ∈) と (L κ , ∈) は ZFC のモデルである。[77]
(V κ , V κ+1 , ∈) は MK のモデルであり、ここで V κ はモデルの集合からなり、 V κ+1 はモデルのクラスからなる。[78]
(V κ , Def(V κ ), ∈) は、NBG の大域選択公理を ZFC の選択公理に置き換えた、メンデルソン版の NBG のモデルである。[79] V κ , ∈) は ZFC のモデルであるため、ZFC 公理はこのモデル内で真である。特に、ZFC の選択公理が成り立つが、 NBG の大域選択公理は成り立たないかもしれない。[注釈 28]
E
{\displaystyle E}
E
=
{
x
∈
V
κ
:
(
V
κ
,
∈
)
⊨
∃
u
∃
v
[
x
=
(
u
,
v
)
∧
u
∈
v
]
}
.
{\displaystyle E=\{x\in V_{\kappa }:(V_{\kappa },\in )\models \exists u\ \exists v[x=(u,v)\land u\in v]\}.}
(L κ , L κ+ , ∈) （κ+ は κ の後続基数）は NBG のモデルである。[注釈 29] L κ , L κ+ , ∈) の中で真である。例えば、
E
{\displaystyle E}
E
=
{
x
∈
L
κ
:
(
L
κ
,
∈
)
⊨
∃
u
∃
v
[
x
=
(
u
,
v
)
∧
u
∈
v
]
}
.
{\displaystyle E=\{x\in L_{\kappa }:(L_{\kappa },\in )\models \exists u\ \exists v[x=(u,v)\land u\in v]\}.}
E ∈ 𝒫(L κ ) である。一般連続体仮説 が L の中で真というゲーデルの証明において、ゲーデルは 𝒫(L κ ) ⊆ L κ+ であることを証明した。[81] E ∈ L κ+ であり、ゆえに (L κ , L κ+ , ∈) の中で帰属公理は真である。同様に、ほかのクラス存在公理も真である。（順序数のクラスを構成可能集合に移す）ゲーデルの関数を κ 未満の順序数に制限 することによって L κ が整列可能であるため、大域選択公理は真である。したがって、 (L κ , L κ+ , ∈) は NBG のモデルである。 NBG の基本概念体系は「大きな対象」をパラドックスのおそれなしに議論する足場を提供する。例えば、圏論 の進展において、「大きい圏 」は対象 と射 が真のクラスをなす圏として定義される。一方、「小さな圏」は対象と射が集合の要素になる圏である。このように、NBG で大きな圏を扱えるため、「すべての集合の圏 」や「すべての小さい圏の圏 」をパラドックスのおそれなしに議論できる。
しかし、NBG は「すべての圏の圏」を扱えない。大きな圏は「すべての圏の圏」の要素となりえて、かつ NBG は真のクラスが何かの要素になることを許容していないためである。このような「圏」を形式的に議論するための基本概念体系の一つの拡張がクラスの集まりとしての複合体(conglomerate)である。このとき「すべての圏の圏」は、すべての圏からなる複合体を対象全体とし、A と B が対象全体を動くときに A から B へのすべての射からなる複合体[82] Muller 2001 を参照せよ。
^ なぜ「強い」かは大域選択公理 の節で説明する。
^ 歴史的な経緯として、当初は2 ソートのアプローチのほうが一般的に見られた。ベルナイスが自身の理論を展開するにあたり、以下のように述べている。「フォン・ノイマン集合論の考えによると、「集合」と「クラス」という 2 種類のものを扱う必要がある」[11]
^ ゲーデルは
(
x
1
,
x
2
,
…
,
x
n
)
=
(
x
1
,
(
x
2
,
…
,
x
n
)
)
{\displaystyle (x_{1},x_{2},\ldots ,x_{n})=(x_{1},(x_{2},\ldots ,x_{n}))}
[15] [16]
^ ベルナイスのクラス存在公理ではクラスがただ一つ定まる。ゲーデルは、ベルナイスの公理のうち3つ（共通部分、補集合、領域）を除くすべてで、双条件法 を論理包含 で置き換えることで条件を弱めた。これはクラスの順序対または 3-組のみ特定することを意味する。本節の公理はベルナイスが（順序対のクラスをただ一つ定めるという点で）強めたVの直積 以外はゲーデルのものである。ベルナイスの公理によってクラス存在定理 の証明が簡単になる。ゲーデルの公理 B6 は組の補題 の4番目として現れる。のちにベルナイスは自身の公理の一つが冗長であると気づいた。つまり、ゲーデルの公理の一つも冗長であることが導かれる。ほかの公理を使って、公理 B6 を公理 B8 から証明することができ、また B8 は B6 から証明することができ、これらは互いに冗長な公理とみなせる。[17] Théorie des ensembles de von Neumann 。
^ a b 本記事ではブルバキ の補集合記号
∁
A
{\displaystyle \complement A}
∁
X
A
=
∁
A
∩
X
{\displaystyle \complement _{X}A=\complement A\cap X}
[22]
¬
{\displaystyle \neg }
^ ゲーデルは、空集合の存在を証明する前にこの公理に言及しているため、空集合を使わずに述べている。[5]
^ 本節と次節の証明はゲーデルの証明に基づく。これはゲーデルがプリンストン高等研究所 で説明したものである。彼はそこで「数理論理学 に精通した聴衆を頼りにすることができた。」[28] [29]
n
{\displaystyle n}
V
{\displaystyle V}
束縛変数 が自由変数の番号に続く添字付き変数で置き換えられること。束縛変数は帰納部分では自由変数となるため、自由変数となるならば、もとの自由変数と同じように扱えるものとみなせる。この証明の利点の一つは、クラスの構成がその定義式の構成の反転となることを示す関数 Class の出力例である
^ この証明には一部詳細部分が抜けている。
∃
x
ϕ
(
x
)
{\displaystyle \exists x\,\phi (x)}
∃
x
[
∃
C
(
x
∈
C
)
∧
ϕ
(
x
)
]
{\displaystyle \exists x[\exists C(x\in C)\land \phi (x)]}
∃
x
[
x
∈
V
∧
ϕ
(
x
)
]
{\displaystyle \exists x[x\in V\land \phi (x)]}
∃
x
n
+
1
[
x
n
+
1
∧
…
]
{\displaystyle \exists x_{n+1}[x_{n+1}\land \dots ]}
∃
x
n
+
1
[
x
n
+
1
∈
V
∧
…
]
{\displaystyle \exists x_{n+1}[x_{n+1}\in V\land \dots ]}
^ 擬似コードで書かれた再帰的プログラムは純粋数学 でも用いられている。例えば、ハイネ・ボレルの被覆定理 や他の解析学 の定理を証明するのに用いられる。[31]
^ この定理はゲーデルの定理 M4 である。彼はまず M1 （自由クラス変数ではなく特別なクラスの記号を使ったクラス存在定理）を証明することで M4 を証明した。M1 から
ϕ
{\displaystyle \phi }
n
{\displaystyle n}
n
{\displaystyle n}
A
×
B
=
{
x
:
∃
y
∃
z
[
x
=
(
y
,
z
)
∧
y
∈
A
∧
z
∈
B
]
}
{\displaystyle A\times B=\{x:\exists y\exists z[x=(y,z)\land y\in A\land z\in B]\}}
A
×
B
{\displaystyle A\times B}
V
n
{\displaystyle V^{n}}
V
n
{\displaystyle V^{n}}
n
{\displaystyle n}
A
×
B
{\displaystyle A\times B}
V
{\displaystyle V}
[33]
^ ゲーデルはベルナイスの和集合・冪集合公理（和集合・冪集合の存在を主張する）を、和集合を含む集合と、冪集合を含む集合の存在を主張する上記の公理に弱めた。[35] [36]
^ ZFCの公理は空集合の存在が必要であるため、空集合が不要である点がNBGの公理の長所である。メンデルソンの公理系はZFCの無限公理を用いており、空集合の公理も含む。[37]
^ 整礎な
V
{\displaystyle V}
サイズ制限公理の導出 （英語版 ） Kanamori 2009 , p. 53を参照。
^ 1917年、ディミトリー・ミリマノフ （英語版 ） [41]
^ a b 1928年、フォン・ノイマンは以下のように述べた。「私の理論に密接に関係する順序数の取り扱いをツェルメロは1916年に知っており、私は個人的なやり取りで教わった。言うまでもなく、各整列集合に対してそれに類似の順序数が存在するという基礎的な定理は、置換公理が知られていなかったので厳密に証明できなかった。」[43]
^ von Neumann 1923 . フォン・ノイマンの定義は整列集合の理論でも使われている。のちに、彼の定義は現代的なものに簡略化された。つまり、順序数を ∈ で順序付けられた推移的集合 とするものである。[44] ^ 累積階層 （en:cumulative hierarchichy ）の導入後、フォン・ノイマンはツェルメロの公理が非可算無限個の継承可算集合 （英語版 ） ω+ω がツェルメロの公理を満たすという結果[46] β が α < βを含意するという結果から従う。[47] ^ フォン・ノイマンは、自身の公理を等価な関数の形で述べている。[49]
^ スコーレムのアプローチでは暗黙に自然数を使っている。なぜならば公理型の論理式が数学的帰納法 を自然数に拡張した構造的帰納法 によって構成されているからである。
^ ミリマノフは1917年に整楚集合を定義した。[53]
^ アキヒロ・カナモリ （英語版 ） [55] [56] ^ フォン・ノイマンの公理が大域選択公理を含意することの証明：
R
=
{
(
x
,
y
)
:
x
≠
∅
∧
y
∈
x
}
{\displaystyle R=\{(x,y):x\neq \emptyset \land y\in x\}}
D
o
m
(
G
)
=
D
o
m
(
R
)
{\displaystyle Dom(G)=Dom(R)}
G
⊆
R
{\displaystyle G\subseteq R}
x
{\displaystyle x}
G
(
x
)
∈
x
{\displaystyle G(x)\in x}
G
{\displaystyle G}
G
{\displaystyle G}
R
{\displaystyle R}
x
∈
D
o
m
(
R
)
{\displaystyle x\in Dom(R)}
α
(
x
)
=
least
{
α
:
∃
y
[
(
x
,
y
)
∈
R
∩
V
α
]
}
{\displaystyle \alpha (x)={\text{least}}\,\{\alpha :\exists y[(x,y)\in R\cap V_{\alpha }]\}}
V
α
{\displaystyle V_{\alpha }}
α
{\displaystyle \alpha }
階数 を持つ集合の集合である。
z
x
=
{
y
:
(
x
,
y
)
∈
R
∩
V
α
(
x
)
}
{\displaystyle z_{x}=\{y:(x,y)\in R\cap V_{\alpha (x)}\}}
F
=
{
(
x
,
G
(
z
x
)
)
:
x
∈
D
o
m
(
R
)
}
{\displaystyle F=\{(x,G(z_{x})):x\in Dom(R)\}}
F
⊆
R
{\displaystyle F\subseteq R}
D
o
m
(
F
)
=
D
o
m
(
R
)
{\displaystyle Dom(F)=Dom(R)}
^ ゲーデルは1938年の自身の相対非矛盾性定理において、フォン・ノイマンの1929年の公理を用ったほか、「T をプリンキピア・マテマティカ のシステムとすると関連する定理が成り立つ」と述べた。[64] [65] 形式体系 における定理の証明はゲーデル馴染みのないものであった。例えば、彼はプリンキピア・マテマティカ のシステムに対して不完全性定理 を証明したが、「広い形式体系で成り立つ ... 」と述べている。[66]
^ ゲーデルの非矛盾性の証明は構成可能集合 を構成する。ZFの中でこれを構成するには、いくつかのモデル理論が必要である。ゲーデルはモデル理論なしにNBGの中でこれを構成した。ゲーデルの構成については Gödel 1940 , pp. 35–46 や Cohen 1966 , pp. 99–103 を参照。
^ コーエンはZFを用いてゲーデルの相対非矛盾性定理の証明も与えた。[74]
^ この保存拡大定理は1960年代にポール・コーエン、ソール・クリプキ 、ロバート・ソロヴェイによって独立に証明された。コーエンの1966年の著書において、この定理について言及し、証明に強制法が必要であると述べている。この定理はロナルド・ジェンセン （英語版 ） [75]
^ どちらの結論も、どの真のクラスもすべての順序数のクラスと一対一対応できるという結論から導かれる。この証明の概要はKanamori 2009 , p. 53 を参照。
^ イーストンはZFCの選択公理が成り立つが大域選択公理が成り立たないメンデルソン版NBGのモデル （英語版 ）
^ 累積階層 Vκ において、 Vκ の部分集合は Vκ+1 に含まれる。構成可能階層 L κ の部分集合の生成され方は Vκ より遅いが、これは L κ の部分集合が L κ+1 ではなく L κ+ に含まれるからである。[80]
^ a b von Neumann 1925 , pp. 221–224, 226, 229; English translation: van Heijenoort 2002b , pp. 396–398, 400, 403.
^ a b c d Bernays 1937 , pp. 66–67.
^ Gödel 1940 , p. [要ページ番号 .^ Gödel 1940 , pp. 3–7.^ a b c Gödel 1940 , p. 6.
^ Gödel 1940 , p. 25.^ Gödel 1940 , pp. 35–38.^ a b "The Neumann-Bernays-Gödel axioms". Encyclopædia Britannica .
^ a b Gödel 1940 , p. 3.
^ Mendelson 1997 , pp. 225–226.^ Bernays 1937 , p. 66.^ Mendelson 1997 , p. 226.^ Gödel's axiom A3 (Gödel 1940 , p. 3).
^ Gödel's axiom A4 (Gödel 1940 , p. 3).
^ Gödel 1940 , p. 4).^ Mendelson 1997 , p. 230.^ Kanamori 2009 , p. 56; Bernays 1937 , p. 69; Gödel 1940 , pp. 5, 9; Mendelson 1997 , p. 231.^ Gödel's axiom B1 (Gödel 1940 , p. 5).
^ Gödel's axiom B2 (Gödel 1940 , p. 5).
^ Gödel's axiom B3 (Gödel 1940 , p. 5).
^ Gödel's axiom B4 (Gödel 1940 , p. 5).
^ Bourbaki 2004 , p. 71.^ Bernays' axiom b(3) (Bernays 1937 , p. 5).
^ Gödel's axiom B7 (Gödel 1940 , p. 5).
^ Gödel's axiom B8 (Gödel 1940 , p. 5).
^ Gödel 1940 , p. 6; Kanamori 2012 , p. 70.^ Kanamori 2009 , p. 57; Gödel 2003 , p. 121. 両文献ともにゲーデルの集合を含むが、カナモリのもののほうが現代的な用語を用いる分読みやすい。^ Dawson 1997 , p. 134.^ Gödel 1940 , pp. 8–11^ Gödel 1940 , p. 11.^ Gray 1991 .^ Gödel 1940 , pp. 11–13.^ Gödel 1940 , pp. 8–15.^ Gödel 1940 , pp. 16–18.^ Bernays 1941 , p. 2; Gödel 1940 , p. 5).^ Kanamori 2009 , p. 48; Gödel 2003 , pp. 104–115.^ Mendelson 1997 , pp. 228, 239.^ Easton 1964 , pp. 56a–64.^ von Neumann 1925 , von Neumann 1928 .^ Ferreirós 2007 , p. 369.^ Mirimanoff 1917 , p. 49.^ Kanamori 2012 , p. 62.^ Hallett 1984 , p. 280.^ Kunen 1980 , p. 16.^ von Neumann 1925 , p. 223 (footnote); English translation: van Heijenoort 2002b , p. 398 (footnote).^ Kanamori 2012 , p. 61^ Kunen 1980 , pp. 95–96. V β ではなく R(β) という表記になっている。^ Hallett 1984 , pp. 288–290.^ von Neumann 1925 , p. 225；英語版：van Heijenoort 2002b , p. 400.^ Fraenkel, Historical Introduction in Bernays 1991 , p. 13.
^ von Neumann 1925 , pp. 224–226; English translation: van Heijenoort 2002b , pp. 399–401.^ Montague 1961 .^ Mirimanoff 1917 , p. 41.^ von Neumann 1925 , pp. 230–232; English translation: van Heijenoort 2002b , pp. 404–405.^ Kanamori 2009 , pp. 53–54.^ Bernays 1941 , p. 6.^ von Neumann 1929 , p. 229; Ferreirós 2007 , pp. 379–380.^ Kanamori 2009 , pp. 49, 53.^ Kanamori 2009 , pp. 48, 58. ベルナイスの論文は Müller 1976 , pp. 1–117 で再発行されている.^ Bernays 1937 , p. 65.^ Kanamori 2009 , pp. 48–54.^ Kanamori 2009 , p. 56.^ Kanamori 2009 , pp. 56–58; Gödel 1940 , p. [要ページ番号 .^ Gödel 1990 , p. 26.^ Gödel 1990 , pp. 28–32.^ Gödel 1986 , p. 145.^ Solovay 1990 , p. 13.^ Kunen 1980 , p. 176.^ Gödel 1990 , p. 108, footnote i. この脚注を含む段落は、なぜゲーデルが「集合の属性」を集合論の原始概念とみなして、どのように自身の存在論 に合わせこんだかを含む。「クラスの属性」はNBGにおける「クラス」概念に対応する。^ Kanamori 2009 , p. 57.^ Cohen 1963 .^ Kanamori 2009 , p. 65: 「強制法自体は、どの形式的なクラス理論のダウングレーディングにおいてもかなりの距離を置いていた。一般に拡張させるクラスを特定しなければならないためである。」^ Cohen 1966 , pp. 107–147.^ Cohen 1966 , pp. 85–99.^ Ferreirós 2007 , pp. 381–382; Cohen 1966 , p. 77; Felgner 1971 .^ Mostowski 1950 , p. 113, footnote 11. 脚注はハオ・ワン の NQ 集合論を参照している。NQ 集合論はのちに発展し MK となった。^ Kanamori 2009b , pp. 18, 29.^ Chuaqui 1981 , p. 313 では (V κ , V κ+1 , ∈) が MKTR + AxC のモデルであることを証明している。 MKT は、選択公理や置換公理を含まない MK におけるタルスキの公理である。MKTR + AxC は MKT に置換公理と選択公理を加えたものであり（Chuaqui 1981 , pp. 4, 125）、これは MK と等価である。^ Mendelson 1997 , p. 275.^ Gödel 1940 , p. 54; Solovay 1990 , pp. 9–11.^ Gödel 1940 , p. 54.^ Adámek, Herrlich & Strecker 2004 , pp. 15–16, 40.
参考文献 [ 編集 ] Adámek, Jiří; Herrlich, Horst; Strecker, George E. (1990), Abstract and Concrete Categories (The Joy of Cats) ISBN 978-0-471-60922-3 , http://katmat.math.uni-bremen.de/acc/ Bernays, Paul (1937), “A System of Axiomatic Set Theory—Part I” , The Journal of Symbolic Logic 2 (1): 65–77, doi :10.2307/2268862 , JSTOR 2268862 , https://jstor.org/stable/2268862 Bernays, Paul (1941), “A System of Axiomatic Set Theory—Part II” , The Journal of Symbolic Logic 6 (1): 1–17, doi :10.2307/2267281 , JSTOR 2267281 , https://jstor.org/stable/2267281 Bernays, Paul (1991), Axiomatic Set Theory (2nd Revised ed.), Dover Publications, ISBN 978-0-486-66637-2 Bourbaki, Nicolas (2004), Elements of Mathematics: Theory of Sets ISBN 978-3-540-22525-6 , https://archive.org/details/springer_10.1007-978-3-642-59309-3 Chuaqui, Rolando (1981), Axiomatic Set Theory: Impredicative Theories of Classes , North-Holland, ISBN 0-444-86178-5 Cohen, Paul (1963), “The Independence of the Continuum Hypothesis” , Proceedings of the National Academy of Sciences of the United States of America 50 (6): 1143–1148, Bibcode : 1963PNAS...50.1143C , doi :10.1073/pnas.50.6.1143 , PMC 221287 , PMID 16578557 , http://www.pubmedcentral.nih.gov/articlerender.fcgi?tool=pmcentrez&artid=221287 Cohen, Paul (1966), Set Theory and the Continuum Hypothesis , W. A. Benjamin Dawson, John W. (1997), Logical dilemmas: The life and work of Kurt Gödel , Wellesley, MA: AK Peters Easton, William B. (1964), Powers of Regular Cardinals (PhD thesis), Princeton University Felgner, Ulrich (1971), “Comparison of the axioms of local and universal choice” , Fundamenta Mathematicae 71 : 43–62, doi :10.4064/fm-71-1-43-62 , http://matwbn.icm.edu.pl/ksiazki/fm/fm71/fm7113.pdf Ferreirós, José (2007), Labyrinth of Thought: A History of Set Theory and Its Role in Mathematical Thought (2nd revised ed.), Basel, Switzerland: Birkhäuser, ISBN 978-3-7643-8349-7 Gödel, Kurt (1940), The Consistency of the Axiom of Choice and of the Generalized Continuum Hypothesis with the Axioms of Set Theory (Revised ed.), Princeton University Press, ISBN 978-0-691-07927-1 Gödel, Kurt (2008), The Consistency of the Axiom of Choice and of the Generalized Continuum Hypothesis with the Axioms of Set Theory , with a foreword by Laver, Richard (Paperback ed.), Ishi Press, ISBN 978-0-923891-53-4 Gödel, Kurt (1986), Collected Works, Volume 1: Publications 1929–1936 , Oxford University Press, ISBN 978-0-19-514720-9 Gödel, Kurt (1990), Collected Works, Volume 2: Publications 1938–1974 , Oxford University Press, ISBN 978-0-19-514721-6 Gödel, Kurt (2003), Collected Works, Volume 4: Correspondence A–G , Oxford University Press, ISBN 978-0-19-850073-5 Gray, Robert (1991), “Computer programs and mathematical proofs”, The Mathematical Intelligencer 13 (4): 45–48, doi :10.1007/BF03028342 Hallett, Michael (1984), Cantorian Set Theory and Limitation of Size (Hardcover ed.), Oxford: Clarendon Press, ISBN 978-0-19-853179-1 Hallett, Michael (1986), Cantorian Set Theory and Limitation of Size (Paperback ed.), Oxford: Clarendon Press, ISBN 978-0-19-853283-5 Kanamori, Akihiro (2009b), The Higher Infinite: Large Cardinals in Set Theory from Their Beginnings , Springer, ISBN 978-3-540-88867-3 Kanamori, Akihiro (2009), “Bernays and Set Theory” , Bulletin of Symbolic Logic 15 (1): 43–69, doi :10.2178/bsl/1231081769 , JSTOR 25470304 , http://math.bu.edu/people/aki/17a.pdf Kanamori, Akihiro (2012), “In Praise of Replacement” , Bulletin of Symbolic Logic 18 (1): 46–90, doi :10.2178/bsl/1327328439 , JSTOR 41472440 , http://math.bu.edu/people/aki/20.pdf Kunen, Kenneth (1980), Set Theory: An Introduction to Independence Proofs (Hardcover ed.), North-Holland, ISBN 978-0-444-86839-8 Kunen, Kenneth (2012), Set Theory: An Introduction to Independence Proofs (Paperback ed.), North-Holland, ISBN 978-0-444-56402-3 Mendelson, Elliott (1997), An Introduction to Mathematical Logic (4th ed.), London: Chapman and Hall/CRC, ISBN 978-0-412-80830-2 relations , order theory , ordinal numbers , transfinite numbers , etc.Mirimanoff, Dmitry (1917), “Les antinomies de Russell et de Burali-Forti et le problème fondamental de la théorie des ensembles”, L'Enseignement Mathématique 19 : 37–52 Montague, Richard (1961), “Semantic Closure and Non-Finite Axiomatizability I”, in Buss, Samuel R. , Infinitistic Methods: Proceedings of the Symposium on Foundations of Mathematics , Pergamon Press, pp. 45–69 Mostowski, Andrzej (1950), “Some impredicative definitions in the axiomatic set theory” , Fundamenta Mathematicae 37 : 111–124, doi :10.4064/fm-37-1-111-124 , http://matwbn.icm.edu.pl/ksiazki/fm/fm37/fm37110.pdf Muller, F. A. (1 September 2001), “Sets, classes, and categories” , British Journal for the Philosophy of Science 52 (3): 539–73, doi :10.1093/bjps/52.3.539 , http://philsci-archive.pitt.edu/1372/1/SetClassCat.PDF Müller, Gurt, ed. (1976), Sets and Classes: On the Work of Paul Bernays , Studies in Logic and the Foundations of Mathematics Volume 84, Amsterdam: North Holland, ISBN 978-0-7204-2284-9 Potter, Michael (2004), Set Theory and Its Philosophy: A Critical Introduction (Hardcover ed.), Oxford University Press, ISBN 978-0-19-926973-0 Potter, Michael (2004p), Set Theory and Its Philosophy: A Critical Introduction (Paperback ed.), Oxford University Press, ISBN 978-0-19-927041-5 Pudlák, Pavel (1998), “The Lengths of Proofs” , in Buss, Samuel R. , Handbook of Proof Theory , Elsevier, pp. 547–637, ISBN 978-0-444-89840-1 , http://users.math.cas.cz/~pudlak/length.pdf Smullyan, Raymond M. ; Fitting, Melvin (2010) [Revised and corrected edition: first published in 1996 by Oxford University Press], Set Theory and the Continuum Problem , Dover, ISBN 978-0-486-47484-7 Solovay, Robert M. (1990), “Introductory note to 1938 , 1939 , 1939a and 1940 ”, Kurt Gödel Collected Works, Volume 2: Publications 1938–1974 , Oxford University Press, pp. 1–25, ISBN 978-0-19-514721-6 von Neumann, John (1922), “Zur Einführung der transfiniten Zahlen” , Acta Litt. Acad. Sc. Szeged X. 1 : 199–208, http://bbi-math.narod.ru/newmann/newmann.html English translation: van Heijenoort, Jean (2002a) [1967], “On the introduction of transfinite numbers” , From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931 (Fourth Printing ed.), Harvard University Press, pp. 346–354, ISBN 978-0-674-32449-7 , https://books.google.com/books?id=v4tBTBlU05sC&pg=PA346
English translation: van Heijenoort, Jean (2002b) [1967], “An axiomatization of set theory” , From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931 (Fourth Printing ed.), Harvard University Press, pp. 393–413, ISBN 978-0-674-32449-7 , https://books.google.com/books?id=v4tBTBlU05sC&pg=PA393 von Neumann, John (1925), “Eine Axiomatisierung der Mengenlehre” , Journal für die Reine und Angewandte Mathematik 154 : 219–240, http://gdz.sub.uni-goettingen.de/dms/load/img/?PPN=PPN243919689_0154&DMDID=DMDLOG_0025 von Neumann, John (1928), “Die Axiomatisierung der Mengenlehre” , Mathematische Zeitschrift 27 : 669–752, doi :10.1007/bf01171122 , http://gdz.sub.uni-goettingen.de/dms/load/img/?PPN=PPN266833020_0027&DMDID=DMDLOG_0042 von Neumann, John (1929), “Über eine Widerspruchsfreiheitsfrage in der axiomatischen Mengenlehre” , Journal für die Reine und Angewandte Mathematik 160 : 227–241, http://gdz.sub.uni-goettingen.de/dms/load/img/?PPN=PPN243919689_0160&DMDID=DMDLOG_0019 外部リンク [ 編集 ] 
![{\displaystyle \forall x_{1}\cdots \,\forall x_{n}[(x_{1},\ldots ,x_{n})\in A\iff \phi (x_{1},\ldots ,x_{n})]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0966544908f832def496cb79ceeac3a3deec676f)
![{\displaystyle \forall A\,\forall B\,[\forall x(x\in A\iff x\in B)\implies A=B]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/241eef7d867be06ecf35bcb9a4dce9da32626e88)
![{\displaystyle \forall x\,\forall y\,\exists p\,\forall z\,[z\in p\iff (z=x\,\lor \,z=y)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/43f8175b900322da6f061d58dd643352a0a5e50e)
![{\displaystyle \exists t[(x,t)\in F\,\land \,(t,y)\in G].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/53dfe627ca14a603359cd959026127bb377f4e2b)
![{\displaystyle G\circ F\,=\,\{(x,y):\exists t[(x,t)\in F\,\land \,(t,y)\in G]\}.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ccdc0eb213206411f44076e60e427b79236873e5)
![{\displaystyle x\in Dom(A)\iff \exists t[(x,t)\in A].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f1aa4ebff266ec5e2538dd6f124d750c177bbd99)
![{\displaystyle \exists E\,\forall x\,\forall y\,[(x,y)\in E\iff x\in y]\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/75b6597b3f8f7f040da8f637d9a5307597f3a1f1)
![{\displaystyle \forall A\,\forall B\,\exists C\,\forall x\,[x\in C\iff (x\in A\,\land \,x\in B)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/197b276873b716c1a83d1d94af367862900da1ea)
![{\displaystyle \forall A\,\exists B\,\forall x\,[x\in B\iff \neg (x\in A)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/9450bca22cfc5d874901ba0d44b3539147e574e0)
![{\displaystyle \forall A\,\exists B\,\forall x\,[x\in B\iff \exists y((x,y)\in A)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f22c660ba2347b6dd6014ac3a26e833bc0caedb9)
![{\displaystyle \forall A\,\exists B\,\forall u\,[u\in B\iff \exists x\,\exists y\,(u=(x,y)\land x\in A)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c2f45de53d4e2ee4c42622d59563b91a4a5dd8e7)
![{\displaystyle \forall A\,\exists B\,\forall x\,\forall y\,\forall z\,[(x,y,z)\in B\iff (y,z,x)\in A]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ecb3d73e80a870caf94253aa8afab0a8e885af66)
![{\displaystyle \forall A\,\exists B\,\forall x\,\forall y\,\forall z\,[(x,y,z)\in B\iff (x,z,y)\in A]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/1ceb9de8295c9ca52de2c8965cdc8e4dd1f72913)
![{\displaystyle \forall A\,\exists B_{1}\,\forall x\,\forall y\,\forall z\,[(z,x,y)\in B_{1}\iff (x,y)\in A]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0551e12143886cea9a751fced7944423cc218627)
![{\displaystyle \forall A\,\exists B_{2}\,\forall x\,\forall y\,\forall z\,[(x,z,y)\in B_{2}\iff (x,y)\in A]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6b6993cde8ec20c99d868ca5fd8a0b1adbda0bf4)
![{\displaystyle \forall A\,\exists B_{3}\,\forall x\,\forall y\,\forall z\,[(x,y,z)\in B_{3}\iff (x,y)\in A]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2e4d1d6722e06510dfc69706454d60d3f63c3055)
![{\displaystyle \forall A\,\exists B_{4}\,\forall x\,\forall y\,\forall z\,[(y,x)\in B_{4}\iff (x,y)\in A]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d0be69b28701384ef168ff9bfffd671d7690ad35)
![{\displaystyle \forall a\,[a\neq \emptyset \implies \exists u(u\in a\land u\cap a=\emptyset )].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/be47d555db4994e987a277a26740c151d0f0c3a6)
![{\displaystyle \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})].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/85ed8313491a2c7b4011ab9a536a751e08a96620)
![{\displaystyle \exists t[(x_{1},t)\in F\,\land \,(t,x_{2})\in G]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c8a10e3ca1610ecdc3870443122a6dd4ed196d2f)
![{\displaystyle {\begin{aligned}\phi (x_{1})\,&=\,\exists u\;\,[\,u\in x_{1}\,\land \,\neg \exists v\;\,(\;v\,\in \,u\,)]\,\land \,\,\exists w\;{\bigl (}w\in x_{1}\,\land \,\exists y\;\,[(\;y\,\in w\;\land \;\neg \exists z\;\,(\;z\,\in \,y\,)]{\bigr )}\\\phi _{r}(x_{1})\,&=\,\exists x_{2}[x_{2}\!\in \!x_{1}\,\land \,\neg \exists x_{3}(x_{3}\!\in \!x_{2})]\,\land \,\,\exists x_{2}{\bigl (}x_{2}\!\in \!x_{1}\,\land \,\exists x_{3}[(x_{3}\!\in \!x_{2}\,\land \,\neg \exists x_{4}(x_{4}\!\in \!x_{3})]{\bigr )}\end{aligned}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ab38cfea7d5044bf3535ff06bc9053ebfaf13385)
![{\displaystyle \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})].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/efbe3e28e60323770b9db02c02a02d6aaadd0a3c)
![{\displaystyle \forall u\,[u\in \complement A\iff \neg (u\in A)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d852dce658c6ce16ea5b96048721853fa96c2ff4)
![{\displaystyle {\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}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2018de32f7ba7fe495e8f566fb579619f4f0c2b5)
![{\displaystyle {\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}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d1814606d89e7d61c7a3dc3fb82b98b724275c16)
![{\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{ 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}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3288241d26bed1d0c0a421a72ec95b3d609753e2)
![{\displaystyle \exists z_{i}[z_{i}=C\land z_{i}\in \Delta ]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/35225fe3cc0ae7d215adf76237d1e0cc5da7be12)
![{\displaystyle \exists z_{i}[z_{i}=P(\Gamma _{1},\dots ,\Gamma _{k})\land z_{i}\in \Delta ]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f249e88ac6fe4af6445d43c04bca0d546d021a8f)
![{\displaystyle {\begin{alignedat}{2}x_{1}\cap Y_{1}\in x_{2}&\iff \exists z_{1}[z_{1}=x_{1}\cap Y_{1}\,\land \,z_{1}\in x_{2}]&&{\text{(rule 3b)}}\\&\iff \exists z_{1}[\forall z_{2}(z_{2}\in z_{1}\iff z_{2}\in x_{1}\cap Y_{1})\,\land \,z_{1}\in x_{2}]&&{\text{(rule 4)}}\\&\iff \exists z_{1}[\forall z_{2}(z_{2}\in z_{1}\iff z_{2}\in x_{1}\land z_{2}\in Y_{1})\,\land \,z_{1}\in x_{2}]\quad &&{\text{(rule 3a)}}\\\end{alignedat}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/16d326641c3315adaeb2b1072bc35dd50addf9fb)
![{\displaystyle F\subseteq V^{2}\land \forall x\,\forall y\,\forall z\,[(x,y)\in F\,\land \,(x,z)\in F\implies y=z].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/39e46fe8c2c518a6c07dfb3747ad4dc24f3802f4)
![{\displaystyle F[A]=\{y:\exists x(x\in A\,\land \,(x,y)\in F)\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e668be6f2fdaf58c792396c642809b66b55c9001)
![{\displaystyle F[a]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7c8e90bfcbe7e0bb619096b7c0d91b12cb7c20f4)
![{\displaystyle \forall F\,\forall a\,[F{\text{ is a function}}\implies \exists b\,\forall y\,(y\in b\iff \exists x(x\in a\,\land \,(x,y)\in F))].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7d5be626156ac915fe374ffe54da1a3a407186fa)
![{\displaystyle F[A]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/667bb1fca53d019ead801661a56c8afeeb4bef8c)
![{\displaystyle \forall a\,\exists b\,\forall x\,[\,\exists y(x\in y\,\,\land \,y\in a)\implies x\in b\,].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/bcd5515f243541353f13ac8782936e9b36dfa8f0)
![{\displaystyle \,\exists a\,[\emptyset \in a\,\land \,\forall x(x\in a\implies x\cup \{x\}\in a)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2e5bb64f8ccc5985f4ddf05a8fce0f41dca57a2a)
![{\displaystyle \exists G\,[G{\text{ is a function}}\,\land \forall x(x\neq \emptyset \implies \exists y(y\in x\land (x,y)\in G))].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/fb1b7fd53af984df9ed30029df16a95bf72f35ae)
![{\displaystyle E=\{x\in V_{\kappa }:(V_{\kappa },\in )\models \exists u\ \exists v[x=(u,v)\land u\in v]\}.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3adaeacce71ec9b637fbe8b57b3b2d277259f962)
![{\displaystyle E=\{x\in L_{\kappa }:(L_{\kappa },\in )\models \exists u\ \exists v[x=(u,v)\land u\in v]\}.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/64231382a0b2b3ae97752075dbbdc0dc52bf498e)
![{\displaystyle \exists x[\exists C(x\in C)\land \phi (x)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/56d1d59dfc8682e3901493ba4092bec0808dcb13)
![{\displaystyle \exists x[x\in V\land \phi (x)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2cd02c6410335e6e0aa7e11d96ef423db424d4d3)
![{\displaystyle \exists x_{n+1}[x_{n+1}\land \dots ]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/fbcb706d5afa593a4200e67fea72609f8f553034)
![{\displaystyle \exists x_{n+1}[x_{n+1}\in V\land \dots ]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/250f71405ab87b2c9ac8ac99c5aa30011d410f99)
![{\displaystyle A\times B=\{x:\exists y\exists z[x=(y,z)\land y\in A\land z\in B]\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/281da45a8d481e1ff92e38828a54e88b8c2438ce)
![{\displaystyle \alpha (x)={\text{least}}\,\{\alpha :\exists y[(x,y)\in R\cap V_{\alpha }]\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a52e0a6ba57a87c7cbe3869edcc8b0a94c4b0bc0)
