# 變數與代數式：式子的值由取值、作用域與數系共同決定

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

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

derivation-mko-variable-expression-01 · production-20261019-adopted-96



## 目標與範圍

設 E=x+1、F=(x+1)÷2、H=Σ_{x=1}^{3}(x+1)。(1) 在 ℤ 中求 E 在 x=2 與 x=5 的值，並證明 E 沒有與 x 無關的固定值；(2) 求 F 在 x=4 時於 ℚ 與 ℤ 中的值；(3) 在外部指定 x=5 時求 H；(4) 判定 (x+1)+x 與 2x+1、x·x 與 2x 在 ℤ 上是否等價；(5) 區分表達式 x+1 與方程 x+1=3，並求方程在 ℤ 中的解集。

只用 ℤ、ℚ 的一般運算，除法取精確除法（G1），一個自由變數 x 與一個有界求和中的約束變數。示範 MKO：代數式的值由取值、作用域、數系與運算規則共同決定；沒有等號的代數式不是方程。不建立形式語法或求值函數，不處理多變數或函數型別；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- add_assoc
- add_comm
- distributive
- mul_inverse_nonzero
- order_basics
- numeric_evaluation


- G1 — 數系與運算：ℤ⊂ℚ，使用一般的加法與乘法；精確除法 u÷v 在數系 S 中定義為使 v·w=u 的唯一 w∈S，若沒有這樣的 w 則在 S 中沒有定義（在 ℚ 中對 v≠0 有 u÷v=u·(1/v)）。
- G2 — 式子：E=x+1，F=(x+1)÷2，H=Σ_{x=1}^{3}(x+1)；其中 Σ_{x=1}^{3} g(x) 表示 g(1)+g(2)+g(3)，H 中的 x 由求和符號約束。
- G3 — 比較的對象：(x+1)+x 與 2x+1；x·x 與 2x；以及 ℤ 上的方程 x+1=3。


- x — 變數；作用域與數系在各部分指定
- U[x:=c] — 把 U 中自由出現的 x 換成 c 後求得的值
- u\div v — 精確除法：使 v·w=u 的唯一 w
- \sum_{x=1}^{3} g(x) — g(1)+g(2)+g(3)，其中 x 是約束變數
- U\equiv_{\mathbb{Z}} V — U 與 V 在 ℤ 上等價





## 規則與來源


- add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
- add_comm · prerequisite — 加法交換律：u+v=v+u。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
- order_basics · prerequisite — 實數的序：任兩數恰有 u<v、u=v、u>v 之一；u<v 且 v<w 推出 u<w；u<v 推出 u+w<v+w；u<v 且 w>0 推出 uw<vw；u<v 且 w<0 推出 uw>vw。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
- eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。
- two_nonzero · prerequisite — 實數中 0<1，故 0<1+1=2，所以 2≠0。
- 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)。
- finite_sum_rules · prerequisite — 有限和：Σ_{i=1}^{0} a_i=0、Σ_{i=1}^{n+1} a_i=Σ_{i=1}^{n} a_i + a_{n+1}；Σ(a_i+b_i)=Σa_i+Σb_i；Σ c·a_i=c·Σa_i。
- mul_one · prerequisite — 乘法單位元：1·u=u。
- mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
- add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
- set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_var_expr · cited — 代數式的值由其中變數的取值、作用域、型別或數系以及運算規則共同決定；沒有等號的代數式本身不是方程式。 · mko-variable-expression
- mko_equation · cited — 給定兩個具有共同語境的表達式 L(x)、R(x)，方程式 L(x)=R(x) 的解集由所有使兩側皆有定義且值相等的允許 x 組成。 · mko-equation
- eval_assign · prerequisite — 求值規則：式子 U 在指派 x:=c（c∈S）下的值，是把 U 中每個自由出現的 x 換成 c，再用 S 的運算計算；若過程中某個運算在 S 中沒有定義，U 在此指派下沒有值。
- bound_var · prerequisite — 約束變數：Σ_{x=1}^{3} g(x) 中的 x 由求和符號約束，只取 1、2、3；外部對 x 的指派不替換約束出現；把約束變數一致改名（例如改成 k）不改變值。
- expr_equiv · prerequisite — 式子等價：U 與 V 在 S 上等價，表示對每個 c∈S，U[x:=c] 與 V[x:=c] 都有值且相等。
- int_no_gap · prerequisite — 整數沒有空隙：對整數 k 與 m，必有 k≤m 或 k≥m+1。
- L_double · lemma — 對每個 x∈ℤ：(x+1)+x=2x+1。





