# 集合：由元素刻畫、外延相等，以及不受限制的建構為何失敗

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-set/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-set-01 · production-20261019-adopted-96



## 目標與範圍

在論域 ℤ 中，設 A={x∈ℤ ∣ x²=4}、B={−2,2}、C={2,−2,2}、D={2}。證明 A=B 與 C=B；證明 D≠B，並區分元素 2 與集合 {2}。最後證明：在任何帶有隸屬關係的論域 U 中，都不存在 R∈U 使「y∈R ⇔ y∉y」對所有 y∈U 成立，因此不是每個條件都能形成集合。

依 MKO：在指定論域中，集合由其元素刻畫，具有相同元素的集合相等。前半在論域 ℤ 中工作，集合都是整數的集合；後半的羅素論證只用純邏輯，對任何帶有隸屬關係的論域都成立，不選定 ZF、ZFC 或其他公理系統。不處理集合運算的一般理論；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- set_extensionality
- set_builder
- subset_def
- zero_product
- distributive
- numeric_evaluation


- G1 — 論域與型別：前半在 ℤ 中工作，所討論的集合都是整數的集合；x∈S 的左邊是整數，右邊是整數的集合。列舉記號：x∈{a,b,c} ⇔ x=a ∨ x=b ∨ x=c，兩個或一個元素時同理。
- G2 — A={x∈ℤ ∣ x²=4}，B={−2,2}，C={2,−2,2}，D={2}。
- G3 — 羅素論證的設定：U 是任意一個對象的論域，帶有二元關係 ∈（對 y,z∈U，y∈z 是命題）；不假設任何集合論公理；採古典邏輯。


- x\in A — x 是 A 的元素
- \{a,b,c\} — 列舉式集合：x∈{a,b,c} ⇔ x=a∨x=b∨x=c
- \{x\in\mathbb{Z}\mid P(x)\} — 在 ℤ 中以條件 P 分出的集合
- A=B — 集合相等：元素完全相同
- U — 任意帶有隸屬關係的論域（羅素論證用）





## 規則與來源


- set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
- set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
- subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。
- zero_product · prerequisite — 零乘積性質：在 ℤ、ℚ、ℝ、ℂ（或任何整域）中，uv=0 ⇔ u=0 或 v=0。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
- add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
- add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
- add_zero · prerequisite — 加法單位元：u+0=u。
- neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- logic_chain · prerequisite — 推論的傳遞：由 P⇒Q 與 Q⇒R 得 P⇒R；⇔ 同理。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
- exists_elim · prerequisite — ∃消去：由 ∃x∈D, P(x)，可取一個新名字 a 表示某個滿足 P(a) 的元素；只要最後結論不含 a，就可用 a 推理。
- forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- modus_ponens · prerequisite — 肯定前件：由 P 與 P⇒Q 得 Q。
- iff_intro · prerequisite — 雙條件：P⇒Q 與 Q⇒P 都成立時，P⇔Q 成立；反之亦然。
- mko_set · cited — 在指定的論域或型別中，集合 A 由哪些對象是其元素來刻畫；具有完全相同元素的集合視為相同。 · mko-set
- list_set · prerequisite — 列舉式集合：x∈{a,b,c} ⇔ x=a ∨ x=b ∨ x=c；兩個或一個元素時同理。
- or_laws · prerequisite — 析取的交換、結合與冪等：P∨Q ⇔ Q∨P；(P∨Q)∨R ⇔ P∨(Q∨R)；P∨P ⇔ P。
- excluded_middle · prerequisite — 排中律（古典邏輯）：對任何命題 P，P∨¬P。
- typed_membership · prerequisite — 型別化的隸屬：在 G1 的語境中，x∈S 只在 x 是整數、S 是整數的集合時才是良構的命題；整數的集合本身不是整數。
- L_C · lemma — 對每個 x∈ℤ：x∈C ⇔ x∈B。





## 逐步主鏈

S01 · definition操作前

\text{a set}\ S\ \text{in the universe}\ \mathbb{Z}

操作後

