在NBG 下,「屬於關係」以一個雙元斷言符號
P
(
x
,
y
)
{\displaystyle P(x,\,y)}
來表示,
P
(
x
,
y
)
{\displaystyle P(x,\,y)}
通常簡記為
x
∈
y
{\displaystyle x\in y}
,並被直觀理解成「x屬於y」;類似地,
P
(
x
,
y
)
{\displaystyle P(x,\,y)}
的否定
¬
P
(
x
,
y
)
{\displaystyle \neg P(x,\,y)}
通稱被簡記為
x
∉
y
{\displaystyle x\notin y}
,並被直觀理解為「x不屬於y」。
以下都把
⊢
N
B
G
{\displaystyle \vdash _{NBG}}
簡寫為普通的
⊢
{\displaystyle \vdash }
。
本條目定理的證明會頻繁引用一階邏輯的定理,定理的代號可以參見一階邏輯#常用的推理性質 一節。
類與集合
「類」這個名詞在公理化集合論 出現之前,通常被理解為「以集合 為元素 的集合。」或是集合(如等價類 )。
但NBG 所談及的一切對象(變數和項 )都是類 。而所謂的集合,是屬於某個類的類 ,也就是說以下的合式公式 (
M
{\displaystyle {\mathcal {M}}}
來自德語 的"集合"「Menge 」)式
M
(
x
)
:=
∃
y
(
x
∈
y
)
{\displaystyle {\mathcal {M}}(x):=\exists y(x\in y)}
可直觀理解為「x是集合」,特別注意到,為了避免跟其他合式公式的變數產生混淆,
y
{\displaystyle y}
必須是展開
M
(
x
)
{\displaystyle {\mathcal {M}}(x)}
時首次出現的變數。反之合式公式
P
r
(
x
)
:=
¬
M
(
x
)
{\displaystyle {\mathcal {Pr}}(x):=\neg {\mathcal {M}}(x)}
可稱為「
x
{\displaystyle x}
是真類 (proper class )」。
子類
直觀上「x包含於y」意為「所有x的元素a都會屬於y」,以此為動機,NBG 有以下的符號簡寫
x
⊆
y
:=
∀
a
[
(
a
∈
x
)
⇒
(
a
∈
y
)
]
{\displaystyle x\subseteq y:=\forall a[\,(a\in x)\Rightarrow (a\in y)\,]}
以上可稱為「x包含於y」或「x是y的子類 (subclass )」;在
M
(
x
)
{\displaystyle {\mathcal {M}}(x)}
和
M
(
y
)
{\displaystyle {\mathcal {M}}(y)}
成立的前提下(也就是「x和y都是集合」),可稱為「x是y的子集 (subset )」。
與集合相關的量詞簡寫
仿造量詞的簡寫 ,對於任意變數
x
{\displaystyle x}
與合式公式
A
{\displaystyle {\mathcal {A}}}
,可作如下的符號定義
(
∀
M
x
)
A
:=
∀
x
[
M
(
x
)
⇒
A
]
{\displaystyle ({\forall }^{M}x){\mathcal {A}}:=\forall x[\,{\mathcal {M}}(x)\Rightarrow {\mathcal {A}}\,]}
(對所有
x
{\displaystyle x}
,
x
{\displaystyle x}
是集合則
A
{\displaystyle {\mathcal {A}}}
)
(
∃
M
x
)
A
:=
∃
x
[
M
(
x
)
∧
A
]
{\displaystyle ({\exists }^{M}x){\mathcal {A}}:=\exists x[\,{\mathcal {M}}(x)\wedge {\mathcal {A}}\,]}
(存在
x
{\displaystyle x}
不但是集合且
A
{\displaystyle {\mathcal {A}}}
)
也有書籍以小寫字母來表示被量化的集合變數[ 3] ,但考慮到一般的非邏輯數學書籍都將大小寫的差異挪作他用,為避免混淆本條目採用以上的上標表示法。
看待等號的不同方式
直觀上,兩個集合相等意為「x的元素就是y的元素」,也就是樸素集合論 的外延公理 ,換句話說,可用以下的嚴謹合式公式重寫為
∀
a
[
(
a
∈
x
)
⇔
(
a
∈
y
)
]
{\displaystyle \forall a[\,(a\in x)\Leftrightarrow (a\in y)\,]}
但一階邏輯的等號可以視為單獨的斷言符號 ,也可以視為一條複合的合式公式。具體來說,視為一個新的斷言符號
Q
(
x
,
y
)
{\displaystyle Q(x,\,y)}
並簡記為
x
=
y
{\displaystyle x=y}
的話,需在NBG 內額外添加以下的公理
(
T
′
)
{\displaystyle (T^{\prime })}
—
(
x
=
y
)
⇔
∀
a
[
(
a
∈
x
)
⇔
(
a
∈
y
)
]
{\displaystyle (x=y)\Leftrightarrow \forall a[\,(a\in x)\Leftrightarrow (a\in y)\,]}
直觀上可理解為「類x的元素就是類y的元素,等價於類x等於類y」。
但視為一條合式公式,則僅需做以下的符號定義
(
x
=
y
)
:=
∀
a
[
(
a
∈
x
)
⇔
(
a
∈
y
)
]
{\displaystyle (x=y):=\forall a[\,(a\in x)\Leftrightarrow (a\in y)\,]}
不管是何種看待方法,習慣上都會把
¬
(
x
=
y
)
{\displaystyle \neg (x=y)}
簡記成
(
x
≠
y
)
{\displaystyle (x\neq y)}
(直觀上的「不相等」)。
等號的良置
為了確保
(
x
=
y
)
{\displaystyle (x=y)}
的確符合直觀上對等號的要求,還需添加以下的公理
(
T
)
{\displaystyle (T)}
—
(
x
=
y
)
⇒
∀
z
[
(
x
∈
z
)
⇔
(
y
∈
z
)
]
{\displaystyle (x=y)\Rightarrow \forall z[\,(x\in z)\Leftrightarrow (y\in z)\,]}
直觀上,這個公理確保「x等於y,則x屬於z等同於y屬於z」。
這樣,以下的元定理 就確保了如此定義的等號是「成功的」。
元定理 — NBG 是帶相等符號
(
x
=
y
)
{\displaystyle (x=y)}
的一階邏輯 理論
證明
以下的證明會逐條檢驗等式定理一節 所條列的定義
(E1):
(
x
=
x
)
{\displaystyle (x=x)}
展開來是(或等價於)
∀
a
[
(
a
∈
x
)
⇔
(
a
∈
x
)
]
{\displaystyle \forall a[\,(a\in x)\Leftrightarrow (a\in x)\,]}
那考慮到恆等關係 和(AND) 有
⊢
(
a
∈
x
)
⇔
(
a
∈
x
)
{\displaystyle \vdash (a\in x)\Leftrightarrow (a\in x)}
那再套用(GEN) ,就會有
⊢
∀
a
[
(
a
∈
x
)
⇔
(
a
∈
x
)
]
{\displaystyle \vdash \forall a[\,(a\in x)\Leftrightarrow (a\in x)\,]}
所以(E1)得證。
(E2):
因為目前的NBG 理論內沒有任何函數符號 ,所以對變數
x
{\displaystyle x}
來說,NBG 的原子公式 只有
(
x
∈
z
)
{\displaystyle (x\in z)}
和
(
z
∈
x
)
{\displaystyle (z\in x)}
兩種可能,這樣的話,(E2)等同於要求以下兩式是NBG 的定理
(1)
(
x
=
y
)
⇒
[
(
x
∈
z
)
⇒
(
y
∈
z
)
]
{\displaystyle (x=y)\Rightarrow [\,(x\in z)\Rightarrow (y\in z)\,]}
(2)
(
x
=
y
)
⇒
[
(
z
∈
x
)
⇒
(
z
∈
y
)
]
{\displaystyle (x=y)\Rightarrow [\,(z\in x)\Rightarrow (z\in y)\,]}
但依據量詞公理 (A4),(1)可從本節一開始添加的公理(T)所推出;類似地,把
(
x
=
y
)
{\displaystyle (x=y)}
視為斷言符號時,(2)都可以從(T')配合(A4)推出;若把
(
x
=
y
)
{\displaystyle (x=y)}
視為合式公式的簡寫,(2)也可以用
(
x
=
y
)
{\displaystyle (x=y)}
的定義配上(A4)推出。
(E3):
本條定義要求以下的合式公式為NBG 的定理
(
x
=
y
)
⇒
(
y
=
x
)
{\displaystyle (x=y)\Rightarrow (y=x)}
從且的交換性 有
⊢
(
∀
z
)
[
(
z
∈
x
)
⇔
(
z
∈
y
)
]
⇒
(
∀
z
)
[
(
z
∈
y
)
⇔
(
z
∈
x
)
]
{\displaystyle \vdash (\forall z)[(z\in x)\Leftrightarrow (z\in y)]\Rightarrow (\forall z)[(z\in y)\Leftrightarrow (z\in x)]}
對上式使用(AND) 和(D1) 就有
(
x
=
y
)
⊢
(
∀
z
)
[
(
z
∈
y
)
⇔
(
z
∈
x
)
]
{\displaystyle (x=y)\vdash (\forall z)[(z\in y)\Leftrightarrow (z\in x)]}
再對上面式使用(AND) 和(D1) 又有
(
x
=
y
)
⊢
(
y
=
x
)
{\displaystyle (x=y)\vdash (y=x)}
所以(E3)的確是NBG 的定理。
綜上所述,定理得證。
◻
{\displaystyle \Box }
真子類
在定義「相等」以後,可以把「相等的類」排除出子類的定義中,換句話說,NBG 有以下的符號定義
x
⊂
y
:=
(
x
⊆
y
)
∧
(
x
≠
y
)
{\displaystyle x\subset y:=(x\subseteq y)\wedge (x\neq y)}
可直觀理解為「x是y的真子類 (proper subclass ),定義為x包含於y且x不等於y」;在
M
(
x
)
{\displaystyle {\mathcal {M}}(x)}
和
M
(
y
)
{\displaystyle {\mathcal {M}}(y)}
成立的前提下(也就是「x和y都是集合」),可稱為「x是y的真子集 (proper subset )」。
外延定理
為以下的定理可直觀理解為「x等於y等價於,對所有集合z,z屬於x等價於z屬於y」,也就是說,等於的定義可以「限縮」成元素為集合的狀況。
外延定理 —
⊢
(
x
=
y
)
⇔
(
∀
M
z
)
[
(
z
∈
x
)
⇔
(
z
∈
y
)
]
{\displaystyle \vdash (x=y)\Leftrightarrow (\forall ^{M}z)[\,(z\in x)\Leftrightarrow (z\in y)\,]}
證明
以下取一個不曾出現的變數
t
{\displaystyle t}
來展開
M
(
z
)
{\displaystyle {\mathcal {M}}(z)}
(
⇒
{\displaystyle \Rightarrow }
)
∀
z
(
z
∈
x
⇔
z
∈
y
)
⊢
∀
z
{
∃
t
(
z
∈
t
)
⇒
[
(
z
∈
x
)
⇔
(
z
∈
y
)
]
}
{\displaystyle \forall z(z\in x\Leftrightarrow z\in y)\vdash \forall z\{\exists t(z\in t)\Rightarrow [(z\in x)\Leftrightarrow (z\in y)]\}}
(1)
∀
z
(
z
∈
x
⇔
z
∈
y
)
{\displaystyle \forall z(z\in x\Leftrightarrow z\in y)}
(Hyp)
(2)
z
∈
x
⇔
z
∈
y
{\displaystyle z\in x\Leftrightarrow z\in y}
(MP with 1, A4)
(3)
∃
t
(
z
∈
t
)
⇒
[
(
z
∈
x
)
⇔
(
z
∈
y
)
]
{\displaystyle \exists t(z\in t)\Rightarrow [(z\in x)\Leftrightarrow (z\in y)]}
(MP with 2, A1)
(4)
∀
z
{
∃
t
(
z
∈
t
)
⇒
[
(
z
∈
x
)
⇔
(
z
∈
y
)
]
}
{\displaystyle \forall z\{\exists t(z\in t)\Rightarrow [(z\in x)\Leftrightarrow (z\in y)]\}}
(GEN with 3)
(
⇐
{\displaystyle \Leftarrow }
)
∀
z
{
M
(
z
)
⇒
[
(
z
∈
x
)
⇔
(
z
∈
y
)
]
}
⊢
∀
z
(
z
∈
x
⇔
z
∈
y
)
{\displaystyle \forall z\{{\mathcal {M}}(z)\Rightarrow [(z\in x)\Leftrightarrow (z\in y)]\}\vdash \forall z(z\in x\Leftrightarrow z\in y)}
A
:=
(
z
∈
x
)
⇔
(
z
∈
y
)
{\displaystyle {\mathcal {A}}:=(z\in x)\Leftrightarrow (z\in y)}
(1)
∀
z
[
∃
t
(
z
∈
t
)
⇒
A
]
{\displaystyle \forall z[\exists t(z\in t)\Rightarrow {\mathcal {A}}]}
(Hyp)
(2)
∃
t
(
z
∈
t
)
⇒
A
{\displaystyle \exists t(z\in t)\Rightarrow {\mathcal {A}}}
(MP with A4, 1)
(3)
¬
A
⇒
∀
t
[
¬
(
z
∈
t
)
]
{\displaystyle \neg {\mathcal {A}}\Rightarrow \forall t[\neg (z\in t)]}
(MP with T, 2)
(4)
¬
A
⇒
[
¬
(
z
∈
t
)
]
{\displaystyle \neg {\mathcal {A}}\Rightarrow [\neg (z\in t)]}
(D1, with A4, 3)
(5)
(
z
∈
t
)
⇒
[
(
z
∈
x
)
⇔
(
z
∈
y
)
]
{\displaystyle (z\in t)\Rightarrow [(z\in x)\Leftrightarrow (z\in y)]}
(MP with T, 4)
(6)
∀
t
{
(
z
∈
t
)
⇒
[
(
z
∈
x
)
⇔
(
z
∈
y
)
]
}
{\displaystyle \forall t\{(z\in t)\Rightarrow [(z\in x)\Leftrightarrow (z\in y)]\}}
(GEN with 5)
(7)
(
z
∈
x
)
⇒
[
(
z
∈
x
)
⇔
(
z
∈
y
)
]
{\displaystyle (z\in x)\Rightarrow [(z\in x)\Leftrightarrow (z\in y)]}
(MP with A4, 6)
(8)
(
z
∈
y
)
⇒
[
(
z
∈
x
)
⇔
(
z
∈
y
)
]
{\displaystyle (z\in y)\Rightarrow [(z\in x)\Leftrightarrow (z\in y)]}
(MP with A4, 6)
(9)
(
z
∈
x
)
⇒
[
(
z
∈
x
)
⇒
(
z
∈
y
)
]
{\displaystyle (z\in x)\Rightarrow [(z\in x)\Rightarrow (z\in y)]}
(D1 with AND, 7)
(10)
(
z
∈
y
)
⇒
[
(
z
∈
y
)
⇒
(
z
∈
x
)
]
{\displaystyle (z\in y)\Rightarrow [(z\in y)\Rightarrow (z\in x)]}
(D1 with AND, 8)
(11)
(
z
∈
x
)
⇒
(
z
∈
y
)
{\displaystyle (z\in x)\Rightarrow (z\in y)}
(MP twice with A2, I, 9)
(12)
(
z
∈
y
)
⇒
(
z
∈
x
)
{\displaystyle (z\in y)\Rightarrow (z\in x)}
(MP twice with A2, I, 10)
(13)
(
z
∈
x
)
⇔
(
z
∈
y
)
{\displaystyle (z\in x)\Leftrightarrow (z\in y)}
(AND with 11, 12)
(14)
∀
z
(
z
∈
x
⇔
z
∈
y
)
{\displaystyle \forall z(z\in x\Leftrightarrow z\in y)}
(GEN with 13)
引入新的函數符號前,常需要唯一存在性 的證明,而外延定理大大簡化了證明的難度。
特定條件下的存在性
以下關於一階邏輯 的一般性定理,也大大簡化了 NBG 引入新公理的過程所需的證明
(DC, Definition under certain condition) —
x
{\displaystyle x}
於合式公式
A
{\displaystyle {\mathcal {A}}}
完全不自由且
c
{\displaystyle c}
是常數符號 。若
A
⊢
(
∃
x
)
B
{\displaystyle {\mathcal {A}}\vdash (\exists x){\mathcal {B}}}
則有
⊢
(
∃
x
)
{
[
¬
A
∧
(
x
=
c
)
]
∨
(
A
∧
B
)
}
{\displaystyle \vdash (\exists x)\{\,[\,\neg {\mathcal {A}}\wedge (x=c)\,]\vee ({\mathcal {A}}\wedge {\mathcal {B}})\,\}}
證明
(1)
A
⇒
(
∃
x
)
B
{\displaystyle {\mathcal {A}}\Rightarrow (\exists x){\mathcal {B}}}
(Hyp)
(2)
(
∀
x
)
{
¬
{
[
¬
A
∧
(
x
=
c
)
]
∨
(
A
∧
B
)
}
}
{\displaystyle (\forall x)\{\neg \{[\neg {\mathcal {A}}\wedge (x=c)]\vee ({\mathcal {A}}\wedge {\mathcal {B}})\}\}}
(Hyp)
(3)
¬
{
[
¬
A
∧
(
x
=
c
)
]
∨
(
A
∧
B
)
}
{\displaystyle \neg \{[\neg {\mathcal {A}}\wedge (x=c)]\vee ({\mathcal {A}}\wedge {\mathcal {B}})\}}
(MP with A4, 2)
(4)
¬
[
¬
A
∧
(
x
=
c
)
]
∧
¬
(
A
∧
B
)
{\displaystyle \neg [\neg {\mathcal {A}}\wedge (x=c)]\wedge \neg ({\mathcal {A}}\wedge {\mathcal {B}})}
(MP with 3, DIS)
(5)
¬
[
¬
A
∧
(
x
=
c
)
]
{\displaystyle \neg [\neg {\mathcal {A}}\wedge (x=c)]}
(MP with AND,4)
(6)
¬
(
A
∧
B
)
{\displaystyle \neg ({\mathcal {A}}\wedge {\mathcal {B}})}
(MP with AND, 4)
(7)
¬
A
⇒
¬
(
x
=
c
)
{\displaystyle \neg {\mathcal {A}}\Rightarrow \neg (x=c)}
(MP with DIS, DN 5)
(8)
A
⇒
¬
B
{\displaystyle {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}}
(MP with DIS, DN, 5)
(9)
B
⇒
¬
A
{\displaystyle {\mathcal {B}}\Rightarrow \neg {\mathcal {A}}}
(MP with T, 8)
(10)
(
∃
x
)
B
⇒
¬
A
{\displaystyle (\exists x){\mathcal {B}}\Rightarrow \neg {\mathcal {A}}}
(GENe with 9)
(11)
A
⇒
¬
(
∃
x
)
B
{\displaystyle {\mathcal {A}}\Rightarrow \neg (\exists x){\mathcal {B}}}
(MP with T, 11)
(12)
¬
A
{\displaystyle \neg {\mathcal {A}}}
(A3' with 1, 11)
(13)
¬
(
x
=
c
)
{\displaystyle \neg (x=c)}
(MP with 7, 12)
(14)
(
∀
x
)
[
¬
(
x
=
c
)
]
{\displaystyle (\forall x)[\neg (x=c)]}
(GEN with 13)
再套用一次(DN)也就是
A
⇒
(
∃
x
)
B
⊢
(
∀
x
)
{
¬
{
[
¬
A
∧
(
x
=
c
)
]
∨
(
A
∧
B
)
}
}
⇒
¬
(
∃
x
)
(
x
=
c
)
{\displaystyle {\mathcal {A}}\Rightarrow (\exists x){\mathcal {B}}\,\vdash (\forall x)\{\neg \{[\neg {\mathcal {A}}\wedge (x=c)]\vee ({\mathcal {A}}\wedge {\mathcal {B}})\}\}\Rightarrow \neg (\exists x)(x=c)}
但由一階邏輯的等式性質 有
⊢
c
=
c
{\displaystyle \vdash c=c}
對上式以變數
x
{\displaystyle x}
套用一次(GENe)有
⊢
(
∃
x
)
(
x
=
c
)
{\displaystyle \vdash (\exists x)(x=c)}
所以由(C2)本定理就會得證。
◻
{\displaystyle \Box }
(
P
)
{\displaystyle (P)}
—
(
∀
M
x
)
(
∀
M
y
)
(
∃
M
p
)
(
∀
M
z
)
{
(
z
∈
p
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
}
{\displaystyle ({\forall }^{M}x)({\forall }^{M}y)({\exists }^{M}p)({\forall }^{M}z)\{(z\in p)\Leftrightarrow [(z=x)\vee (z=y)]\}}
這個公理的直觀意思是「對所有集合x和集合y,存在一個僅以x跟y為元素的集合p」。
這個公理還確保了以下的唯一性:
定理(P-1) —
M
(
x
)
∧
M
(
y
)
⊢
(
∃
!
p
)
{
M
(
p
)
∧
(
∀
M
z
)
{
(
z
∈
p
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
}
}
{\displaystyle {\mathcal {M}}(x)\wedge {\mathcal {M}}(y)\vdash (\exists !p){\big \{}\,{\mathcal {M}}(p)\wedge ({\forall }^{M}z)\{\,(z\in p)\Leftrightarrow [(z=x)\vee (z=y)]\,\}\,{\big \}}}
證明
根據量詞的簡寫 ,配對公理(P)等價於
(
∀
x
)
(
∀
y
)
{
M
(
x
)
∧
M
(
y
)
⇒
(
∃
p
)
{
M
(
p
)
∧
(
∀
M
z
)
{
(
z
∈
p
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
}
}
}
{\displaystyle (\forall x)(\forall y){\bigg \{}\,{\mathcal {M}}(x)\wedge {\mathcal {M}}(y)\Rightarrow (\exists p){\big \{}\,{\mathcal {M}}(p)\wedge ({\forall }^{M}z)\{\,(z\in p)\Leftrightarrow [(z=x)\vee (z=y)]\,\}\,{\big \}}\,{\bigg \}}}
這樣對上式套用兩次量詞公理 的(A4)有
M
(
x
)
∧
M
(
y
)
⇒
(
∃
p
)
{
M
(
p
)
∧
(
∀
M
z
)
{
(
z
∈
p
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
}
}
{\displaystyle {\mathcal {M}}(x)\wedge {\mathcal {M}}(y)\Rightarrow (\exists p){\big \{}\,{\mathcal {M}}(p)\wedge ({\forall }^{M}z)\{\,(z\in p)\Leftrightarrow [(z=x)\vee (z=y)]\,\}\,{\big \}}}
這樣在有
M
(
x
)
∧
M
(
y
)
{\displaystyle {\mathcal {M}}(x)\wedge {\mathcal {M}}(y)}
的前提就有
(
∃
p
)
{
M
(
p
)
∧
(
∀
M
z
)
{
(
z
∈
p
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
}
}
{\displaystyle (\exists p){\big \{}\,{\mathcal {M}}(p)\wedge ({\forall }^{M}z)\{\,(z\in p)\Leftrightarrow [(z=x)\vee (z=y)]\,\}\,{\big \}}}
所以
M
(
x
)
∧
M
(
y
)
⊢
(
∃
p
)
{
M
(
p
)
∧
(
∀
M
z
)
{
(
z
∈
p
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
}
}
{\displaystyle {\mathcal {M}}(x)\wedge {\mathcal {M}}(y)\vdash (\exists p){\big \{}\,{\mathcal {M}}(p)\wedge ({\forall }^{M}z)\{\,(z\in p)\Leftrightarrow [(z=x)\vee (z=y)]\,\}\,{\big \}}}
另一方面,若假設
M
(
p
)
∧
(
∀
M
z
)
{
(
z
∈
p
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
}
{\displaystyle {\mathcal {M}}(p)\wedge ({\forall }^{M}z)\{\,(z\in p)\Leftrightarrow [(z=x)\vee (z=y)]\,\}}
M
(
π
)
∧
(
∀
M
z
)
{
(
z
∈
π
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
}
{\displaystyle {\mathcal {M}}(\pi )\wedge ({\forall }^{M}z)\{\,(z\in \pi )\Leftrightarrow [(z=x)\vee (z=y)]\,\}}
這樣根據邏輯與的直觀性質 有
(
∀
M
z
)
{
(
z
∈
p
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
}
{\displaystyle ({\forall }^{M}z)\{\,(z\in p)\Leftrightarrow [(z=x)\vee (z=y)]\,\}}
(
∀
M
z
)
{
(
z
∈
π
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
}
{\displaystyle ({\forall }^{M}z)\{\,(z\in \pi )\Leftrightarrow [(z=x)\vee (z=y)]\,\}}
再根據(A4)有
M
(
z
)
⇒
{
(
z
∈
p
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
}
{\displaystyle {\mathcal {M}}(z)\Rightarrow \{\,(z\in p)\Leftrightarrow [(z=x)\vee (z=y)]\,\}}
M
(
z
)
⇒
{
(
z
∈
π
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
}
{\displaystyle {\mathcal {M}}(z)\Rightarrow \{\,(z\in \pi )\Leftrightarrow [(z=x)\vee (z=y)]\,\}}
如果再假設
M
(
z
)
{\displaystyle {\mathcal {M}}(z)}
,根據MP律 有
(
z
∈
p
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
{\displaystyle (z\in p)\Leftrightarrow [(z=x)\vee (z=y)]}
(
z
∈
π
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
{\displaystyle (z\in \pi )\Leftrightarrow [(z=x)\vee (z=y)]}
這樣根據演繹定理 的推論(D1)和邏輯與的直觀性質 有
(
z
∈
p
)
⇔
(
z
∈
π
)
{\displaystyle (z\in p)\Leftrightarrow (z\in \pi )}
也就是說
B
(
p
)
∧
B
(
π
)
,
M
(
z
)
⊢
(
z
∈
p
)
⇔
(
z
∈
π
)
{\displaystyle {\mathcal {B}}(p)\wedge {\mathcal {B}}(\pi ),\,{\mathcal {M}}(z)\,\vdash \,(z\in p)\Leftrightarrow (z\in \pi )}
其中
B
(
p
)
:=
M
(
p
)
∧
(
∀
M
z
)
{
(
z
∈
p
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
}
{\displaystyle {\mathcal {B}}(p):={\mathcal {M}}(p)\wedge ({\forall }^{M}z)\{\,(z\in p)\Leftrightarrow [(z=x)\vee (z=y)]\,\}}
因為變數
z
{\displaystyle z}
在
B
(
p
)
{\displaystyle {\mathcal {B}}(p)}
和
B
(
π
)
{\displaystyle {\mathcal {B}}(\pi )}
內完全不自由,對上式套用演繹定理 (D)將
M
(
z
)
{\displaystyle {\mathcal {M}}(z)}
移到右方後,再對
z
{\displaystyle z}
套用普遍化 會有
B
(
p
)
∧
B
(
π
)
⊢
(
∀
M
z
)
[
(
z
∈
p
)
⇔
(
z
∈
π
)
]
{\displaystyle {\mathcal {B}}(p)\wedge {\mathcal {B}}(\pi )\,\vdash \,(\forall ^{M}z)[\,(z\in p)\Leftrightarrow (z\in \pi )\,]}
這樣根據本條目的外延定理 有
B
(
p
)
∧
B
(
π
)
⊢
(
p
=
π
)
{\displaystyle {\mathcal {B}}(p)\wedge {\mathcal {B}}(\pi )\,\vdash \,(p=\pi )}
那以演繹定理 (D)將
B
(
p
)
∧
B
(
π
)
{\displaystyle {\mathcal {B}}(p)\wedge {\mathcal {B}}(\pi )}
移到右方,然後接連對
p
{\displaystyle p}
和
π
{\displaystyle \pi }
使用普遍化 有
⊢
(
∀
p
)
(
∀
π
)
[
B
(
p
)
∧
B
(
π
)
⇒
(
p
=
π
)
]
{\displaystyle \vdash (\forall p)(\forall \pi )[\,{\mathcal {B}}(p)\wedge {\mathcal {B}}(\pi )\Rightarrow (p=\pi )\,]}
故本定理得証。
◻
{\displaystyle \Box }
這樣的話會有
定理 —
⊢
(
∃
!
p
)
{
{
¬
[
M
(
x
)
∧
M
(
y
)
]
∧
(
p
=
∅
)
}
∨
{
M
(
x
)
∧
M
(
y
)
∧
M
(
p
)
∧
(
∀
M
z
)
{
(
z
∈
p
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
}
}
}
{\displaystyle \vdash (\exists !p){\bigg \{}\,\{\,\neg [\,{\mathcal {M}}(x)\wedge {\mathcal {M}}(y)\,]\wedge (p=\varnothing )\,\}\vee {\big \{}\,{\mathcal {M}}(x)\wedge {\mathcal {M}}(y)\wedge {\mathcal {M}}(p)\wedge ({\forall }^{M}z)\{\,(z\in p)\Leftrightarrow [(z=x)\vee (z=y)]\,\}\,{\big \}}\,{\bigg \}}}
證明
根據(P-1)和本條目的特定條件下的存在性 (DC)會有
(P-2)
⊢
(
∃
p
)
{
{
¬
[
M
(
x
)
∧
M
(
y
)
]
∧
(
p
=
∅
)
}
∨
{
M
(
x
)
∧
M
(
y
)
∧
M
(
p
)
∧
(
∀
M
z
)
{
(
z
∈
p
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
}
}
}
{\displaystyle \vdash (\exists p){\bigg \{}\,\{\,\neg [\,{\mathcal {M}}(x)\wedge {\mathcal {M}}(y)\,]\wedge (p=\varnothing )\,\}\vee {\big \{}\,{\mathcal {M}}(x)\wedge {\mathcal {M}}(y)\wedge {\mathcal {M}}(p)\wedge ({\forall }^{M}z)\{\,(z\in p)\Leftrightarrow [(z=x)\vee (z=y)]\,\}\,{\big \}}\,{\bigg \}}}
設
A
(
p
)
:=
¬
[
M
(
x
)
∧
M
(
y
)
]
∧
(
p
=
∅
)
{\displaystyle {\mathcal {A}}(p):=\neg [\,{\mathcal {M}}(x)\wedge {\mathcal {M}}(y)\,]\wedge (p=\varnothing )}
B
(
p
)
:=
M
(
x
)
∧
M
(
y
)
∧
M
(
p
)
∧
(
∀
M
z
)
{
(
z
∈
p
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
}
{\displaystyle {\mathcal {B}}(p):={\mathcal {M}}(x)\wedge {\mathcal {M}}(y)\wedge {\mathcal {M}}(p)\wedge ({\forall }^{M}z)\{\,(z\in p)\Leftrightarrow [(z=x)\vee (z=y)]\,\}}
C
:=
M
(
x
)
∧
M
(
y
)
{\displaystyle {\mathcal {C}}:={\mathcal {M}}(x)\wedge {\mathcal {M}}(y)}
那連續套用邏輯與合邏輯或的分配律 與邏輯與的交換性 會有
⊢
{
[
A
(
p
)
∨
B
(
p
)
]
∧
[
A
(
π
)
∨
B
(
π
)
]
}
⇔
{
{
[
A
(
p
)
∧
A
(
π
)
]
∨
[
B
(
p
)
∧
A
(
π
)
]
}
∨
{
[
A
(
p
)
∧
B
(
π
)
]
∨
[
B
(
p
)
∧
B
(
π
)
]
}
}
{\displaystyle \vdash \{\,[\,{\mathcal {A}}(p)\vee {\mathcal {B}}(p)\,]\wedge [\,{\mathcal {A}}(\pi )\vee {\mathcal {B}}(\pi )\,]\,\}\Leftrightarrow {\big \{}\,\{\,[\,{\mathcal {A}}(p)\wedge {\mathcal {A}}(\pi )\,]\vee [\,{\mathcal {B}}(p)\wedge {\mathcal {A}}(\pi )\,]\,\}\vee \{\,[\,{\mathcal {A}}(p)\wedge {\mathcal {B}}(\pi )\,]\vee [\,{\mathcal {B}}(p)\wedge {\mathcal {B}}(\pi )\,]\,\}\,{\big \}}}
但考慮到邏輯與的直觀性質 和邏輯與的定義 有
⊢
[
B
(
p
)
∧
A
(
π
)
]
⇒
(
¬
C
∧
C
)
{\displaystyle \vdash [\,{\mathcal {B}}(p)\wedge {\mathcal {A}}(\pi )\,]\Rightarrow (\neg {\mathcal {C}}\wedge {\mathcal {C}})}
⊢
[
A
(
p
)
∧
B
(
π
)
]
⇒
(
¬
C
∧
C
)
{\displaystyle \vdash [\,{\mathcal {A}}(p)\wedge {\mathcal {B}}(\pi )\,]\Rightarrow (\neg {\mathcal {C}}\wedge {\mathcal {C}})}
⊢
(
¬
C
∧
C
)
⇔
¬
(
C
⇒
C
)
{\displaystyle \vdash (\neg {\mathcal {C}}\wedge {\mathcal {C}})\Leftrightarrow \neg ({\mathcal {C}}\Rightarrow {\mathcal {C}})}
那根據恆等關係
(
I
)
{\displaystyle (I)}
和常用的推理性質 (T)有
⊢
¬
[
B
(
p
)
∧
A
(
π
)
]
{\displaystyle \vdash \neg [\,{\mathcal {B}}(p)\wedge {\mathcal {A}}(\pi )\,]}
⊢
¬
[
A
(
p
)
∧
B
(
π
)
]
{\displaystyle \vdash \neg [\,{\mathcal {A}}(p)\wedge {\mathcal {B}}(\pi )\,]}
所以根據邏輯或的定義 來重複使用演繹定理 的推論(D1)會有
⊢
{
[
A
(
p
)
∨
B
(
p
)
]
∧
[
A
(
π
)
∨
B
(
π
)
]
}
⇔
{
[
A
(
p
)
∧
A
(
π
)
]
∨
[
B
(
p
)
∧
B
(
π
)
]
}
{\displaystyle \vdash \{\,[\,{\mathcal {A}}(p)\vee {\mathcal {B}}(p)\,]\wedge [\,{\mathcal {A}}(\pi )\vee {\mathcal {B}}(\pi )\,]\,\}\Leftrightarrow \{\,[\,{\mathcal {A}}(p)\wedge {\mathcal {A}}(\pi )\,]\vee [\,{\mathcal {B}}(p)\wedge {\mathcal {B}}(\pi )\,]\,\}}
然後從NBG 的等式定理 會有
⊢
[
A
(
p
)
∧
A
(
π
)
]
⇒
(
p
=
π
)
{\displaystyle \vdash [\,{\mathcal {A}}(p)\wedge {\mathcal {A}}(\pi )\,]\Rightarrow (p=\pi )}
另一方面,根據(P-1)有
⊢
[
B
(
p
)
∧
B
(
π
)
]
⇒
(
p
=
π
)
{\displaystyle \vdash [\,{\mathcal {B}}(p)\wedge {\mathcal {B}}(\pi )\,]\Rightarrow (p=\pi )}
這樣結合邏輯與 的(DisJ)有
⊢
{
[
A
(
p
)
∨
B
(
p
)
]
∧
[
A
(
π
)
∨
B
(
π
)
]
}
⇒
(
p
=
π
)
{\displaystyle \vdash \{\,[\,{\mathcal {A}}(p)\vee {\mathcal {B}}(p)\,]\wedge [\,{\mathcal {A}}(\pi )\vee {\mathcal {B}}(\pi )\,]\,\}\Rightarrow (p=\pi )}
再對
p
{\displaystyle p}
和
π
{\displaystyle \pi }
套用普遍化 有
⊢
(
∀
p
)
(
∀
π
)
{
{
[
A
(
p
)
∨
B
(
p
)
]
∧
[
A
(
π
)
∨
B
(
π
)
]
}
⇒
(
p
=
π
)
}
{\displaystyle \vdash (\forall p)(\forall \pi ){\bigg \{}\,\{\,[\,{\mathcal {A}}(p)\vee {\mathcal {B}}(p)\,]\wedge [\,{\mathcal {A}}(\pi )\vee {\mathcal {B}}(\pi )\,]\,\}\Rightarrow (p=\pi )\,{\bigg \}}}
這樣結合剛剛的(P-2)與邏輯與的直觀性質 ,本定理就得證了。
◻
{\displaystyle \Box }
所以根據函數符號與唯一性 一節,可以在NBG 加入新的雙元函數符號
f
p
2
(
x
,
y
)
{\displaystyle f_{p}^{2}(x,\,y)}
(簡記為
{
x
,
y
}
{\displaystyle \{x,\,y\}}
)和以下的新公理
(
P
′
)
{\displaystyle (P^{\prime })}
—
{
¬
[
M
(
x
)
∧
M
(
y
)
]
∧
(
{
x
,
y
}
=
∅
)
}
∨
{\displaystyle {\bigg \{}\neg [\,{\mathcal {M}}(x)\wedge {\mathcal {M}}(y)\,]\wedge (\{x,\,y\}=\varnothing ){\bigg \}}\vee }
{
M
(
x
)
∧
M
(
y
)
∧
M
(
{
x
,
y
}
)
∧
(
∀
M
z
)
{
(
z
∈
{
x
,
y
}
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
}
}
{\displaystyle {\bigg \{}{\mathcal {M}}(x)\wedge {\mathcal {M}}(y)\wedge {\mathcal {M}}\left(\{x,\,y\}\right)\wedge ({\forall }^{M}z)\{\,(z\in \{x,\,y\})\Leftrightarrow [(z=x)\vee (z=y)]\,\}{\bigg \}}}
這個新公理的直觀意思是「若x和y為集合,則
{
x
,
y
}
{\displaystyle \{x,\,y\}}
就是那個只以x和y為元素的集合;但反之,若x和y不全為集合,則
{
x
,
y
}
{\displaystyle \{x,\,y\}}
為空集 」。
有序對
{
x
}
:=
{
x
,
x
}
{\displaystyle \{x\}:=\{x,\,x\}}
⟨
x
⟩
:=
x
{\displaystyle \langle x\rangle :=x}
⟨
x
,
y
⟩
:=
{
{
x
}
,
{
x
,
y
}
}
{\displaystyle \langle x,\,y\rangle :=\{\{x\},\,\{x,\,y\}\}}
⟨
x
1
,
…
,
x
n
,
x
n
+
1
⟩
:=
⟨
⟨
x
1
,
…
,
x
n
⟩
,
x
n
+
1
⟩
{\displaystyle \langle x_{1},\,\dots ,\,\,x_{n},\,x_{n+1}\rangle :=\langle \langle x_{1},\,\dots ,\,\,x_{n}\rangle ,\,x_{n+1}\rangle }
在不跟括弧產生混淆的情況下,也可以把
⟨
x
1
,
…
,
x
n
,
x
n
+
1
⟩
{\displaystyle \langle x_{1},\,\dots ,\,\,x_{n},\,x_{n+1}\rangle }
記為
(
x
1
,
…
,
x
n
,
x
n
+
1
)
{\displaystyle (x_{1},\,\dots ,\,\,x_{n},\,x_{n+1})}
。
關係
R
e
l
(
f
)
:=
(
∀
M
a
)
{
(
a
∈
f
)
⇒
(
∃
x
)
(
∃
y
)
{
M
(
x
)
∧
M
(
y
)
∧
[
a
=
(
x
,
y
)
]
}
}
{\displaystyle Rel(f):=(\forall ^{M}a){\big \{}\,(a\in f)\Rightarrow (\exists x)(\exists y)\{\,{\mathcal {M}}(x)\wedge {\mathcal {M}}(y)\wedge [\,a=(x,\,y)\,]\,\}\,{\big \}}}
類函數
F
n
c
(
f
)
:=
R
e
l
(
f
)
∧
(
∀
M
x
)
(
∀
M
y
)
(
∀
M
υ
)
{
[
(
x
,
y
)
∈
f
∧
(
x
,
υ
)
∈
f
]
⇒
(
y
=
υ
)
}
{\displaystyle Fnc(f):=Rel(f)\wedge (\forall ^{M}x)(\forall ^{M}y)(\forall ^{M}\upsilon )\{\,[\,(x,\,y)\in f\wedge (x,\,\upsilon )\in f\,]\Rightarrow (y=\upsilon )\,\}}
類函數跟普通函數 的差別在於普通函數是個集合 。
屬於類公理
(
K
∈
)
{\displaystyle (K_{\in })}
—
(
∃
e
)
(
∀
M
a
)
(
∀
M
b
)
{
[
(
a
,
b
)
∈
e
]
⇔
(
a
∈
b
)
}
{\displaystyle (\exists e)(\forall ^{M}a)(\forall ^{M}b)\{[(a,\,b)\in e]\Leftrightarrow (a\in b)\}}
交類公理
(
K
i
)
{\displaystyle (K_{i})}
—
(
∀
x
)
(
∀
y
)
(
∃
i
)
(
∀
M
a
)
{
(
a
∈
i
)
⇔
[
(
a
∈
x
)
∧
(
a
∈
y
)
]
}
{\displaystyle (\forall x)(\forall y)(\exists i)({\forall }^{M}a)\{(a\in i)\Leftrightarrow [(a\in x)\wedge (a\in y)]\}}
補類公理
(
K
c
)
{\displaystyle (K_{c})}
—
(
∀
x
)
(
∃
c
)
(
∀
M
a
)
[
(
a
∈
c
)
⇔
(
a
∉
x
)
]
{\displaystyle (\forall x)(\exists c)({\forall }^{M}a)[(a\in c)\Leftrightarrow (a\not \in x)]}
定義域公理
(
K
D
)
{\displaystyle (K_{D})}
—
(
∀
x
)
(
∃
d
)
(
∀
M
a
)
{
(
a
∈
d
)
⇔
(
∃
M
b
)
[
(
a
,
b
)
∈
x
]
}
{\displaystyle (\forall x)(\exists d)(\forall ^{M}a)\{(a\in d)\Leftrightarrow (\exists ^{M}b)[(a,\,b)\in x]\}}
積類公理
(
K
p
)
{\displaystyle (K_{p})}
—
(
∀
x
)
(
∃
p
)
(
∀
M
a
)
(
∀
M
b
)
{
[
(
a
,
b
)
∈
p
]
⇔
(
a
∈
x
)
}
{\displaystyle (\forall x)(\exists p)(\forall ^{M}a)(\forall ^{M}b)\{[\,(a,\,b)\in p\,]\Leftrightarrow (a\in x)\}}
置換類公理
(
K
σ
1
)
{\displaystyle (K_{\sigma 1})}
—
(
∀
x
)
(
∃
σ
)
(
∀
M
a
)
(
∀
M
b
)
(
∀
M
c
)
{
[
(
a
,
b
,
c
)
∈
x
]
⇔
[
(
b
,
c
,
a
)
∈
σ
]
}
{\displaystyle (\forall x)(\exists \sigma )(\forall ^{M}a)(\forall ^{M}b)(\forall ^{M}c)\{[(a,\,b,\,c)\in x]\Leftrightarrow [(b,\,c,\,a)\in \sigma ]\}}
(
K
σ
2
)
{\displaystyle (K_{\sigma 2})}
—
(
∀
x
)
(
∃
σ
)
(
∀
M
a
)
(
∀
M
b
)
(
∀
M
c
)
{
[
(
a
,
b
,
c
)
∈
x
]
⇔
[
(
a
,
c
,
b
)
∈
σ
]
}
{\displaystyle (\forall x)(\exists \sigma )(\forall ^{M}a)(\forall ^{M}b)(\forall ^{M}c)\{[(a,\,b,\,c)\in x]\Leftrightarrow [(a,\,c,\,b)\in \sigma ]\}}
類的存在元定理
這個元定理對應到ZFC爾集合論的分類公理 。
首先需要遞歸地定義 「可敘述公式 」(predicative well-formed formula):
對任意變數
x
{\displaystyle x}
和
y
{\displaystyle y}
,
x
∈
y
{\displaystyle x\in y}
為可敘述公式。
若
P
{\displaystyle {\mathcal {P}}}
與
Q
{\displaystyle {\mathcal {Q}}}
為可敘述公式,
x
{\displaystyle x}
為任意變數,則
(
¬
P
)
{\displaystyle (\neg {\mathcal {P}})}
、
(
P
⇒
Q
)
{\displaystyle ({\mathcal {P}}\Rightarrow {\mathcal {Q}})}
與
(
∀
M
x
)
P
{\displaystyle (\forall ^{M}x){\mathcal {P}}}
都是可敘述公式。
這樣依據上列諸類存在公理,就有以下元定理:
類的存在元定理 —
P
{\displaystyle {\mathcal {P}}}
為一條只內含變數
x
1
,
…
,
x
n
,
y
1
,
…
,
y
m
{\displaystyle x_{1},\,\dots ,\,x_{n},\,y_{1},\,\dots ,\,y_{m}}
的可敘述公式,則有
⊢
(
∃
s
)
(
∀
M
x
1
)
…
(
∀
M
x
n
)
[
(
⟨
x
1
,
…
,
x
n
⟩
∈
s
)
⇔
P
]
{\displaystyle \vdash (\exists s)(\forall ^{M}x_{1})\ldots (\forall ^{M}x_{n})[(\langle x_{1},\,\dots ,\,x_{n}\rangle \in s)\Leftrightarrow {\mathcal {P}}]}