## 逐步主鏈

S01 · definition操作前

x+1,\ (x+1)\div 2,\ \sum_{x=1}^{3}(x+1)

操作後

\text{value}=U[x:=c]\ \text{computed in a stated}\ S

條件：無

規則：mko_var_expr · 依賴：G1, G2

葉節點依據：mko_var_expr + eval_assign

MKO 說代數式的值由變數取值、作用域、數系與運算規則共同決定。所以求值前要說清四件事：x 取哪個值（指派）、哪些 x 是自由出現（作用域）、在哪個數系計算，以及用哪些運算規則（G1 的加法、乘法與精確除法）。缺任何一項，「式子的值」都沒有確定意義。



S02 · equivalent操作前

E[x:=2]\ \text{in}\ \mathbb{Z}

操作後

2+1=3

條件：無

規則：eval_assign · 依賴：S01, G2

葉節點依據：eval_assign + numeric_evaluation

E=x+1 中 x 自由出現一次；依 eval_assign 把它換成 2 得 2+1，在 ℤ 中計算得 3。



S03 · equivalent操作前

E[x:=5]\ \text{in}\ \mathbb{Z}

操作後

5+1=6

條件：無

規則：eval_assign · 依賴：S01, G2

葉節點依據：eval_assign + numeric_evaluation

同一個式子，換一個指派：把 x 換成 5 得 5+1，在 ℤ 中等於 6。



S04 · implies操作前

E[x:=2]=3,\ E[x:=5]=6

操作後

\neg\exists v\in\mathbb{Z}\ \forall c\in\mathbb{Z}:\ E[x:=c]=v

條件：無

規則：contradiction · 依賴：S02, S03

葉節點依據：contradiction + eq_refl_symm_trans + numeric_evaluation

假設有一個固定的整數 v，使每個指派都有 E[x:=c]=v。取 c=2 得 v=3，取 c=5 得 v=6，依等號的對稱與傳遞得 3=6，與 3≠6 矛盾。所以 E 沒有與 x 無關的固定值；說「x+1 的值」時必須先指定 x。



S05 · equivalent操作前

F[x:=4]\ \text{in}\ \mathbb{Q}

操作後

(4+1)\div 2=5\cdot\tfrac{1}{2}=\tfrac{5}{2}

條件：2\neq 0

規則：eval_assign · 依賴：S01, G1, G2

葉節點依據：eval_assign + mul_inverse_nonzero + two_nonzero + numeric_evaluation

把 x 換成 4 得 (4+1)÷2=5÷2。在 ℚ 中 2≠0，所以依 G1，5÷2=5·(1/2)=5/2；它是 2w=5 在 ℚ 中唯一的解（代回 2·(5/2)=5）。



S06 · case_split操作前

F[x:=4]\ \text{in}\ \mathbb{Z}:\ w\in\mathbb{Z}\ \text{with}\ 2w=5\ ?

操作後

w\le 2\ \lor\ w\ge 3

條件：w\in\mathbb{Z}

規則：int_no_gap · 依賴：G1, G2

葉節點依據：int_no_gap + case_analysis

在 ℤ 中，(4+1)÷2=5÷2 需要一個整數 w 使 2w=5。依 int_no_gap（m=2），每個整數 w 滿足 w≤2 或 w≥3，兩支涵蓋全部整數，在 S06.1、S06.2 處理。



S07 · implies操作前

\forall w\in\mathbb{Z}:\ 2w\neq 5

操作後

F[x:=4]\ \text{has no value in}\ \mathbb{Z},\ \text{while}\ F[x:=4]=\tfrac{5}{2}\ \text{in}\ \mathbb{Q}

條件：無

規則：case_analysis · 依賴：S06, S06.1, S06.2, S05, G1

葉節點依據：case_analysis + eval_assign + quantifier_negation

兩支都得 2w≠5，所以 ℤ 中沒有 w 使 2w=5；依 G1，5÷2 在 ℤ 中沒有定義，再依 eval_assign，F 在 x=4 時於 ℤ 中沒有值。對照 S05：同一個式子、同一個指派，換了數系，從「值為 5/2」變成「沒有值」。數系是求值資料的一部分。