A=B\iff\forall x\in\mathbb{Z}\,(x\in A\iff x\in B)

條件：無

規則：mko_set · 依賴：G1

葉節點依據：mko_set + set_extensionality

依 MKO，在指定論域中集合由「哪些對象是它的元素」刻畫，元素完全相同的集合相等。論域是 ℤ（G1），所以要證兩個集合相等，就要對任意整數 x 證明 x∈A ⇔ x∈B；要證不相等，只需找到一個整數屬於其中一個而不屬於另一個。



S02 · equivalent操作前

x\in A

操作後

x^2=4

條件：x\in\mathbb{Z}

規則：set_builder · 依賴：G2

葉節點依據：set_builder + and_intro_elim

依集合建構式，x∈A ⇔ x∈ℤ 且 x²=4。在論域 ℤ 中 x∈ℤ 已成立，所以 x∈A ⇔ x²=4。A 是在既有集合 ℤ 中以條件分出元素，這是受限的建構方式。



S03 · equivalent操作前

x^2=4

操作後

x^2-4=0

條件：無

規則：eq_congruence · 依賴：S02

葉節點依據：eq_congruence + add_inverse + add_assoc + add_zero

兩邊同加 −4；反向是兩邊同加 4。



S04 · equivalent操作前

x^2-4=0

操作後

(x-2)(x+2)=0

條件：無

規則：distributive · 依賴：S03

葉節點依據：distributive + neg_mul + add_inverse + eq_replace

依分配律 (x−2)(x+2)=x²+2x−2x−4=x²−4，對每個整數成立；等值代換不改變等式的真假。



S05 · equivalent操作前

(x-2)(x+2)=0

操作後

x-2=0\ \lor\ x+2=0

條件：無

規則：zero_product · 依賴：S04

葉節點依據：zero_product

ℤ 是整域，依零乘積性質：兩個整數的積為 0，當且僅當至少一個因子為 0。



S06 · equivalent操作前

x-2=0\ \lor\ x+2=0

操作後

x=2\ \lor\ x=-2

條件：無

規則：eq_congruence · 依賴：S05

葉節點依據：eq_congruence + add_inverse + numeric_evaluation

第一支兩邊同加 2，第二支兩邊同加 −2；兩支各自是雙向等價，所以析取前後同真同假。



S07 · equivalent操作前

x=2\ \lor\ x=-2

操作後

x\in B

條件：無

規則：list_set · 依賴：S06, G1, G2

葉節點依據：or_laws + list_set

依析取交換律改寫為 x=−2 ∨ x=2；依列舉記號（G1）這正是 x∈B。



S08 · implies操作前

\text{for arbitrary}\ x\in\mathbb{Z}:\ x\in A\iff x\in B

操作後

A=B

條件：無

規則：set_extensionality · 依賴：S02, S03, S04, S05, S06, S07

葉節點依據：logic_chain + forall_intro + set_extensionality

S02 到 S07 對任意整數 x 成立，依推論的傳遞串起來得 x∈A ⇔ x∈B；依全稱推廣與集合相等的判準，A=B。作為對照的非元素：3²=9≠4，所以 3∉A；又 3≠−2、3≠2，所以 3∉B，兩邊一致。



S09 · implies操作前

\forall x\in\mathbb{Z}:\ x\in C\iff x\in B

操作後

C=B

條件：無

規則：set_extensionality · 依賴：L_C, G2

葉節點依據：set_extensionality + list_set + or_laws

依引理 L_C（在 S09.1、S09.2 證明），每個整數 x 都有 x∈C ⇔ x∈B；依集合相等的判準，C=B。C 的寫法有三個符號、順序也不同，但集合只看元素，順序與重複都不產生新集合。



S10 · implies操作前

-2\in B,\ -2\notin D

操作後

D\neq B

條件：無

規則：contradiction · 依賴：G1, G2, list_set

葉節點依據：contradiction + set_extensionality + list_set + numeric_evaluation

依列舉記號，−2∈B（第一支 −2=−2 成立）；而 −2∈D ⇔ −2=2，但 −2≠2，所以 −2∉D。若 D=B，兩者元素相同，就會有 −2∈D，矛盾。所以 D={2}≠B。



