# 數學表徵：判定文字、符號、表格與序對是否表示同一個函數

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

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

derivation-mko-mathematical-representation-01 · production-20261019-adopted-96



## 目標與範圍

固定對象 f:D→ℤ，D={0,1,2,3}，f(x)=2x−1。判定：文字「輸入加倍後減 1」對應 2x−1；表格 T1={(0,−1),(1,1),(2,3),(3,5)} 表示 f；序對集合是 f 的圖形；由兩列 (1,1)、(3,5) 唯一恢復仿射規則；表格 T2 把 (3,5) 換成 (3,6) 後不表示 f，也不表示任何仿射規則；含重複輸入的 T3 不是函數表；定義在 ℤ 上的 g(x)=2x−1 與 f 不是同一個函數；以及表格不提供未列點的值。

具體練習使用整係數仿射規則與完整明示的有限表格／序對（MKO 假設 a1）；輔助的兩點仿射引理則在實數係數與實數座標下敘述；所有核對只在列出的定義域上進行，未列點與圖形外觀不提供數值（假設 a2）。不處理一般圖形的語義或更完整的 typed semantic bridge；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- function_def
- cartesian_product_def
- set_extensionality
- mul_inverse_nonzero
- quantifier_negation


- G1 — 對象：f:D→ℤ，D={0,1,2,3}，f(x)=2x−1。
- G2 — 解讀規則：表格的一列 (x,y) 表示「輸入 x 的輸出是 y」。一個表格表示 f，當且僅當它的輸入恰為 D 的元素、每個各出現一次，且每一列都滿足 y=f(x)。
- G3 — 文字表徵 W：「把輸入加倍，然後減 1」。
- G4 — T1={(0,−1),(1,1),(2,3),(3,5)}；T2={(0,−1),(1,1),(2,3),(3,6)}；T3=(0,−1),(1,1),(1,2),(2,3),(3,5)（輸入 1 出現兩次）。
- G5 — g:ℤ→ℤ，g(x)=2x−1。


- D=\{0,1,2,3\} — f 的定義域
- f(x)=2x-1 — 符號表徵
- T_1,\ T_2,\ T_3 — 三個待檢查的表格／序對列表
- \Gamma_f — f 的圖形 {(x,f(x)) ∣ x∈D}
- g — 定義在 ℤ 上的同一公式





## 規則與來源


- function_def · prerequisite — 函數：f:A→B 對每個 a∈A 指定恰好一個 f(a)∈B。兩函數相等 ⇔ 定義域、對應域相同且對每個 a 都有相同值。
- 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，即兩者有相同元素。
- mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- finite_counting_basics · prerequisite — 有限計數：互斥有限集合 A、B 有 |A∪B|=|A|+|B|；|A×B|=|A|·|B|；有限集之間存在雙射 ⇔ 元素個數相同。
- set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
- eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_repr · cited — 同一數學對象可以用文字、符號、表格、序對或圖形表示。兩個表示是否對應，必須先固定對象、定義域、標度與解讀規則；不能只依外觀宣稱等價。 · mko-mathematical-representation
- mko_repr_notes · cited — 表格列出指定輸入與輸出，符號式則給計算規則；二者只有在共同域及每列數值相符時形成明示語義橋。兩點可決定非垂直仿射規則，但必須先確認橫坐標不同；重複輸入若對應不同輸出，就不是函數表。圖像可以支援理解，但像素位置、視覺直線感或未標示刻度不能替代明示資料。 · mko-mathematical-representation
- L_two_point · lemma — 對實數座標，若 x₁≠x₂，則恰有一個實係數仿射規則 y=ax+b 通過 (x₁,y₁) 與 (x₂,y₂)，即 a=(y₂−y₁)/(x₂−x₁)，b=y₁−a·x₁。





## 逐步主鏈

S01 · definition操作前

\text{several representations}

操作後

\text{object }f:D\to\mathbb{Z},\ D=\{0,1,2,3\},\ \text{row }(x,y)\ \text{means}\ f(x)=y

條件：無

規則：mko_repr · 依賴：G1, G2, mko_repr

葉節點依據：mko_repr + def_intro

依 MKO，判定對應之前要先固定對象、定義域與解讀規則。對象是 G1 的 f，定義域是四個整數，表格的解讀規則由 G2 給出。之後每個判定都是對照這些固定的設定，而不是比較外觀。



S02 · equivalent操作前

W:\ \text{double the input, then subtract 1}

操作後

x\mapsto 2x-1

條件：無

規則：def_unfold · 依賴：G3, G1

葉節點依據：def_unfold

