二元關係：定義域、關係像與逆關係的逐步計算

目標與範圍

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

逐步主鏈

R=\{(1,2),(1,3),(3,3),(4,6)\}

R\subseteq A\times B

x\in\mathrm{Dom}(R)

x\in A\ \land\ \exists y\in B:\ (x,y)\in R

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

1,3,4\in\mathrm{Dom}(R)

y\in B,\quad (2,y)\in R\ ?

\forall y\in B:\ (2,y)\notin R

\forall y\in B:\ (2,y)\notin R

2\notin\mathrm{Dom}(R)

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

2\notin\mathrm{Dom}(R),\ (1,2)\in R,\ (1,3)\in R

R\ \text{is not a function}\ A\to B

y\in R[C],\quad C=\{1,3\}

2\in R[C],\ 3\in R[C]

2,3\in R[C]

R[C]=\{2,3\}

R[\varnothing]

R[\varnothing]=\varnothing

R=\{(1,2),(1,3),(3,3),(4,6)\}

R^{-1}=\{(2,1),(3,1),(3,3),(6,4)\}\subseteq B\times A

(1,2)\in R,\ (2,1)\in R^{-1}

(2,1)\notin R,\ \text{so}\ R^{-1}\neq R

\mathrm{Dom}(R^{-1})

\mathrm{Dom}(R^{-1})=R[A]=\{2,3,6\}

R^{-1}=\{(2,1),(3,1),(3,3),(6,4)\}

R^{-1}\ \text{is not a function}\ B\to A

(R^{-1})^{-1}

(R^{-1})^{-1}=R

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

局部子步與引理

(y,x)\in S^{-1}

(x,y)\in S

y\in\mathrm{Dom}(R^{-1})

y\in R[A]

(x,y)\in(R^{-1})^{-1}

(x,y)\in R

逐步反向審查

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