S11 · implies操作前

2\ \text{versus}\ \{2\}

操作後

\{2\}\subseteq B\iff 2\in B;\quad \{2\}\in B\ \text{is not a true statement}

條件：無

規則：subset_def · 依賴：G1, G2, list_set, typed_membership

葉節點依據：subset_def + list_set + typed_membership

2 是整數，{2}=D 是整數的集合，兩者不是同一個對象。它們的正確關係是：依子集定義，{2}⊆B ⇔ 對每個 y，y∈{2} ⇒ y∈B；因 y∈{2} ⇔ y=2，這等價於 2∈B。2∈B 成立，所以 {2}⊆B。另一方面，依 typed_membership，B 的元素是整數，{2} 不是整數，所以「{2}∈B」在本語境中不是為真的命題（在型別化的讀法中它甚至不是良構的）。混淆 2 與 {2}，就會把 ⊆ 與 ∈ 混為一談。



S12 · implies操作前

\exists R\in U\ \forall y\in U:\ (y\in R\iff y\notin y)

操作後

\text{fix such an}\ R\in U

條件：無

規則：exists_elim · 依賴：G3

葉節點依據：exists_elim

轉到 MKO 的第二個誤解：「任意條件都能不受限制地定義集合」。若條件「y∉y」能在論域 U 中定義一個集合，就會有某個 R∈U，其元素恰好是不屬於自身的對象。為了反證，暫時假設這樣的 R 存在，並給它一個新名字 R。



S13 · implies操作前

\forall y\in U:\ (y\in R\iff y\notin y)

操作後

R\in R\iff R\notin R

條件：R\in U

規則：forall_elim · 依賴：S12

葉節點依據：forall_elim

S12 的性質對每個 y∈U 成立，而 R 本身就在 U 中，所以可以取 y=R，得 R∈R ⇔ R∉R。



S14 · case_split操作前

R\in R\iff R\notin R

操作後

R\in R\ \lor\ R\notin R

條件：無

規則：case_analysis · 依賴：S13, excluded_middle

葉節點依據：case_analysis + excluded_middle

依排中律，R∈R 或 R∉R。兩種情形在 S14.1、S14.2 中都由 S13 導出矛盾，兩支涵蓋所有可能。



S15 · implies操作前

\text{the assumption of S12 leads to a contradiction}

操作後

\neg\exists R\in U\ \forall y\in U:\ (y\in R\iff y\notin y)

條件：無

規則：contradiction · 依賴：S12, S14, S14.1, S14.2

葉節點依據：contradiction + exists_elim

S12 的暫時假設在兩個情形下都導出矛盾，依反證法，這樣的 R 不存在。這個結論對任何論域 U 與任何隸屬關係都成立，沒有用到集合論公理。所以不存在 U 內的對象 R∈U，其對 U 中各 y 的隸屬關係恰好由 y∉y 刻畫：不能要求每個條件都由 U 內的一個集合表示。這不排除在通常集合論中以受限分離形成 R={y∈U ∣ y∉y}⊆U；此時 R 不屬於 U。相對地，S02 用的是在既有集合 ℤ 中分出元素的受限形式。



S16 · implies操作前

\text{conclusions of S08, S09, S10, S11, S15}

操作後

A=B=C,\ D\neq B,\ \{2\}\subseteq B,\ \neg\exists R\in U\ \forall y\in U:\ (y\in R\iff y\notin y)

條件：無

規則：and_intro_elim · 依賴：S08, S09, S10, S11, S15

葉節點依據：and_intro_elim

合起來：以條件寫成的 A、以列舉寫成的 B、帶重複的 C 是同一個集合；D={2} 不等於 B；元素 2 與集合 {2} 以 ∈ 與 ⊆ 分別連到 B；不存在 R∈U 對所有 y∈U 滿足 y∈R ⇔ y∉y。







## 局部子步與引理

S09.1 · equivalent操作前

x\in C

操作後