S08 · equivalent操作前

H=\sum_{x=1}^{3}(x+1)

操作後

H=(1+1)+(2+1)+(3+1)

條件：無

規則：finite_sum_rules · 依賴：G2, bound_var

葉節點依據：finite_sum_rules + bound_var

依求和記號的意義（G2，亦即 finite_sum_rules 的遞迴定義展開三次），H 是把約束變數 x 依序換成 1、2、3 後相加。這裡的 x 只取 1、2、3，與外部是否指定 x 無關。



S09 · equivalent操作前

(1+1)+(2+1)+(3+1)

操作後

2+3+4=9

條件：無

規則：numeric_evaluation · 依賴：S08

葉節點依據：numeric_evaluation

逐項計算 1+1=2、2+1=3、3+1=4，再相加得 9。



S10 · implies操作前

H[x:=5]

操作後

H[x:=5]=H=9\neq 18=(5+1)+(5+1)+(5+1)

條件：無

規則：bound_var · 依賴：S09, bound_var, eval_assign

葉節點依據：bound_var + eval_assign + numeric_evaluation

依 eval_assign，指派 x:=5 只替換自由出現的 x；H 中的 x 全是約束出現（bound_var），沒有自由出現，所以 H[x:=5] 就是 H 本身，值仍為 9。若錯把約束的 x 也換成 5，會得到 (5+1)+(5+1)+(5+1)=18，與 9 不同；這正是忽略作用域的錯誤。



S11 · equivalent操作前

(x+1)+x

操作後

2x+1

條件：x\in\mathbb{Z}

規則：L_double · 依賴：G3

葉節點依據：add_assoc + add_comm + distributive + mul_one + numeric_evaluation

任取 x∈ℤ，不加任何額外假設。依引理 L_double，(x+1)+x=2x+1。引理在 S11.1、S11.2 中只用 ℤ 的運算規則證明，而不是看兩式外觀相似。



S12 · implies操作前

\text{for arbitrary}\ x\in\mathbb{Z}:\ (x+1)+x=2x+1

操作後

(x+1)+x\equiv_{\mathbb{Z}}2x+1

條件：無

規則：forall_intro · 依賴：S11, expr_equiv

葉節點依據：forall_intro + expr_equiv

S11 對任意 x∈ℤ 成立，沒有對 x 加任何條件；依全稱推廣，對所有 x∈ℤ 兩式的值相等，而且兩式在 ℤ 中總有值（只用加法與乘法），依 expr_equiv 兩式在 ℤ 上等價。語法不同的式子可以等價，但理由是運算規則。



S13 · implies操作前

x\cdot x\ \text{vs}\ 2x

操作後

1\cdot 1=1\neq 2=2\cdot 1,\ \text{so}\ x\cdot x\not\equiv_{\mathbb{Z}}2x

條件：無

規則：quantifier_negation · 依賴：G3, expr_equiv

葉節點依據：quantifier_negation + expr_equiv + numeric_evaluation

等價要求每個 x 都相等。取 x=1：x·x=1，2x=2，1≠2，所以存在使兩式不等的 x，依量詞否定兩式在 ℤ 上不等價。注意兩式在 x=0（都為 0）與 x=2（都為 4）相等：在部分取值上相等不足以推出等價。



S14 · implies操作前

x+1\quad\text{vs}\quad x+1=3

操作後

\{x\in\mathbb{Z}\mid x+1=3\}=\{2\}

條件：無

規則：mko_equation · 依賴：G3, S02, mko_equation

葉節點依據：mko_equation + eq_congruence + add_inverse + set_extensionality

x+1 沒有等號，是表達式：它在每個指派下有一個值（S02、S03），但本身沒有真假，也沒有解集。x+1=3 有等號，是方程：依 mko_equation，它的解集是使兩側都有定義且相等的 x∈ℤ。兩側在 ℤ 中總有定義；兩邊同加 −1 得 x+1=3 ⇔ x=2（反向是同加 1），所以解集是 {2}。S02 的 E[x:=2]=3 正是這個解的代回核對。



S15 · implies操作前

\text{conclusions of S04, S07, S10, S12, S13, S14}

