# 二元關係：定義域、關係像與逆關係的逐步計算 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-relation/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-relation-01 · production-20261019-adopted-96 ## 目標與範圍 設 A={1,2,3,4}、B={2,3,4,5,6}、R={(1,2),(1,3),(3,3),(4,6)}、C={1,3}。核對 R⊆A×B；計算 Dom(R)、R[C]、R[∅]、R⁻¹ 與 Dom(R⁻¹)；判定 R 是否為函數 A→B、R⁻¹ 是否為函數 B→A。 在 MKO 的範圍內工作：明示的有限整數集合與有序對資料。依 MKO 的定義逐步計算定義域、關係像與逆關係，並證明三個一般小引理（逆關係的成員條件、Dom(R⁻¹)=R[A]、(R⁻¹)⁻¹=R）。函數條件只作為額外限制來判定；不處理關係合成、等價關係或序關係；不改動 canonical MKO 或英文 edition。 ## 已知條件與符號 - cartesian_product_def - subset_def - set_builder - set_extensionality - exists_intro - roster_membership - G1 — 來源 A={1,2,3,4}，目標 B={2,3,4,5,6}，都以列舉明示。 - G2 — R={(1,2),(1,3),(3,3),(4,6)}，以列舉完整給出，宣告為從 A 到 B 的關係；有序對保留方向（MKO 假設 a2）。 - G3 — C={1,3}⊆A（MKO 假設 a1）。 - A,\ B — 來源 {1,2,3,4} 與目標 {2,3,4,5,6} - R — 從 A 到 B 的關係，即 A×B 的子集合 - \mathrm{Dom}(R) — 關係定義域：實際有出邊的第一分量 - R[C] — C 在 R 下的關係像 - R^{-1} — 逆關係 {(y,x) ∣ (x,y)∈R}⊆B×A ## 規則與來源 - cartesian_product_def · prerequisite — 笛卡兒積：A×B 是所有有序對 (a,b)（a∈A、b∈B）的集合；(a,b)=(c,d) ⇔ a=c 且 b=d。 - subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。 - set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。 - set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。 - exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。 - forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。 - case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。 - quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。 - numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。 - eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。 - logic_chain · prerequisite — 推論的傳遞：由 P⇒Q 與 Q⇒R 得 P⇒R；⇔ 同理。 - and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。 - mko_relation_def · cited — 對集合 A、B，從 A 到 B 的二元關係 R 是 A×B 的子集合；xRy 表示 (x,y)∈R。關係定義域 Dom(R)={x∈A:存在 y∈B，使 (x,y)∈R}，關係像 R[C]={y∈B:存在 x∈C，使 (x,y)∈R}，逆關係 R⁻¹={(y,x):(x,y)∈R}⊆B×A。 · mko-relation - roster_membership · prerequisite — 列舉集合的成員關係：對以列舉給出的有限集合 S={s_i ∣ 1≤i≤n}，z∈S 當且僅當存在 i（1≤i≤n）使 z=s_i。 - empty_set_def · prerequisite — 空集合：對每個 x，x∉∅。 - function_graph · prerequisite — 關係 F⊆X×Y 是總函數 X→Y（的圖形），當且僅當每個 x∈X 恰有一個 y∈Y 使 (x,y)∈F：至少一個（總定義）且至多一個（單值）。 - L_converse_member · lemma — 對任何關係 S⊆X×Y 與任何 x、y：(y,x)∈S⁻¹ ⇔ (x,y)∈S。 - L_dom_converse · lemma — 對任何關係 R⊆A×B：Dom(R⁻¹)=R[A]，其中 Dom(R⁻¹)={y∈B ∣ 存在 x∈A 使 (y,x)∈R⁻¹}。 - L_converse_twice · lemma — 對任何關係 R⊆A×B：(R⁻¹)⁻¹=R。 ## 逐步主鏈 S01 · implies操作前 R=\{(1,2),(1,3),(3,3),(4,6)\} 操作後 R\subseteq A\times B 條件：無 規則：subset_def · 依賴：G1, G2, subset_def, cartesian_product_def, roster_membership 葉節點依據：subset_def + cartesian_product_def + roster_membership 依子集定義，要檢查 R 的每個元素都在 A×B 中。R 以列舉給出四個有序對；每一對的第一分量要在 A、第二分量要在 B：(1,2)：1∈A、2∈B；(1,3)：1∈A、3∈B；(3,3)：3∈A、3∈B；(4,6)：4∈A、6∈B。四對都合格，所以 R⊆A×B，R 確實是從 A 到 B 的二元關係。 S02 · equivalent操作前 x\in\mathrm{Dom}(R) 操作後 x\in A\ \land\ \exists y\in B:\ (x,y)\in R 條件：無 規則：mko_relation_def · 依賴：mko_relation_def, S01 葉節點依據：mko_relation_def + set_builder 依 MKO，Dom(R)={x∈A ∣ 存在 y∈B 使 (x,y)∈R}。由集合建構式，x∈Dom(R) 當且僅當 x∈A 且有某個 y∈B 使 (x,y)∈R。Dom(R) 由 R 的資料決定，不是宣告來源 A 的別名。 S03 · implies操作前 (1,2)\in R,\ (3,3)\in R,\ (4,6)\in R 操作後 1,3,4\in\mathrm{Dom}(R) 條件：無 規則：exists_intro · 依賴：S02, G2, exists_intro 葉節點依據：exists_intro + set_builder 找見證：(1,2)∈R 給 x=1 的見證 y=2；(3,3)∈R 給 x=3 的見證 y=3；(4,6)∈R 給 x=4 的見證 y=6。見證都在 B 中，1、3、4 都在 A 中，依 ∃引入與 S02，1、3、4∈Dom(R)。1 還有第二個見證 y=3，但一個就夠。 S04 · implies操作前 y\in B,\quad (2,y)\in R\ ? 操作後 \forall y\in B:\ (2,y)\notin R 條件：無 規則：cartesian_product_def · 依賴：G2, roster_membership, cartesian_product_def, forall_intro 葉節點依據：roster_membership + cartesian_product_def + forall_intro + case_analysis 任取 y∈B。由列舉，(2,y)∈R 當且僅當 (2,y) 等於 (1,2)、(1,3)、(3,3)、(4,6) 之一。有序對相等需要第一分量相等，即 2=1、2=1、2=3 或 2=4，四者皆假（N2 以乘積 (2−1)(2−1)(2−3)(2−4)≠0 核對）。所以 (2,y)∉R；y 是任意的，依 ∀引入得結論。 S05 · implies操作前 \forall y\in B:\ (2,y)\notin R 操作後 2\notin\mathrm{Dom}(R) 條件：無 規則：quantifier_negation · 依賴：S02, S04, quantifier_negation 葉節點依據：quantifier_negation + set_builder 依量詞否定律，∀y∈B (2,y)∉R 等價於 ¬∃y∈B (2,y)∈R。由 S02，2∈Dom(R) 需要這樣的 y，所以 2∉Dom(R)。2 屬於宣告來源 A，卻沒有任何出邊。 S06 · implies操作前 1,3,4\in\mathrm{Dom}(R),\ 2\notin\mathrm{Dom}(R),\ \mathrm{Dom}(R)\subseteq A 操作後 \mathrm{Dom}(R)=\{1,3,4\}\neq A 條件：無 規則：set_extensionality · 依賴：S03, S05, G1, set_extensionality 葉節點依據：set_extensionality + subset_def + roster_membership ⊇：S03。⊆：Dom(R)⊆A={1,2,3,4}，而 2 已被 S05 排除，所以 Dom(R) 的元素只能是 1、3、4。依集合相等，Dom(R)={1,3,4}。因 2∈A∖Dom(R)，Dom(R)≠A。 S07 · implies操作前 2\notin\mathrm{Dom}(R),\ (1,2)\in R,\ (1,3)\in R 操作後 R\ \text{is not a function}\ A\to B 條件：無 規則：function_graph · 依賴：S05, G2, function_graph 葉節點依據：function_graph + numeric_evaluation 函數 A→B 要求每個 x∈A 恰有一個 y。R 有兩處不符：2 沒有任何 y（S05，不是總定義）；1 有兩個 y，即 2 與 3，且 2≠3（不是單值）。任一處就足以否定。MKO 第一段指出關係不必是總函數。 S08 · implies操作前 y\in R[C],\quad C=\{1,3\} 操作後 2\in R[C],\ 3\in R[C] 條件：無 規則：mko_relation_def · 依賴：mko_relation_def, G2, G3, exists_intro 葉節點依據：mko_relation_def + exists_intro + set_builder 依 MKO，y∈R[C] 當且僅當 y∈B 且有某個 x∈C 使 (x,y)∈R。第一分量在 C={1,3} 的對是 (1,2)、(1,3)、(3,3)，給出輸出 2、3、3。依 ∃引入，2∈R[C]（見證 x=1），3∈R[C]（見證 x=1 或 x=3）。 S09 · implies操作前 2,3\in R[C] 操作後 R[C]=\{2,3\} 條件：無 規則：set_extensionality · 依賴：S08, G2, G3, set_extensionality 葉節點依據：set_extensionality + roster_membership + cartesian_product_def ⊆：B 的其餘元素是 4、5、6。R 中沒有第二分量為 4 或 5 的對；第二分量為 6 的只有 (4,6)，其第一分量 4∉C（N4：(4−1)(4−3)≠0）。所以 4、5、6∉R[C]。合併 S08，R[C]={2,3}。輸出 3 出現兩次（來自 (1,3) 與 (3,3)），在集合中只列一次。 S10 · implies操作前 R[\varnothing] 操作後 R[\varnothing]=\varnothing 條件：無 規則：mko_relation_def · 依賴：mko_relation_def, empty_set_def 葉節點依據：mko_relation_def + empty_set_def + quantifier_negation + set_extensionality y∈R[∅] 需要某個 x∈∅ 使 (x,y)∈R；∅ 沒有元素，所以對每個 y 這都不成立，R[∅]=∅。這正是 MKO 第二段所說：空輸入集合的像為空。 S11 · implies操作前 R=\{(1,2),(1,3),(3,3),(4,6)\} 操作後 R^{-1}=\{(2,1),(3,1),(3,3),(6,4)\}\subseteq B\times A 條件：無 規則：mko_relation_def · 依賴：mko_relation_def, G2, L_converse_member 葉節點依據：mko_relation_def + cartesian_product_def + set_extensionality 依 MKO，R⁻¹={(y,x) ∣ (x,y)∈R}：把每一對交換方向。(1,2)→(2,1)、(1,3)→(3,1)、(3,3)→(3,3)、(4,6)→(6,4)。各對第一分量 2、3、3、6 在 B 中，第二分量 1、1、3、4 在 A 中，所以 R⁻¹⊆B×A：來源與目標也一起交換。由 L_converse_member，R⁻¹ 恰好由這四對組成。 S12 · implies操作前 (1,2)\in R,\ (2,1)\in R^{-1} 操作後 (2,1)\notin R,\ \text{so}\ R^{-1}\neq R 條件：無 規則：set_extensionality · 依賴：S01, S11, set_extensionality 葉節點依據：set_extensionality + cartesian_product_def + subset_def 有序對保留方向：(2,1)∈R⁻¹，但 (2,1)∉R，因為 R⊆A×B（S01）而第二分量 1∉B。依集合相等，R⁻¹≠R。雖然 A 與 B 有共同標籤 2、3、4，(1,2) 與 (2,1) 仍是不同的有序對。 S13 · theorem_application操作前 \mathrm{Dom}(R^{-1}) 操作後 \mathrm{Dom}(R^{-1})=R[A]=\{2,3,6\} 條件：無 規則：L_dom_converse · 依賴：S11, L_dom_converse 葉節點依據：mko_relation_def + set_extensionality + exists_intro 依引理 L_dom_converse，Dom(R⁻¹)=R[A]。計算 R[A]：R 的四對第一分量都在 A 中，所以全部計入，輸出為 2、3、3、6，集合為 {2,3,6}。直接核對：R⁻¹ 各對的第一分量是 2、3、3、6，一致。B 中的 4、5 不在其中。 S14 · implies操作前 R^{-1}=\{(2,1),(3,1),(3,3),(6,4)\} 操作後 R^{-1}\ \text{is not a function}\ B\to A 條件：無 規則：function_graph · 依賴：S11, S13, function_graph 葉節點依據：function_graph + roster_membership 函數 B→A 要求每個 y∈B 恰有一個 x。4∈B 不在 Dom(R⁻¹)={2,3,6} 中（N5），沒有任何 x；3 有兩個 x，即 1 與 3。所以 R⁻¹ 不是函數。逆關係總是存在，但它不自動是反函數，也不提供單射、滿射或可逆性的證明（MKO 第三段）。 S15 · theorem_application操作前 (R^{-1})^{-1} 操作後 (R^{-1})^{-1}=R 條件：無 規則：L_converse_twice · 依賴：S11, L_converse_twice 葉節點依據：mko_relation_def + set_extensionality 依引理 L_converse_twice，再交換一次就回到 R：(2,1)→(1,2)、(3,1)→(1,3)、(3,3)→(3,3)、(6,4)→(4,6)，正是 R 的四對。取逆關係這個運算在關係層次可以還原，這與 R⁻¹ 是否為函數無關。 S16 · implies操作前 \text{S01, S06, S07, S09, S10, S11, S13, S14} 操作後 \mathrm{Dom}(R)=\{1,3,4\},\ R[C]=\{2,3\},\ R[\varnothing]=\varnothing,\ \mathrm{Dom}(R^{-1})=\{2,3,6\} 條件：無 規則：and_intro_elim · 依賴：S01, S06, S07, S09, S10, S11, S13, S14 葉節點依據：and_intro_elim 彙整：R⊆A×B（S01）；Dom(R)={1,3,4}≠A（S06）；R 不是函數 A→B（S07）；R[C]={2,3}（S09）；R[∅]=∅（S10）；R⁻¹={(2,1),(3,1),(3,3),(6,4)}⊆B×A（S11）；Dom(R⁻¹)=R[A]={2,3,6}（S13）；R⁻¹ 不是函數 B→A（S14）。 ## 局部子步與引理 S11.1 · equivalent操作前 (y,x)\in S^{-1} 操作後 (x,y)\in S 條件：S\subseteq X\times Y 規則：cartesian_product_def · 依賴：mko_relation_def, cartesian_product_def 葉節點依據：mko_relation_def + cartesian_product_def + eq_replace 對任何關係 S⊆X×Y。⇐：若 (x,y)∈S，依定義 (y,x)∈S⁻¹。⇒：若 (y,x)∈S⁻¹，則 (y,x)=(y′,x′) 對某個 (x′,y′)∈S；有序對相等給出 y=y′、x=x′，所以 (x,y)=(x′,y′)∈S。這證得引理 L_converse_member。 S13.1 · equivalent操作前 y\in\mathrm{Dom}(R^{-1}) 操作後 y\in R[A] 條件：無 規則：L_converse_member · 依賴：mko_relation_def, L_converse_member, set_extensionality 葉節點依據：mko_relation_def + set_builder + set_extensionality + logic_chain 對 R⁻¹⊆B×A 套用 MKO 的定義域定義：y∈Dom(R⁻¹) ⇔ y∈B 且 ∃x∈A (y,x)∈R⁻¹。由 L_converse_member，(y,x)∈R⁻¹ ⇔ (x,y)∈R，所以上式 ⇔ y∈B 且 ∃x∈A (x,y)∈R ⇔ y∈R[A]（取 C=A）。依集合相等，Dom(R⁻¹)=R[A]。這證得引理 L_dom_converse。 S15.1 · equivalent操作前 (x,y)\in(R^{-1})^{-1} 操作後 (x,y)\in R 條件：無 規則：L_converse_member · 依賴：L_converse_member, set_extensionality 葉節點依據：set_extensionality + logic_chain + cartesian_product_def 對關係 R⁻¹ 套用 L_converse_member：(x,y)∈(R⁻¹)⁻¹ ⇔ (y,x)∈R⁻¹；再對 R 套用一次：(y,x)∈R⁻¹ ⇔ (x,y)∈R。兩集合的元素相同，依集合相等 (R⁻¹)⁻¹=R。這證得引理 L_converse_twice。 ## 逐步反向審查 - S16 · sufficient_goal_reduction · S01, S06, S07, S09, S10, S11, S13, S14, and_intro_elim — 目標 G：題目要求的各項計算與判定。足夠條件 H：所列各步的結論；H⇒G 只是合取。H 的每一部分都由 G1 到 G3 正向證成，沒有把 G 當作前提。 - S15.1 · inverse_equivalence · L_converse_member, logic_chain — 兩次等價串接仍是等價。 - S15 · premise_audit · L_converse_twice — 這是關係層次的事實；不宣稱 R 或 R⁻¹ 有反函數。 - S14 · premise_audit · S13, function_graph — 一個失敗點就足以否定；不宣稱任何關係的逆關係都不是函數。 - S13.1 · inverse_equivalence · mko_relation_def, L_converse_member, logic_chain — 鏈中每一環都是等價，所以整條鏈雙向成立。 - S13 · premise_audit · L_dom_converse, S11 — 引理在 S13.1 證明；R[A] 的計算方法與 S08、S09 相同。 - S12 · premise_audit · S01, S11, set_extensionality, cartesian_product_def — 一個屬於一邊而不屬於另一邊的元素就足以說明兩集合不等。 - S11.1 · inverse_equivalence · mko_relation_def, cartesian_product_def, eq_replace — 兩個方向分別由逆關係的定義與有序對相等條件給出。 - S11 · premise_audit · mko_relation_def, L_converse_member, cartesian_product_def — 需要 R 的列舉完整；(3,3) 交換後不變，但仍是 R⁻¹ 的元素。 - S10 · premise_audit · mko_relation_def, empty_set_def, quantifier_negation — 這對任何關係都成立，不依賴 R 的具體資料。 - S09 · premise_audit · S08, set_extensionality, roster_membership — ⊆ 方向需要排除 B 的每個其餘元素；兩個方向合起來才得集合相等。 - S08 · premise_audit · mko_relation_def, exists_intro — 每個輸出需要一個在 C 中的見證；此步只證 ⊇ 方向。 - S07 · premise_audit · S05, function_graph — 只需一個失敗點（N6 核對 2≠3）；不宣稱 R 經修補後會成為函數。 - S06 · premise_audit · S03, S05, set_extensionality — 需要兩個方向的包含；A 的四個元素都已處理（N3：3+1=4）。 - S05 · premise_audit · S02, S04, quantifier_negation — 需要 S04 對 B 的每個 y 都成立；只檢查幾個 y 不夠。 - S04 · premise_audit · roster_membership, cartesian_product_def, forall_intro — 需要 R 的列舉是完整的（G2）；若 R 還有沒列出的對，此步就不成立。 - S03 · premise_audit · S02, exists_intro — 每個 x 需要一個在 B 中的見證；不宣稱見證唯一。 - S02 · inverse_equivalence · mko_relation_def, set_builder — 展開定義與集合建構式都是雙向的。 - S01 · premise_audit · subset_def, cartesian_product_def, roster_membership — 需要逐對檢查，且分量順序不能交換：(4,6) 的 4 要在 A、6 要在 B；(6,4) 就不在 A×B 中，因為 6∉A。不宣稱 R 等於 A×B（A×B 有 20 個元素，N1）。 ## 錯誤控制與反例 宣告來源不是定義域MKO 指出的誤解之一是把宣告來源集合當成實際關係定義域。R 宣告為從 A={1,2,3,4} 出發，但 2 沒有任何對（S04、S05），所以 Dom(R)={1,3,4}。若直接把 A 叫作定義域，就漏掉了 2 這個差異。 逆關係不是反函數MKO 指出的另一個誤解是把逆關係當成已存在的反函數。R⁻¹ 對任何關係都存在，但在本例中 4∈B 沒有輸出、3 有兩個輸出（S14），所以 R⁻¹ 不是函數 B→A，更不是 R 的反函數；R 本身也不是函數（S07）。 有序對保留方向，像只列一次(1,2)∈R 不推出 (2,1)∈R：R⊆A×B 而 1∉B（S12）。A、B 共用標籤不使順序變得無關。計算 R[C] 時，輸出 3 來自兩個對，但在集合中只列一次，所以 R[C] 有 2 個元素而不是 3 個（S09）。 - R 宣告為從 A 到 B 的關係，所以 Dom(R)=A → reject — 2∈A 沒有任何 (2,y)∈R；Dom(R)={1,3,4}。 - R⁻¹ 是 R 的反函數 → reject — R⁻¹ 不是函數 B→A：4 沒有輸出，3 有 1 與 3 兩個輸出；R 本身也不是函數。 - R[C]={2,3,3}，有三個元素 → reject — 集合中重複值只算一次；R[C]={2,3} 有兩個元素。 - (1,2)∈R，所以 (2,1)∈R → reject — R⊆A×B 而 1∉B，所以 (2,1)∉R；有序對保留方向。 ## 結論與限制 因 R⊆A×B，R 是從 A 到 B 的關係。Dom(R)={1,3,4}，與宣告來源 A 不同（2 沒有出邊）；R[C]={2,3}，R[∅]=∅；R⁻¹={(2,1),(3,1),(3,3),(6,4)}⊆B×A，Dom(R⁻¹)=R[A]={2,3,6}，且 (R⁻¹)⁻¹=R。R 不是函數 A→B（2 無輸出、1 有兩個輸出），R⁻¹ 也不是函數 B→A（4 無輸出、3 有兩個輸出），所以逆關係並不給出反函數。 - N2、N4、N5 以「差的乘積非零」表示某數不等於每一個列出的值（零乘積性質），只是對這些具體數字的重算；論證本身在對應步驟中逐項說明。 - 本稿不處理關係合成、等價關係、序關係或無限關係。 ## 驗證及來源綁定 6 個本稿宣告算術檢查；只支持所列算式。 - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: 43c26b506fc0b915b03ad39f9c5dcf722f8dfaf1e7be2295ec1d0d519436062d - original source SHA-256: 43c26b506fc0b915b03ad39f9c5dcf722f8dfaf1e7be2295ec1d0d519436062d - Lean: NOT_RUN · independent AI: NOT_MEASURED [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-relation-01.json)