依文字的運算次序：先加倍得 2x，再減 1 得 2x−1。次序很重要：「先減 1 再加倍」是 2(x−1)=2x−2，在 x=0 給出 −2 而不是 −1。



S03 · equivalent操作前

f(0),f(1),f(2),f(3)

操作後

-1,\ 1,\ 3,\ 5

條件：無

規則：numeric_evaluation · 依賴：G1

葉節點依據：numeric_evaluation

在定義域的四點逐一計算：2·0−1=−1，2·1−1=1，2·2−1=3，2·3−1=5。



S04 · implies操作前

\text{inputs of }T_1:\ 0,1,2,3

操作後

\text{each }x\in D\ \text{appears exactly once in }T_1

條件：無

規則：function_def · 依賴：G4, G1, function_def

葉節點依據：function_def + finite_counting_basics

T1 的輸入是 0、1、2、3，恰為 D 的四個元素，各出現一次。所以 T1 給每個 x∈D 恰好一個輸出，定義了一個 D 上的函數（記為 h₁）。



S05 · implies操作前

h_1(x)\ \text{vs}\ f(x)\ \text{for }x\in D

操作後

h_1=f\ \text{(}T_1\ \text{represents }f\text{)}

條件：\text{same domain }D

規則：function_def · 依賴：S03, S04, G2, mko_repr_notes

葉節點依據：function_def + numeric_evaluation

逐列比對：(0,−1) 對 f(0)=−1，(1,1) 對 f(1)=1，(2,3) 對 f(2)=3，(3,5) 對 f(3)=5，四列全部相符。h₁ 與 f 有相同定義域 D 且每點值相同，依函數相等的定義 h₁=f。這就是 MKO 說的「共同域且每列數值相符」的明示語義橋。



S06 · equivalent操作前

\Gamma_f=\{(x,f(x))\mid x\in D\}

操作後

\Gamma_f=\{(0,-1),(1,1),(2,3),(3,5)\}=T_1

條件：無

規則：set_builder · 依賴：S03, G1, G4

葉節點依據：set_builder + set_extensionality

序對表徵：f 的圖形是所有 (x,f(x)) 的集合；依 S03 列出四個序對，與 T1 的列完全相同，所以作為集合 Γ_f=T1。



S07 · implies操作前

(x_1,y_1),(x_2,y_2),\ x_1\neq x_2

操作後

a=\frac{y_2-y_1}{x_2-x_1},\ b=y_1-a\,x_1\ \text{(unique)}

條件：x_1\neq x_2

規則：L_two_point · 依賴：L_two_point

葉節點依據：mul_inverse_nonzero + eq_congruence

依引理 L_two_point（在 S07.1、S07.2 證明唯一性與存在性）：橫坐標不同的兩點恰好決定一個仿射規則。



S08 · implies操作前

(1,1),(3,5)\in T_1,\ 1\neq 3

操作後

a=\tfrac{5-1}{3-1}=2,\ b=1-2=-1;\ \text{rows }(0,-1),(2,3)\ \text{also satisfy }y=2x-1

條件：1\neq 3

規則：L_two_point · 依賴：S07, G4, S03

葉節點依據：L_two_point + numeric_evaluation

先確認兩列的橫坐標 1≠3，再依引理得 a=4/2=2、b=1−2·1=−1，恢復規則 y=2x−1。兩點只決定候選規則；其餘兩列 (0,−1)、(2,3) 仍要另外核對：2·0−1=−1、2·2−1=3，都相符。



S09 · implies操作前

T_2\ \text{row }(3,6),\ f(3)=5

操作後

T_2\ \text{does not represent }f\ \text{nor any affine rule}

條件：無

規則：quantifier_negation · 依賴：G4, S03, S07

葉節點依據：quantifier_negation + L_two_point + numeric_evaluation

T2 在 x=3 的列是 6，但 f(3)=5，一列不符就否定「每一列都相符」，所以 T2 不表示 f。更進一步，若某個仿射規則表示 T2，它必通過 (0,−1) 與 (1,1)（0≠1），依 L_two_point 只能是 y=2x−1，而它在 x=3 給 5≠6，所以沒有任何仿射規則表示 T2。前三列都相符並不足夠。



S10 · implies操作前

T_3\ni(1,1),(1,2)

操作後

T_3\ \text{is not a function table}

條件：1\neq 2

規則：function_def · 依賴：G4, function_def, mko_repr_notes

葉節點依據：function_def