x=2\lor x=-2\lor x=2

條件：無

規則：list_set · 依賴：G2, list_set

葉節點依據：list_set

依列舉記號展開 C={2,−2,2}：x∈C ⇔ x=2 ∨ x=−2 ∨ x=2。



S09.2 · equivalent操作前

x=2\lor x=-2\lor x=2

操作後

x=-2\lor x=2,\ \text{i.e.}\ x\in B

條件：無

規則：or_laws · 依賴：S09.1, or_laws

葉節點依據：or_laws + list_set

依析取的交換與結合改寫為 (x=2∨x=2)∨x=−2；依冪等律 x=2∨x=2 ⇔ x=2，得 x=2∨x=−2；再交換得 x=−2∨x=2，依列舉記號即 x∈B。S09.1 與 S09.2 合起來證得引理 L_C。



S14.1 · implies操作前

R\in R

操作後

R\notin R,\ \text{contradiction}

條件：無

規則：modus_ponens · 依賴：S13, S14

葉節點依據：modus_ponens + iff_intro

情形一：R∈R。由 S13 的「⇒」方向得 R∉R，與 R∈R 同時成立，矛盾。



S14.2 · implies操作前

R\notin R

操作後

R\in R,\ \text{contradiction}

條件：無

規則：modus_ponens · 依賴：S13, S14

葉節點依據：modus_ponens + iff_intro

情形二：R∉R。由 S13 的「⇐」方向得 R∈R，與 R∉R 同時成立，矛盾。







## 逐步反向審查


- S16 · sufficient_goal_reduction · S08, S09, S10, S11, S15, and_intro_elim — 目標 G：題目要求的四個結論。足夠條件 H：S08、S09、S10、S11、S15；H⇒G 只是並列。H 由 G1 到 G3 正向證成，沒有把 G 當作前提。
- S15 · premise_audit · S12, S14, contradiction, exists_elim — 反證的結論不含見證名字 R 的自由出現，符合 exists_elim 的限制；不宣稱任何特定公理系統中哪些條件可以形成集合（MKO 不選定 ZF 或 ZFC）。
- S14.2 · premise_audit · S13, modus_ponens, iff_intro — 只用到雙條件的另一個方向。
- S14.1 · premise_audit · S13, modus_ponens, iff_intro — 只用到雙條件的一個方向。
- S14 · premise_audit · S13, excluded_middle, case_analysis — 兩個情形涵蓋全部可能，依據是排中律。
- S13 · premise_audit · S12, forall_elim — 代入需要 R∈U，這正是「R 是論域中的一個集合」的意思。
- S12 · premise_audit · G3, exists_elim — 這是暫時假設，只在 S12 到 S14 的反證範圍內使用；最後的結論 S15 不含見證 R 的自由出現。
- S11 · premise_audit · subset_def, list_set, typed_membership — {2}⊆B ⇔ 2∈B 由子集定義與列舉記號雙向成立；「{2}∈B 不為真」只依賴型別區分，不需要其他公理。
- S10 · premise_audit · list_set, set_extensionality, contradiction — 一個屬於一邊而不屬於另一邊的元素就足以否定相等；不宣稱兩者沒有共同元素（2 屬於兩者）。
- S09.2 · inverse_equivalence · or_laws, list_set — 交換、結合、冪等都是雙向等價。
- S09.1 · inverse_equivalence · list_set — 列舉記號的定義是雙向的。
- S09 · premise_audit · L_C, set_extensionality — 需要對每個 x 的等價；引理對任意 x 證成。
- S08 · premise_audit · S02, S07, logic_chain, forall_intro, set_extensionality — 需要每個整數都比較過：x 是任取的，沒有額外假設。x=3 只是例子，不是證明的一部分。
- S07 · inverse_equivalence · or_laws, list_set — 交換律與列舉記號的定義都是雙向的。
- S06 · inverse_equivalence · eq_congruence, add_inverse, numeric_evaluation — 代回：2−2=0、(−2)+2=0。
- S05 · inverse_equivalence · zero_product — 兩個方向都包含在 zero_product 中。
- S04 · inverse_equivalence · distributive, eq_replace — 恆等式的代換雙向成立；N1 是獨立的多項式核對。
- S03 · inverse_equivalence · eq_congruence, add_inverse — 加 −4 與加 4 互為反運算，在 ℤ 中沒有附加條件。
- S02 · inverse_equivalence · set_builder, and_intro_elim — 建構式的定義本身是雙向的；拿掉已成立的合取項 x∈ℤ 也是雙向的。
- S01 · premise_audit · G1, mko_set, set_extensionality — 此步只寫出判準，不推出新事實。





