等價關係：在完整有限關係表上逐項核對三公理並輸出等價類

目標與範圍

在 X={0,1,2,3,4} 上，關係 R 完整列出為 13 個有序對：(0,0)、(1,1)、(2,2)、(3,3)、(4,4)、(0,2)、(2,0)、(1,3)、(3,1)、(1,4)、(4,1)、(3,4)、(4,3)。逐項核對反身、對稱、傳遞，證明 R 是等價關係並輸出等價類；再說明去掉 (3,4)、(4,3) 後的 R′ 雖反身且對稱，卻不是等價關係。

只在 MKO 的範圍內：載體標籤 0 到 n−1、關係由互異有序對完整列出（假設 a1）；三項全部通過後才輸出等價類，單一反例足以否證對應公理（假設 a2）。傳遞性以「區塊關係」引理一次涵蓋全部可串接對，而非抽樣。不處理商集與基數比較，不改動 canonical MKO 或英文 edition。

已知條件與符號

• cartesian_product_def
• set_extensionality
• set_operations_def
• relation_def
• finite_forall

• G1 — X={0,1,2,3,4}；R={(0,0),(1,1),(2,2),(3,3),(4,4),(0,2),(2,0),(1,3),(3,1),(1,4),(4,1),(3,4),(4,3)}，13 個互異有序對，完整列出。
• G2 — 對照：R′ 是從 R 去掉 (3,4) 與 (4,3) 後的 11 個有序對。

• X — 載體 {0,1,2,3,4}
• R,\ R' — 完整列出的關係與去掉兩對後的對照關係
• xRy — (x,y)∈R
• B_1,\ B_2 — 區塊 {0,2} 與 {1,3,4}
• T — 區塊關係 B_1×B_1 ∪ B_2×B_2
• [x] — x 的等價類 {y∈X : xRy}

規則與來源

• cartesian_product_def · prerequisite — 笛卡兒積：A×B 是所有有序對 (a,b)（a∈A、b∈B）的集合；(a,b)=(c,d) ⇔ a=c 且 b=d。
• set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
• set_operations_def · prerequisite — 集合運算：x∈A∪B ⇔ x∈A 或 x∈B；x∈A∩B ⇔ x∈A 且 x∈B；x∈A∖B ⇔ x∈A 且 x∉B；在全集 U 中 Aᶜ=U∖A。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
• finite_counting_basics · prerequisite — 有限計數：互斥有限集合 A、B 有 |A∪B|=|A|+|B|；|A×B|=|A|·|B|；有限集之間存在雙射 ⇔ 元素個數相同。
• subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。
• eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
• exists_elim · prerequisite — ∃消去：由 ∃x∈D, P(x)，可取一個新名字 a 表示某個滿足 P(a) 的元素；只要最後結論不含 a，就可用 a 推理。
• contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
• forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
• quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
• de_morgan_logic · prerequisite — 邏輯的德摩根律：¬(P∧Q) ⇔ ¬P∨¬Q；¬(P∨Q) ⇔ ¬P∧¬Q。
• mko_equiv_def · cited — 關係R在集合X上為等價關係，若每個x都有xRx；xRy推出yRx；xRy且yRz推出xRz。本輪在完整有限載體與完整關係對集合上逐項核對。 · mko-equivalence-relation
• relation_def · prerequisite — X 上的關係是子集 R⊆X×X；xRy 表示 (x,y)∈R。完整列出時，未列出的有序對不在 R 中。
• finite_forall · prerequisite — 有限全稱：對有限集合 D，「對所有 t∈D，Φ(t)」等價於把 D 的每個元素逐一代入所得命題的合取；列表必須完整。
• eq_class_def · prerequisite — 等價類：R 為等價關係時，[x]={y∈X : xRy}。依 MKO，只有三項公理都通過後才輸出等價類。
• L_block_trans · lemma — 若 B_1、B_2 是 X 的兩兩不交子集，則 T=(B_1×B_1)∪(B_2×B_2) 是傳遞關係：(x,y)∈T 且 (y,z)∈T 推出 (x,z)∈T。