函數對每個輸入指定恰好一個輸出。T3 中輸入 1 同時對應 1 與 2，而 1≠2，所以 T3 不是函數表，也就不能表示 f 或任何函數。這也是兩點橫坐標相同（垂直排列）時 L_two_point 不適用的情形：(1,1) 與 (1,2) 的斜率需要除以 0。



S11 · implies操作前

g:\mathbb{Z}\to\mathbb{Z},\ f:D\to\mathbb{Z}

操作後

g\neq f,\ \ g|_D=f

條件：D\neq\mathbb{Z}

規則：function_def · 依賴：G1, G5, function_def

葉節點依據：function_def + set_extensionality

g 與 f 用同一個公式，但定義域不同（ℤ 與 D），依函數相等的定義它們不是同一個函數；例如 g(4)=7 有定義，而 4∉D。把 g 限制在 D 上，每點值都與 f 相同，所以 g|_D=f。MKO 要求先固定定義域，原因就在此。



S12 · implies操作前

x=4,\ x=\tfrac{1}{2}

操作後

\text{no value supplied: }4,\tfrac{1}{2}\notin D

條件：無

規則：mko_repr_notes · 依賴：G1, G4, mko_repr_notes

葉節點依據：mko_repr_notes + function_def

T1 只列出 D 的四點。f(4) 沒有定義，因為 4∉D；1/2 也不在 D 中。若把四個點畫出來，它們看起來在一條直線上，直線經過 (1/2,0)，但依 MKO 假設 a2，圖形外觀與未列點不提供數值，所以不能宣稱 f(1/2)=0。



S13 · implies操作前

\text{decisions}

操作後

W,\ 2x-1,\ T_1,\ \Gamma_f\ \text{represent }f;\ T_2,\ T_3,\ g\ \text{do not}

條件：無

規則：and_intro_elim · 依賴：S02, S05, S06, S08, S09, S10, S11, S12

葉節點依據：and_intro_elim

合併判定：在固定的對象、定義域與解讀規則下，文字 W、公式 2x−1、表格 T1 與序對集合 Γ_f 都表示 f；兩列 (1,1)、(3,5) 唯一恢復規則；T2 不表示 f 也不表示任何仿射規則；T3 不是函數表；g 定義域不同而與 f 不等；未列點沒有值。







## 局部子步與引理

S07.1 · implies操作前

a x_1+b=y_1,\ a x_2+b=y_2

操作後

a(x_2-x_1)=y_2-y_1\ \Rightarrow\ a=\frac{y_2-y_1}{x_2-x_1},\ b=y_1-a\,x_1

條件：x_2-x_1\neq 0

規則：mul_inverse_nonzero · 依賴：mul_inverse_nonzero, eq_congruence

葉節點依據：mul_inverse_nonzero + eq_congruence + distributive

唯一性：若 y=ax+b 通過兩點，兩式相減消去 b 得 a(x₂−x₁)=y₂−y₁。因 x₂−x₁≠0，兩邊乘以 1/(x₂−x₁) 得 a 的唯一值；再由第一式 b=y₁−a·x₁。若 x₁=x₂，這裡就要除以 0，論證失效。



S07.2 · implies操作前

a=\frac{y_2-y_1}{x_2-x_1},\ b=y_1-a\,x_1

操作後

a x_1+b=y_1,\ a x_2+b=y_2

條件：x_2-x_1\neq 0

規則：eq_replace · 依賴：S07.1

葉節點依據：eq_replace + distributive + mul_inverse_nonzero

存在性：代回 a x₁+b=a x₁+y₁−a x₁=y₁；a x₂+b=y₁+a(x₂−x₁)=y₁+(y₂−y₁)=y₂（乘以 x₂−x₁ 後的恆等式見 N9）。所以這個規則確實通過兩點。S07.1 與 S07.2 合起來證得引理 L_two_point。







## 逐步反向審查


