冯·诺伊曼-博内斯-哥德尔集合论 (英語:von Neumann–Bernays–Gödel Set Theory ,NBG )是種以类 為直觀動機的一阶 公理化集合论 ,它是配上选择公理 的策梅洛-弗兰克尔集合论 (英語:Zermelo-Fraenkel Set Theory with the axiom of Choice ,ZFC )的保守扩展 (ZFC 裡可以證明的定理 也都是NBG 的定理)[ 1] ,而且NBG 僅需在一階邏輯基本的公理模式 上添加有限数目的公理,但ZFC 需添加與集合有關的公理模式[ 2] 。
NBG 首先由冯·诺伊曼 在1920年代提出,從1937年开始由保罗·博内斯 作修改,在1940年由哥德尔 进一步简化。
在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 }
( N ) {\displaystyle (N)} — ( ∃ M x ) ( ∀ M y ) ( y ∉ x ) {\displaystyle ({\exists }^{M}x)({\forall }^{M}y)(y\not \in x)}
這個公理的直觀意思是「存在集合x,使的所有集合y都不屬於x」。
事實上這個公理還確保了空集 的唯一性,嚴格來說,它確保了:
定理 — ⊢ ( ∃ ! x ) [ M ( x ) ∧ ( ∀ M y ) ( y ∉ x ) ] {\displaystyle \vdash (\exists !x)[\,{\mathcal {M}}(x)\wedge ({\forall }^{M}y)(y\not \in x)\,]}
證明 假設
( ∀ M y ) ( y ∉ x ) {\displaystyle ({\forall }^{M}y)(y\not \in x)} ( ∀ M y ) ( y ∉ t ) {\displaystyle ({\forall }^{M}y)(y\not \in t)} 那根據量词公理 的(A4)有
M ( y ) ⇒ ( y ∉ x ) {\displaystyle {\mathcal {M}}(y)\Rightarrow (y\not \in x)} M ( y ) ⇒ ( y ∉ t ) {\displaystyle {\mathcal {M}}(y)\Rightarrow (y\not \in t)} 另一方面,根據常用的推理性質 的(M0)有
⊢ ( y ∉ x ) ⇒ [ ( y ∈ x ) ⇒ ( y ∈ t ) ] {\displaystyle \vdash (y\not \in x)\Rightarrow [\,(y\in x)\Rightarrow (y\in t)\,]} ⊢ ( y ∉ t ) ⇒ [ ( y ∈ t ) ⇒ ( y ∈ x ) ] {\displaystyle \vdash (y\not \in t)\Rightarrow [\,(y\in t)\Rightarrow (y\in x)\,]} 這樣根據演繹定理 的推論(D1)有
M ( y ) ⇒ [ ( y ∈ x ) ⇒ ( y ∈ t ) ] {\displaystyle {\mathcal {M}}(y)\Rightarrow [\,(y\in x)\Rightarrow (y\in t)\,]} M ( y ) ⇒ [ ( y ∈ t ) ⇒ ( y ∈ x ) ] {\displaystyle {\mathcal {M}}(y)\Rightarrow [\,(y\in t)\Rightarrow (y\in x)\,]} 這樣根據常用的推理性質 (T)有
¬ [ ( y ∈ x ) ⇒ ( y ∈ t ) ] ⇒ ¬ M ( y ) {\displaystyle \neg [\,(y\in x)\Rightarrow (y\in t)\,]\Rightarrow \neg {\mathcal {M}}(y)} ¬ [ ( y ∈ t ) ⇒ ( y ∈ x ) ] ⇒ ¬ M ( y ) {\displaystyle \neg [\,(y\in t)\Rightarrow (y\in x)\,]\Rightarrow \neg {\mathcal {M}}(y)} 這樣根據德摩根定律 和邏輯與 的(DisJ)有
¬ { [ ( y ∈ x ) ⇒ ( y ∈ t ) ] ∧ [ ( y ∈ t ) ⇒ ( y ∈ x ) ] } ⇒ ¬ M ( y ) {\displaystyle \neg \{\,[\,(y\in x)\Rightarrow (y\in t)\,]\wedge [\,(y\in t)\Rightarrow (y\in x)\,]\,\}\Rightarrow \neg {\mathcal {M}}(y)} 這樣再根據(T)有
M ( y ) ⇒ [ ( y ∈ x ) ⇔ ( y ∈ t ) ] {\displaystyle {\mathcal {M}}(y)\Rightarrow [\,(y\in x)\Leftrightarrow (y\in t)\,]} 這樣根據普遍化 有
( ∀ M y ) [ ( y ∈ x ) ⇔ ( y ∈ t ) ] {\displaystyle (\forall ^{M}y)[\,(y\in x)\Leftrightarrow (y\in t)\,]} 那這樣根據上節的外延定理 有
x = t {\displaystyle x=t} 換句話說
⊢ [ ( ∀ M y ) ( y ∉ x ) ∧ ( ∀ M y ) ( y ∉ t ) ] ⇒ ( x = t ) {\displaystyle \vdash [\,({\forall }^{M}y)(y\not \in x)\wedge ({\forall }^{M}y)(y\not \in t)\,]\Rightarrow (x=t)} 這樣根據邏輯與的直觀性質 和(D1)有
⊢ { [ M ( x ) ∧ ( ∀ M y ) ( y ∉ x ) ] ∧ [ M ( t ) ∧ ( ∀ M y ) ( y ∉ t ) ] } ⇒ ( x = t ) {\displaystyle \vdash \{\,[\,{\mathcal {M}}(x)\wedge ({\forall }^{M}y)(y\not \in x)\,]\wedge [\,{\mathcal {M}}(t)\wedge ({\forall }^{M}y)(y\not \in t)\,]\,\}\Rightarrow (x=t)} 這樣根據普遍化 有
⊢ ( ∀ x ) ( ∀ t ) { { [ M ( x ) ∧ ( ∀ M y ) ( y ∉ x ) ] ∧ [ M ( t ) ∧ ( ∀ M y ) ( y ∉ t ) ] } ⇒ ( x = t ) } {\displaystyle \vdash (\forall x)(\forall t){\big \{}\,\{\,[\,{\mathcal {M}}(x)\wedge ({\forall }^{M}y)(y\not \in x)\,]\wedge [\,{\mathcal {M}}(t)\wedge ({\forall }^{M}y)(y\not \in t)\,]\,\}\Rightarrow (x=t)\,{\big \}}} 再綜合本節的空集合公理(N),本定理就得証了。 ◻ {\displaystyle \Box }
也就是直觀上,「空集 是唯一存在的」,這樣根據函數符號與唯一性 一節,可以在NBG 加入新的常數符號 ∅ {\displaystyle \varnothing } 和以下的新公理(嚴格來說,把完全沒有函數符號和常數符號的NBG 擴展成有 ∅ {\displaystyle \varnothing } 的新NBG ,但兩個理論是等效的)
( N ′ ) {\displaystyle (N^{\prime })} — M ( ∅ ) ∧ ( ∀ M y ) ( y ∉ ∅ ) {\displaystyle {\mathcal {M}}(\varnothing )\wedge ({\forall }^{M}y)(y\not \in \varnothing )}
這個新公理直觀上以「 ∅ {\displaystyle \varnothing } 為集合,且任意集合y都不屬於 ∅ {\displaystyle \varnothing } 」,把 ∅ {\displaystyle \varnothing } 定義成了空集 的表示符號。
( 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}}]} ( U ) {\displaystyle (U)} — ( ∀ M x ) ( ∃ M u ) ( ∀ M a ) [ ( a ∈ u ) ⇔ ( ∃ M ξ ∈ x ) ( a ∈ ξ ) ] {\displaystyle (\forall ^{M}x)(\exists ^{M}u)(\forall ^{M}a)[(a\in u)\Leftrightarrow (\exists ^{M}\xi \in x)(a\in \xi )]}
( W ) {\displaystyle (W)} — ( ∀ M x ) ( ∃ M w ) ( ∀ M ξ ) { ( ξ ∈ w ) ⇔ ( ξ ⊆ x ) } {\displaystyle (\forall ^{M}x)(\exists ^{M}w)(\forall ^{M}\xi )\{(\xi \in w)\Leftrightarrow (\xi \subseteq x)\}}
( S ) {\displaystyle (S)} — ( ∀ M x ) ( ∀ y ) ( ∃ M z ) ( ∀ M a ) { ( a ∈ z ) ⇔ [ ( a ∈ x ) ∧ ( a ∈ y ) ] } {\displaystyle (\forall ^{M}x)(\forall y)(\exists ^{M}z)(\forall ^{M}a)\{(a\in z)\Leftrightarrow [(a\in x)\wedge (a\in y)]\}}
( I ) {\displaystyle (I)} — ( ∃ M I ) { ( ∅ ∈ I ) ∧ ( ∀ M a ) [ ( a ∈ I ) ⇒ ( a ∩ { a } ∈ I ) ] } {\displaystyle (\exists ^{M}I)\{(\varnothing \in I)\wedge (\forall ^{M}a)[(a\in I)\Rightarrow (a\cap \{a\}\in I)]\}}
( R ) {\displaystyle (R)} — F n c ( f ) ⇒ ( ∀ M x ) ( ∃ M r ) ( ∀ M b ) { ( b ∈ r ) ⇒ ( ∃ M a ) { ( ⟨ a , b ⟩ ∈ r ) ∧ ( a ∈ x ) } } {\displaystyle Fnc(f)\Rightarrow (\forall ^{M}x)(\exists ^{M}r)(\forall ^{M}b){\bigg \{}(b\in r)\Rightarrow (\exists ^{M}a)\{(\langle a,\,b\rangle \in r)\wedge (a\in x)\}{\bigg \}}}
直觀意義為「 f {\displaystyle f} 為类函数則對任意集合 x {\displaystyle x} ,存在一個集合 r {\displaystyle r} ,正好就是在 f {\displaystyle f} 的規則下映射出的像 」。
对于任何类 C ,存在一个集合 x 使得 R p ( C , x ) {\displaystyle Rp(C,x)} (謂 x 是 C 的表示,即 C 和 x 所包含的元素一樣),当且仅当没有在 C 和所有集合的类 V 之间的双射。 这个公理贡献自冯·诺伊曼,并一下实现了分离公理、替代公理和全局选择公理。他效力相當於原始的替代公理加上这选择公理。完全的大小限制公理蕴涵了全局选择公理 ,因为序数的类不是集合,所以有从序数到全集的双射。
Bernays, Paul. Axiomatic Set Theory. Dover Publications. 1991. ISBN 978-0-486-66637-2 . John von Neumann , 1925, "An Axiomatization of Set Theory." English translation in Jean van Heijenoort , ed., 1967. From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931 . Harvard University Press. Mendelson, Elliott, 1997 (1964). An Introduction to Mathematical Logic , 4th ed. Chapman & Hall. The classic textbook treatment of NBG set theory, showing how it can found mathematics. Richard Montague , 1961, "Semantic Closure and Non-Finite Axiomatizability I," in Infinitistic Methods, Proceedings of the Symposium on Foundations of Mathematics , (Warsaw, 2-9 September 1959). Pergamon: 45-69. von Neumann-Bernays-Gödel set theory . PlanetMath .
^ Cohen, Paul J. Set Theory and the Continuum Hypothesis . New York: W. A. Benjamin. 1966 [2023-05-15 ] . (原始内容存档 于2023-05-15). ^ Montague, Richard. Semantical Closure and Non-Finite Axiomatizability I . Journal of Symbolic Logic. 1964, 29 (1) [2023-05-15 ] . doi:10.2307/2269797 . (原始内容存档 于2023-05-15). ^ Mendelson, Elliott. Introduction to Mathematical Logic (6th Edition). Chapman & Hall. 2015: 233–233. ISBN 9781482237726 .