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

目標與範圍

在論域 ℤ 中，設 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。

逐步主鏈

\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)

x\in A

x^2=4

x^2=4

x^2-4=0

x^2-4=0

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

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

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

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

x=2\ \lor\ x=-2

x=2\ \lor\ x=-2

x\in B

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

A=B

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

C=B

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

D\neq B

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

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

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

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

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

R\in R\iff R\notin R

R\in R\iff R\notin R

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

\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)

\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)

局部子步與引理

x\in C

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

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

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

R\in R

R\notin R,\ \text{contradiction}

R\notin R

R\in R,\ \text{contradiction}

逐步反向審查

• 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、反控制與修訂記錄）