- S13 · sufficient_goal_reduction · S02, S05, S06, S08, S09, S10, S11, S12, and_intro_elim — 目標 G：本稿目標的各項判定。足夠條件 H：所列各步已證（H⇒G 由合取引入）。H 由給定條件正向推出，沒有把 G 當作前提。
- S12 · premise_audit · mko_repr_notes, function_def — 只需要這些點不在定義域中；結論是「沒有資料」，不是「值為某數」。
- S11 · premise_audit · function_def, set_extensionality — 定義域不同就足以使函數不等；公式相同不能補救。
- S10 · premise_audit · function_def, mko_repr_notes — 只需要一個輸入對應兩個不同輸出；若重複的列輸出相同，那只是重複列，另行處理。
- S09 · premise_audit · S03, L_two_point, quantifier_negation — 否定全稱只需一個反例；「沒有仿射規則」用到引理的唯一性。
- S08 · premise_audit · L_two_point, numeric_evaluation — 需要 x₁≠x₂；核對其餘各列是必要的，因為仿射規則只由兩點決定，其他列可能不在其上（S09）。
- S07.2 · premise_audit · eq_replace, distributive, mul_inverse_nonzero — 需要 a(x₂−x₁)=y₂−y₁，這由 a 的定義與 x₂−x₁≠0 得到。
- S07.1 · premise_audit · mul_inverse_nonzero, eq_congruence, distributive — 這一步只證明「若存在則唯一」；存在性在 S07.2 另外核對。
- S07 · premise_audit · L_two_point — 依賴該引理，前提 x₁≠x₂ 不可省略。
- S06 · inverse_equivalence · set_builder, set_extensionality, cartesian_product_def — 兩邊有相同的元素，集合相等雙向成立。
- S05 · premise_audit · S03, S04, function_def, mko_repr_notes — 需要四列全部相符；只檢查部分列不足以推出函數相等（見 S09 的 T2）。
- S04 · premise_audit · function_def, G4 — 需要「涵蓋 D」與「不重複」兩件事；只檢查其一不足以得到函數。
- S03 · inverse_equivalence · numeric_evaluation — 精確整數計算，雙向相同。
- S02 · inverse_equivalence · def_unfold — 把 2x−1 讀回文字：先乘 2，再減 1，正是 W；兩個方向描述同一個計算程序。
- S01 · premise_audit · G1, G2, mko_repr — 此步只固定設定，不推出新事實。





## 錯誤控制與反例

看起來相同不等於等價MKO 指出的誤解之一：把 T2 畫出來，(3,6) 只比直線高一格，四點看起來近乎在一條線上。但對應由逐列數值決定：f(3)=5≠6（S09）。像素位置與視覺直線感不能代替明示資料。

定義域與重複輸入不可忽略MKO 指出的另一個誤解：g(x)=2x−1 在 ℤ 上與 f 公式相同，但定義域不同，所以不是同一個函數（S11）；T3 的輸入 1 對應兩個輸出，不是函數表（S10）。判定前必須先核對定義域與每個輸入只出現一次。

兩點決定候選，其餘各列仍要核對由兩列恢復仿射規則需要橫坐標不同（S07.1 要除以 x₂−x₁）。恢復出的規則只是候選：T1 的其他列核對後相符（S08），T2 的第四列則不符（S09）。


- T2 表示 f，因為四列中有三列相符，而且畫出來幾乎是一條直線 → reject — 表示要求每一列都相符；f(3)=5≠6（S09）。
- g:ℤ→ℤ，g(x)=2x−1 與 f 是同一個函數 → reject — 定義域不同；例如 g(4)=7 有定義，4∉D（S11）。
- T3 的每一列都是序對，所以 T3 是一個函數表 → reject — 輸入 1 對應 1 與 2 兩個輸出（S10）。
- 由 T1 可知 f(1/2)=0，因為這些點在一條直線上 → reject — 1/2∉D，未列點與圖形外觀不提供數值（S12）。
- 文字「把輸入加倍，然後減 1」描述的是 2(x−1) → reject — 2(x−1) 是先減後乘；在 x=0 得 −2，而 W 給 −1（S02）。





## 結論與限制

固定 f:D→ℤ（D={0,1,2,3}，f(x)=2x−1）與「列 (x,y) 表示 f(x)=y」的解讀規則後：文字「輸入加倍後減 1」、公式 2x−1、表格 T1 與序對集合 {(0,−1),(1,1),(2,3),(3,5)} 都表示 f；由 (1,1)、(3,5)（1≠3）唯一恢復 y=2x−1，其餘列另外核對相符。T2 在 x=3 的值 6≠5，不表示 f，且依兩點唯一性不表示任何仿射規則；T3 中輸入 1 對應兩個輸出，不是函數表；g:ℤ→ℤ 與 f 定義域不同而不相等；表格不提供 x=4 或 x=1/2 的值。


- 圖形表徵只在錯誤控制與 S12 中討論，沒有建立座標刻度與像素的正式對應；更完整的 typed semantic bridge 屬於 MKO 的 formal next。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: c57160d6a5d2e6e5cf54e5bc2ba0141c674852fb5e67bc4370040368f3ac58c2
- original source SHA-256: 9a638a2170e8b0d8bd35dbc76a4458dca4722cbd6f58352d5b1d907fd8f30ae8
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-mathematical-representation-01.json)