## 錯誤控制與反例

元素與只含它的集合MKO 指出的常見誤解是把元素 x 與只含 x 的集合混為一談。2 是整數，{2} 是整數的集合：2∈B 與 {2}⊆B 都成立而且互相等價（S11），但「{2}∈B」不為真，{2} 也不等於 B（S10）。讀到 2 或 {2} 等記號時，先辨認它在本語境中表示整數元素，還是整數的集合，再決定用 ∈ 還是 ⊆。

不是每個條件都能形成集合MKO 的另一個誤解是認為任意條件都能不受限制地定義集合。S12 到 S15 證明：對任何論域 U，不存在 R∈U 對所有 y∈U 滿足 y∈R ⇔ y∉y。這不排除在通常集合論中以受限分離形成 R={y∈U ∣ y∉y}⊆U；此時 R∉U。所以集合的形成需要原則，例如只在已知集合中分出元素（S02 的 {x∈ℤ ∣ x²=4}）；本稿不選定具體公理系統。

順序與重複不產生新集合C={2,−2,2} 寫了三個符號，但依外延性 C=B={−2,2}（S09）。若要區分順序或重數，需要另一種對象，例如有序三元組 (2,−2,2) 或多重集合；它們不是本 MKO 所說的集合。


- {2,−2,2} 有三個元素，所以與 {−2,2} 不同 → reject — x∈{2,−2,2} ⇔ x=−2∨x=2，與 B 的元素相同，依外延性相等（S09）。
- 2 與 {2} 是同一個東西 → reject — 2 是整數，{2} 是整數的集合；2∈B 成立而「{2}∈B」不為真（S11）。
- 對任何條件 P(y)，{y ∣ P(y)} 都是集合 → reject — 取 P(y) 為 y∉y，S12 到 S15 導出矛盾。
- A 用條件寫、B 用列舉寫，所以 A≠B → reject — 集合由元素決定，與寫法無關；S08 證明 A=B。





## 結論與限制

在論域 ℤ 中，A={x∈ℤ ∣ x²=4}、B={−2,2}、C={2,−2,2} 有相同元素，所以 A=B=C；D={2}≠B，因為 −2∈B 而 −2∉D。2 是整數，{2} 是集合：2∈B 與 {2}⊆B 成立，而「{2}∈B」不為真。在任何帶有隸屬關係的論域 U 中，都不存在 R∈U 對所有 y∈U 滿足 y∈R ⇔ y∉y；這禁止不受限制地要求每個條件都由 U 內的集合表示，並不禁止在通常集合論中以受限分離形成 R={y∈U ∣ y∉y}⊆U（此時 R∉U）。


- 前半的型別化語境（typed_membership）是本稿的前提，對應 MKO 的「指定論域或型別」；在不分型別的集合論中，2 與 {2} 的關係取決於所選公理與數的編碼，本稿不處理。
- 羅素論證只證明不存在 U 內的 R∈U 對 U 中所有 y 表示條件 y∉y，並未否定受限分離形成的子集 R⊆U；哪些條件可以形成集合由具體公理系統決定（MKO 第三段），本稿不選定。





## 驗證及來源綁定

9 個本稿宣告算術檢查；只支持所列算式。


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 81bb053444cb9fae0c721ca4c93b2655272c5d7fc28922dbed489183ee255de8
- original source SHA-256: 81bb053444cb9fae0c721ca4c93b2655272c5d7fc28922dbed489183ee255de8
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-set-01.json)