逐步主鏈

R\ \text{is an equivalence relation on}\ X

\forall x\,(xRx)\ \land\ \forall x,y\,(xRy\Rightarrow yRx)\ \land\ \forall x,y,z\,(xRy\land yRz\Rightarrow xRz)

\forall x\in X:\ (x,x)\in R

(0,0),(1,1),(2,2),(3,3),(4,4)\in R

\forall (x,y)\in R:\ (y,x)\in R

(0,2)\leftrightarrow(2,0),\ (1,3)\leftrightarrow(3,1),\ (1,4)\leftrightarrow(4,1),\ (3,4)\leftrightarrow(4,3);\ (x,x)\ \text{self-reverse}

X=\{0,1,2,3,4\}

B_1=\{0,2\},\ B_2=\{1,3,4\},\ T=(B_1\times B_1)\cup(B_2\times B_2)

(B_1\times B_1)\cup(B_2\times B_2)

\{(0,0),(0,2),(2,0),(2,2)\}\cup\{(1,1),(1,3),(1,4),(3,1),(3,3),(3,4),(4,1),(4,3),(4,4)\}

(x,y)\in R

R\subseteq T

R\subseteq T,\ (x,y)\in T

T\subseteq R,\ \text{hence}\ R=T

R=T=(B_1\times B_1)\cup(B_2\times B_2),\ B_1\cap B_2=\varnothing

xRy\land yRz\Rightarrow xRz\ \text{for all}\ x,y,z\in X

\text{reflexive, symmetric, transitive}

R\ \text{is an equivalence relation on}\ X

[x]=\{y\in X: xRy\}

[0]=[2]=\{0,2\},\ [1]=[3]=[4]=\{1,3,4\}

\{0,2\},\ \{1,3,4\}

\{0,2\}\cap\{1,3,4\}=\varnothing,\ \{0,2\}\cup\{1,3,4\}=X

R'=R\setminus\{(3,4),(4,3)\}

R'\ \text{reflexive and symmetric}

(3,1)\in R',\ (1,4)\in R'

(3,4)\notin R'\Rightarrow R'\ \text{not transitive}

R'\ \text{reflexive, symmetric, not transitive}

R'\ \text{not an equivalence relation; no classes emitted}

局部子步與引理

(x,y)\in T,\ (y,z)\in T

(x,y)\in B_i\times B_i,\ (y,z)\in B_j\times B_j,\ y\in B_i\cap B_j

y\in B_i\cap B_j,\ B_1\cap B_2=\varnothing

i=j

x\in B_i,\ z\in B_j,\ i=j

(x,z)\in B_i\times B_i\subseteq T

逐步反向審查

