在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 內額外添加以下的公理
直觀上可理解為「類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)} 的確符合直觀上對等號的要求,還需添加以下的公理
直觀上,這個公理確保「x等於y,則x屬於z等同於y屬於z」。
這樣,以下的元定理 就確保了如此定義的等號是「成功的」。
元定理 — NBG 是帶相等符號 ( x = y ) {\displaystyle (x=y)} 的一阶逻辑 理論
真子類 编辑 在定義「相等」以後,可以把「相等的類」排除出子類的定義中,換句話說,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 引入新公理的過程所需的證明
證明 (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 }
這個公理的直觀意思是「對所有集合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 σ 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}})} 與 ( ∀ x M ) P {\displaystyle (\forall x^{M}){\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}}]}