操作後

\text{value of }U=\text{function of assignment, scope, system and rules}

條件：無

規則：and_intro_elim · 依賴：S04, S07, S10, S12, S13, S14

葉節點依據：and_intro_elim

把結論合在一起：取值改變值（S04）；數系改變有無值（S07）；作用域決定哪些 x 被指派取代（S10）；等價由運算規則對所有取值證明（S12），部分取值相等不夠（S13）；表達式與方程角色不同（S14）。







## 局部子步與引理

S06.1 · implies操作前

w\le 2

操作後

2w\le 4<5,\ \text{so}\ 2w\neq 5

條件：2>0

規則：order_basics · 依賴：S06

葉節點依據：order_basics + numeric_evaluation

若 w<2，乘以正數 2 保持順序，得 2w<4；若 w=2，則 2w=4。所以 2w≤4<5，於是 2w≠5。



S06.2 · implies操作前

w\ge 3

操作後

2w\ge 6>5,\ \text{so}\ 2w\neq 5

條件：2>0

規則：order_basics · 依賴：S06

葉節點依據：order_basics + numeric_evaluation

若 w>3，乘以 2>0 得 2w>6；若 w=3，則 2w=6。所以 2w≥6>5，於是 2w≠5。



S11.1 · equivalent操作前

(x+1)+x

操作後

(x+x)+1

條件：無

規則：add_assoc · 依賴：add_assoc, add_comm

葉節點依據：add_assoc + add_comm

(x+1)+x=x+(1+x)（結合律）=x+(x+1)（交換律）=(x+x)+1（結合律）。



S11.2 · equivalent操作前

(x+x)+1

操作後

2x+1

條件：無

規則：distributive · 依賴：S11.1

葉節點依據：distributive + mul_one + mul_comm + numeric_evaluation

x+x=1·x+1·x（乘法單位元）=(1+1)x（分配律與交換律）=2x，所以 (x+x)+1=2x+1。S11.1 與 S11.2 合起來證得引理 L_double。







## 逐步反向審查


- S15 · sufficient_goal_reduction · S04, S07, S10, S12, S13, S14, and_intro_elim — 目標 G：回答題目的五個部分。足夠條件 H：S04、S07、S10、S12、S13、S14 的結論；H⇒G 只是並列。H 由 G1 到 G3 正向證成，沒有把 G 當作前提。
- S14 · premise_audit · mko_equation, eq_congruence, S02, set_extensionality — 解集的計算用了等價變形（同加 −1 與同加 1 互逆），而且兩側在 ℤ 中都有定義；這一步沒有把表達式 x+1 本身當作方程。
- S13 · premise_audit · expr_equiv, quantifier_negation, numeric_evaluation — 一個反例足以否定「對所有 x 相等」；不宣稱兩式只在 x=1 不等。
- S12 · premise_audit · S11, forall_intro, expr_equiv — 需要 S11 中的 x 是任意的；N11 只是在少數格點上的獨立交叉核對，一般性來自 S11 的規則推導。
- S11.2 · inverse_equivalence · distributive, mul_one, numeric_evaluation — 所用的都是恆等式，等值代換雙向成立。
- S11.1 · inverse_equivalence · add_assoc, add_comm — 結合律與交換律都是對所有整數成立的等式，倒著讀同樣成立。
- S11 · inverse_equivalence · L_double — 兩式是同一個整數的兩種寫法；引理的每一步都是等值代換，可逆。
- S10 · premise_audit · S09, bound_var, eval_assign — 需要辨認 H 中每個 x 都被 Σ 約束；結論只關於 H，不宣稱外部的 x 在其他式子中沒有作用。
- S09 · inverse_equivalence · numeric_evaluation — 兩邊是同一個整數，可重算（N8）。
- S08 · inverse_equivalence · finite_sum_rules, bound_var — 展開與收回求和記號是同一定義的兩個方向。
- S07 · premise_audit · S06, S06.1, S06.2, case_analysis, eval_assign — 需要兩支涵蓋所有整數；結論只關於 x=4，不宣稱 F 在 ℤ 中對任何 x 都沒有值（例如 x=3 時 (3+1)÷2=2）。
- S06.2 · premise_audit · order_basics — 同 S06.1；不宣稱反向。
- S06.1 · premise_audit · order_basics, two_nonzero — 用到 2>0 保持不等號方向；只推出 2w≠5，不宣稱反向。
- S06 · premise_audit · G1, int_no_gap — 分情況依賴 w 是整數；在 ℚ 中 w=5/2 就落在兩支之間，這正是 S05 與 S07 結論不同的原因。
- S05 · inverse_equivalence · eval_assign, mul_inverse_nonzero, numeric_evaluation — 兩邊是同一個有理數；條件 2≠0 使 1/2 存在，唯一性來自兩邊同乘 1/2 與同乘 2 互為反運算。
- S04 · premise_audit · S02, S03, contradiction, eq_refl_symm_trans — 兩個不同的值就足以推翻「有固定值」；這一步不需要也不宣稱 E 的值域是什麼。
- S03 · inverse_equivalence · eval_assign, numeric_evaluation — 兩邊是同一個整數，可重算（N2）。
- S02 · inverse_equivalence · eval_assign, numeric_evaluation — E[x:=2]、2+1 與 3 是同一個整數的不同寫法，可獨立重算（N1）；這只是 x=2 時的值。
- S01 · premise_audit · G1, G2, mko_var_expr, eval_assign — 此步只列出求值所需的資料，不推出新事實。