• S14 · sufficient_goal_reduction · S01, S13 — 目標 G：R′ 不是等價關係。足夠條件 H：某一項公理失敗；H⇒G 由定義（三項缺一不可）。H 由 S13 正向給出。
• S13 · premise_audit · G2, contradiction — 需要 R′ 的列表完整，才能確定 (3,4)∉R′。只要一個反例，不需檢查其他串接。
• S12 · premise_audit · G2, finite_forall — R′ 的 11 對都已檢查（5+2·3=11）；此步不宣稱 R′ 傳遞。
• S11 · premise_audit · S10, set_operations_def — 只對這兩個具體集合做交集與聯集的計算；不在此一般地證明等價類必構成分割。
• S10 · premise_audit · S09, eq_class_def — 輸出等價類的前提是 S09；若三項未全部通過（如 R′），按 MKO 不輸出。
• S09 · sufficient_goal_reduction · S01, S02, S03, S08 — 目標 G：R 是等價關係。足夠條件 H：三項公理都成立；H⇒G 由定義。H 由 S02、S03、S08 正向證成，沒有把 G 當作前提。
• S08.3 · premise_audit · S08.2, cartesian_product_def, forall_intro — 證明沒有對 x、y、z 加任何額外假設，所以可以全稱推廣；此子步不使用 L_block_trans。
• S08.2 · premise_audit · S08.1, contradiction — 反證法的前提是區塊不交；此子步不使用 L_block_trans。
• S08.1 · premise_audit · set_operations_def, cartesian_product_def — 只是展開聯集與笛卡兒積的成員資格；此子步不使用 L_block_trans。
• S08 · premise_audit · S07, L_block_trans — 需要 R=T 完全相等（S07）與區塊不交（S04）；若只有 R⊆T，T 的傳遞性不能轉移到 R。
• S07 · premise_audit · S06, set_extensionality — 兩個包含都由逐元素檢查得到；只有兩個方向都成立才能宣稱相等。
• S06 · premise_audit · G1, S05, subset_def — 只證 R⊆T；反向包含在 S07 另外證明。
• S05 · inverse_equivalence · cartesian_product_def, set_extensionality — 列出的集合與定義的集合逐元素相同，雙向成立。
• S04 · premise_audit · def_intro — 定義不推出事實；B_1∩B_2=∅ 可直接看出，之後的引理需要這一點。
• S03 · inverse_equivalence · finite_forall, relation_def — 13 對全部配對完畢（5+2·4=13），沒有遺漏，所以逐項成立與全稱成立等價。
• S02 · inverse_equivalence · finite_forall — 全稱推出每個實例；五個實例涵蓋 X 全部元素時，反之亦然。
• S01 · premise_audit · mko_equiv_def, relation_def — 此步只展開定義，列出三項責任，不推出新事實。

錯誤控制與反例

只核反身與對稱不夠

MKO 指出的常見誤解是只核反身與對稱就叫等價關係。R′ 兩項都通過（S12），但 3R′1、1R′4 而 (3,4)∉R′（S13）。傳遞性是獨立的第三項責任。

不要看圖分群

畫出 R′ 的關係圖，0、2 一群，1、3、4 看起來也連成一群；但 R′ 的「類」{1,3} 與 {1,4} 相交而不相等。等價類只能在三項核對全部通過後由關係本身讀出（S10）。

傳遞性要涵蓋全部可串接對

R 的可串接對 (x,y)、(y,z) 共有 2·2²+3·3²=35 組。抽查幾組（例如 (0,2)、(2,0) 推出 (0,0)）不構成證明；本稿用 R=T 與引理 L_block_trans 一次涵蓋全部 35 組。

• R′ 反身且對稱，所以 R′ 是等價關係 → reject — 3R′1、1R′4，但 (3,4)∉R′，傳遞性失敗。
• 對稱且傳遞的關係一定反身 → reject — 在 {0,1,2} 上，S={0,1}×{0,1} 對稱且傳遞（單一區塊），但 (2,2)∉S。
• R′ 的串接 (0,2)、(2,0) 推出 (0,0)∈R′，所以 R′ 傳遞 → reject — 一組串接成立不代表全部成立；(3,1)、(1,4) 這組失敗。
• R′ 的等價類是 {0,2} 與 {1,3,4} → reject — R′ 不是等價關係，不輸出等價類；硬算得到的 {1,3} 與 {1,4} 也不構成分割。

結論與限制

R 反身（5 個對角對）、對稱（4 組反向配對）且傳遞（R 等於區塊關係 (B_1×B_1)∪(B_2×B_2)，由引理 L_block_trans 涵蓋全部 35 個可串接對），所以 R 是等價關係，等價類為 {0,2} 與 {1,3,4}。R′ 反身且對稱，但 3R′1、1R′4 而非 3R′4，所以不是等價關係，不輸出等價類。

• 本稿不一般地證明「等價類構成載體的分割」；S11 只對本例的兩個集合核對。
• finite_forall、relation_def 與 eq_class_def 是本稿的前提。

驗證及來源綁定

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 90ad3357e3d147bcb375215a2ad86359916fc907de884703d58672c5ebc480e1
• original source SHA-256: 90ad3357e3d147bcb375215a2ad86359916fc907de884703d58672c5ebc480e1
• Lean: NOT_RUN · independent AI: NOT_MEASURED

同源完整 JSON（含公式、AST、反控制與修訂記錄）