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

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

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

derivation-mko-equivalence-relation-01 · production-20261019-adopted-96



## 目標與範圍

在 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。





## 逐步主鏈

S01 · definition操作前

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)

條件：無

規則：mko_equiv_def · 依賴：G1, relation_def

葉節點依據：mko_equiv_def + def_unfold

依 MKO 展開定義：三項公理反身、對稱、傳遞都必須成立。每一項都是對有限集合的全稱命題，所以可以完整核對；任何一項有一個反例，R 就不是等價關係。



S02 · equivalent操作前

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

操作後

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

條件：無

規則：finite_forall · 依賴：S01, G1, finite_forall

葉節點依據：finite_forall + relation_def

X 有五個元素，反身性等價於五個對角對都在 R 中。逐一查 G1 的列表：五個都在。反身性成立。



S03 · equivalent操作前

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

條件：無

規則：finite_forall · 依賴：S01, G1, finite_forall

葉節點依據：finite_forall + relation_def + numeric_evaluation

對稱性只需檢查 R 中的每一對（xRy 為假時蘊含自動成立）。13 對中，5 個對角對的反向是自己；其餘 8 對成 4 組互為反向，每組兩對都在列表中。對稱性成立。



S04 · definition操作前

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)

條件：無

規則：def_intro · 依賴：G1

葉節點依據：def_intro + set_operations_def

為了一次處理全部可串接對，引入兩個候選區塊與區塊關係 T。B_1 與 B_2 不交，聯集是 X。這只是命名，T 是否等於 R 要在 S05 到 S07 證明，不能只看圖猜。



S05 · equivalent操作前

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

條件：無

規則：cartesian_product_def · 依賴：S04, cartesian_product_def

葉節點依據：cartesian_product_def + finite_counting_basics

依笛卡兒積定義列出：B_1×B_1 有 2·2=4 對，B_2×B_2 有 3·3=9 對。兩個積不交（區塊不交），所以 |T|=4+9=13。



S06 · implies操作前

(x,y)\in R

操作後

R\subseteq T

條件：無

規則：subset_def · 依賴：G1, S05

葉節點依據：subset_def + finite_forall

逐一檢查 R 的 13 對：五個對角對各在自己的區塊積中；(0,2)、(2,0) 兩端都在 B_1；(1,3)、(3,1)、(1,4)、(4,1)、(3,4)、(4,3) 兩端都在 B_2。每一對都在 T 中。



S07 · implies操作前

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

操作後

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

條件：無

規則：set_extensionality · 依賴：S05, S06, G1

葉節點依據：set_extensionality + subset_def + finite_counting_basics

S05 列出的 T 的 13 對，每一對都出現在 G1 的 R 列表中，所以 T⊆R。結合 S06 的 R⊆T，依集合外延性 R=T。（另一個核對：兩者都恰有 13 個互異元素。）



S08 · theorem_application操作前

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

條件：B_1\cap B_2=\varnothing

規則：L_block_trans · 依賴：S04, S07

葉節點依據：L_block_trans + eq_replace

依引理 L_block_trans（S08.1 到 S08.3 證明），T 是傳遞的；因 R=T，R 也是傳遞的。這一次涵蓋全部 35 個可串接的 (x,y)、(y,z)，不是抽樣。



S09 · implies操作前

\text{reflexive, symmetric, transitive}

操作後

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

條件：無

規則：and_intro_elim · 依賴：S01, S02, S03, S08

葉節點依據：mko_equiv_def + and_intro_elim

反身（S02）、對稱（S03）、傳遞（S08）三項都通過，依 S01 的定義 R 是等價關係。到這裡才允許輸出等價類。



S10 · implies操作前

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

操作後

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

條件：R\ \text{equivalence relation (S09)}

規則：eq_class_def · 依賴：S09, G1, eq_class_def

葉節點依據：eq_class_def + set_builder + relation_def

讀出每個 x 對應的行：以 0 開頭的對是 (0,0)、(0,2)，所以 [0]={0,2}；以 2 開頭的是 (2,2)、(2,0)，[2]={0,2}；以 1 開頭的是 (1,1)、(1,3)、(1,4)，[1]={1,3,4}；以 3 開頭的是 (3,3)、(3,1)、(3,4)；以 4 開頭的是 (4,4)、(4,1)、(4,3)，所以 [3]=[4]={1,3,4}。



S11 · implies操作前

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

操作後

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

條件：無

規則：set_operations_def · 依賴：S10

葉節點依據：set_operations_def + finite_counting_basics

兩個相異的等價類不交，聯集是 X，2+3=5=|X|。它們恰是 S04 的兩個區塊：區塊是由驗證後的關係得到的，不是先由圖猜出的。



S12 · implies操作前

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

操作後

R'\ \text{reflexive and symmetric}

條件：無

規則：finite_forall · 依賴：G2, S02, S03

葉節點依據：finite_forall + relation_def + numeric_evaluation

R′ 保留全部五個對角對，所以仍反身；去掉的兩對互為反向，其餘 3 組反向配對 (0,2)/(2,0)、(1,3)/(3,1)、(1,4)/(4,1) 都完整保留，所以仍對稱。



S13 · implies操作前

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

操作後

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

條件：無

規則：contradiction · 依賴：G2, S12

葉節點依據：contradiction + quantifier_negation + relation_def

取 x=3、y=1、z=4：3R′1 且 1R′4，但 (3,4) 已被去掉，3R′4 不成立。傳遞性是全稱命題，一個反例就否證它。



S14 · implies操作前

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

操作後

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

條件：無

規則：mko_equiv_def · 依賴：S01, S12, S13, eq_class_def

葉節點依據：mko_equiv_def + de_morgan_logic

缺少傳遞性，依 S01 R′ 不是等價關係，不輸出等價類。若硬算 {y : xR′y}，會得到 {1,3}（x=3）與 {1,4}（x=4），兩者相交於 1 卻不相等，不構成分割。這顯示反身加對稱不足，也顯示看圖分群不可靠。







## 局部子步與引理

S08.1 · implies操作前

(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

條件：無

規則：set_operations_def · 依賴：cartesian_product_def, set_operations_def

葉節點依據：set_operations_def + cartesian_product_def + exists_elim

取任意 x、y、z 使 (x,y)、(y,z) 都在 T 中。T 是兩個積的聯集，所以有某個 i 使 (x,y)∈B_i×B_i，有某個 j 使 (y,z)∈B_j×B_j。由笛卡兒積定義，y 既在 B_i（第二座標）也在 B_j（第一座標）。



S08.2 · implies操作前

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

操作後

i=j

條件：B_1\cap B_2=\varnothing

規則：contradiction · 依賴：S08.1, contradiction

葉節點依據：contradiction + set_operations_def

若 i≠j，則 {i,j}={1,2}，y∈B_1∩B_2=∅，矛盾。所以 i=j。這裡用到區塊兩兩不交；若區塊相交，這一步會失敗。



S08.3 · implies操作前

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

操作後

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

條件：無

規則：cartesian_product_def · 依賴：S08.1, S08.2, forall_intro

葉節點依據：cartesian_product_def + forall_intro

由 S08.1，x∈B_i、z∈B_j，而 S08.2 給 i=j，所以 x、z 都在 B_i，(x,z)∈B_i×B_i⊆T。x、y、z 是任意取的，依全稱推廣，T 是傳遞的。S08.1 到 S08.3 合起來證得引理 L_block_trans。







## 逐步反向審查


- 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、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-equivalence-relation-01.json)