## 錯誤控制與反例

本例 E=x+1 的值依賴 x 的取值MKO 指出的常見誤解是把含變數的表達式當成已有固定值。x+1 在 x=2 時是 3，在 x=5 時是 6（S02、S03），S04 證明它沒有與 x 無關的值。所以「x+1=3」只能讀成對 x 的要求（方程），不能讀成「x+1 這個式子就是 3」。

沒有等號就不是方程MKO 的另一個誤解是把任何含 x 的文字都當作方程。x+1 沒有等號，不能「解」；若有人說「解 x+1 得 x=−1」，其實是自行補上了方程 x+1=0。方程需要兩個表達式與等號，解集還要求兩側在指定數系中有定義（S14）。

約束變數不接受外部指派H=Σ_{x=1}^{3}(x+1) 中的 x 被求和符號約束。外部指派 x=5 時 H 仍是 9；把約束出現也換成 5 會錯得 18（S10）。把約束變數改名為 k，寫成 Σ_{k=1}^{3}(k+1)，就看得出它與外部的 x 無關。


- x+1 的值是 3 → reject — 只在指派 x=2 時成立；x=5 時值為 6（S03、S04）。
- x+1 是方程，它的解是 x=−1 → reject — x+1 沒有等號；x=−1 是另一個方程 x+1=0 的解，而那個方程不是題目給的。
- x·x 與 2x 在 x=0 與 x=2 時相等，所以它們在 ℤ 上等價 → reject — x=1 時 1≠2（S13）；部分取值相等不足以推出等價。
- (x+1)÷2 在 x=4 時的值是 5/2，在任何數系都一樣 → reject — 在 ℤ 中沒有整數 w 使 2w=5，所以沒有值（S07）。
- 外部指定 x=5 時，Σ_{x=1}^{3}(x+1)=18 → reject — H 中的 x 是約束變數，不被外部指派取代，值仍為 9（S10）。





## 結論與限制

在 ℤ 中 E 在 x=2 時為 3、在 x=5 時為 6，因此沒有固定值。F 在 x=4 時於 ℚ 中為 5/2，於 ℤ 中沒有值。外部指定 x=5 時 H 仍為 9，因為 H 中的 x 是約束變數。(x+1)+x 與 2x+1 在 ℤ 上等價；x·x 與 2x 不等價（x=1 時 1≠2）。x+1 是表達式，沒有解集；x+1=3 是方程，在 ℤ 中的解集為 {2}。


- 本稿以 eval_assign、bound_var、expr_equiv 的文字定義作為前提，未建立形式語法、自由變數的遞迴定義或求值函數（MKO 的 formal next）。
- N11 是在格點 {0,1} 上的一次多項式恆等式核對，只作為 S11 的獨立交叉核對；本稿的一般性來自 S11 的規則推導。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 7bae56c281b5a8252bb4564f48957ca0b1b4d33f1093e8dfcaed3df6d8e85309
- original source SHA-256: 4e7848b5ae3d6ec21f3cf5b0f6297ac58148c0066c80cbcda81b003b28355a4a
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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