# 四則運算：同一組輸入在 ℕ、ℤ、ℚ 中是否有定義

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

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

derivation-mko-arithmetic-operations-01 · production-20261019-adopted-96



## 目標與範圍

取 a=3、b=5。在 ℕ（含 0）、ℤ、ℚ 三個數系中，判定 a+b、a·b、a−b、a÷b 是否有定義；有定義時求出結果，並判定結果屬於哪些數系。再判定 3÷0 與 0÷0 在這三個數系中是否有定義。

只處理三個明示數系 ℕ⊂ℤ⊂ℚ 與一組明示輸入；差與商以「方程 b+c=a、b·q=a 在該數系中恰有一解」定義（G2）。示範 MKO 的要點：運算是否有定義、結果是否留在原數系，必須連同數系與除零邊界一起指定。不建構這些數系，不處理截斷減法或帶餘除法等其他運算，不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- order_basics
- add_inverse
- mul_inverse_nonzero
- mul_zero
- numeric_evaluation


- G1 — 數系：ℕ={n∈ℤ ∣ n≥0}，且 ℕ⊂ℤ⊂ℚ；三者共用同一套加法、乘法與大小順序（ℚ 的運算與順序限制到 ℤ、ℕ 上）。
- G2 — 差與商的定義：設 S 是上述數系之一，a,b∈S。若恰有一個 c∈S 使 b+c=a，則稱 a−b 在 S 中有定義，且 a−b=c；若恰有一個 q∈S 使 b·q=a，則稱 a÷b 在 S 中有定義，且 a÷b=q。若沒有這樣的元素，或不只一個，該運算對這組輸入在 S 中沒有定義。
- G3 — 輸入：a=3、b=5；另外檢查除數為零的兩組輸入 (3,0) 與 (0,0)。


- \mathbb{N} — 非負整數 0、1、2 等組成的集合
- \mathbb{Z},\ \mathbb{Q} — 整數集與有理數集
- a-b — 在指定數系中使 b+c=a 的唯一 c
- a\div b — 在指定數系中使 b·q=a 的唯一 q
- \tfrac{1}{u} — 非零有理數 u 的倒數





## 規則與來源


- 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。
- add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
- mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
- mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
- add_zero · prerequisite — 加法單位元：u+0=u。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
- add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
- add_comm · prerequisite — 加法交換律：u+v=v+u。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- mul_one · prerequisite — 乘法單位元：1·u=u。
- mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。
- mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
- contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_arith · cited — 四則運算以兩個輸入形成結果；運算是否有定義、結果是否仍在原數系中，必須連同數系與除零等邊界一起指定。 · mko-arithmetic-operations
- nat_closed · prerequisite — ℕ 對加法與乘法封閉：若 m,n∈ℕ，則 m+n∈ℕ 且 m·n∈ℕ（非負整數的和與積仍是非負整數）。
- int_no_gap · prerequisite — 整數沒有空隙：對整數 k 與 m，必有 k≤m 或 k≥m+1；特別是沒有整數嚴格介於 m 與 m+1 之間。
- L_sub · lemma — 在 ℤ 或 ℚ 中，對該數系的 a、b、c：b+c=a ⇔ c=a+(−b)。
- L_div · lemma — 在 ℚ 中，對 a,q∈ℚ 與 b≠0：b·q=a ⇔ q=a·(1/b)。





## 逐步主鏈

S01 · definition操作前

a,b\ \text{and an operation, system not yet stated}

操作後

S\in\{\mathbb{N},\mathbb{Z},\mathbb{Q}\};\ a-b=c\iff b+c=a\ (\text{unique }c\in S);\ a\div b=q\iff bq=a\ (\text{unique }q\in S)

條件：無

規則：mko_arith · 依賴：G1, G2

葉節點依據：mko_arith + def_intro

MKO 要求運算的定義連同數系與除零邊界一起指定，所以先固定：三個數系 ℕ⊂ℤ⊂ℚ 共用同一套加法與乘法（G1）；減法與除法定義為「解方程」：a−b 是使 b+c=a 的唯一 c，a÷b 是使 b·q=a 的唯一 q，而且解必須在所討論的數系 S 之中（G2）。之後說「有定義」一律指這個意義。



S02 · implies操作前

3,5\in\mathbb{N}

操作後

3+5=8\in\mathbb{N},\quad 3\cdot 5=15\in\mathbb{N}

條件：3\ge 0; 5\ge 0

規則：nat_closed · 依賴：G1, G3, nat_closed

葉節點依據：nat_closed + numeric_evaluation

3 與 5 是非負整數，所以屬於 ℕ。依 nat_closed，它們的和與積仍在 ℕ 中；計算得 3+5=8、3·5=15，兩者都 ≥0。加法與乘法對這組輸入在 ℕ 中有定義，結果留在 ℕ。因三個數系共用同一套運算（G1），在 ℤ、ℚ 中的和與積也是 8 與 15。



S03 · implies操作前

c\in\mathbb{N}

操作後

5+c\ge 5

條件：c\ge 0

規則：order_basics · 依賴：G1

葉節點依據：order_basics + add_zero

為了判定 3−5 在 ℕ 中是否有定義，先看 5+c 在 ℕ 中能取哪些值。任取 c∈ℕ，則 c≥0。若 c>0，依 order_basics（u<v 推出 u+w<v+w，取 u=0、v=c、w=5）得 5+0<5+c；若 c=0，則 5+c=5。兩種情形都有 5+c≥5+0=5。



S04 · implies操作前

\forall c\in\mathbb{N}:\ 5+c\ge 5>3

操作後

\neg\exists c\in\mathbb{N}:\ 5+c=3

條件：無

規則：quantifier_negation · 依賴：S03

葉節點依據：quantifier_negation + order_basics

由 S03，每個 c∈ℕ 都有 5+c≥5，而 5>3，依順序的傳遞得 5+c>3；依三一律，5+c>3 排除 5+c=3。所以每個 c∈ℕ 都有 5+c≠3，依量詞否定，這等價於「不存在 c∈ℕ 使 5+c=3」。



S05 · implies操作前

\neg\exists c\in\mathbb{N}:\ 5+c=3

操作後

3-5\ \text{is undefined in}\ \mathbb{N}

條件：無

規則：def_unfold · 依賴：S04, G2

葉節點依據：def_unfold

依 G2，3−5 在 ℕ 中有定義需要恰有一個 c∈ℕ 使 5+c=3；S04 說連一個都沒有，所以 3−5 在 ℕ 中沒有定義。這表示 ℕ 對減法不封閉。



S06 · equivalent操作前

5+c=3,\ c\in\mathbb{Z}

操作後

c=3+(-5)=-2

條件：無

規則：L_sub · 依賴：G1, G3

葉節點依據：eq_congruence + add_assoc + add_comm + add_inverse + add_zero + numeric_evaluation

在 ℤ 中依引理 L_sub（a=3、b=5）：5+c=3 ⇔ c=3+(−5)，而 3+(−5)=−2。所以在 ℤ 中方程 5+c=3 恰有一個解 c=−2。同一論證在 ℚ 中也成立，ℚ 中的唯一解也是 −2。



S07 · implies操作前

c=-2\ \text{is the only solution in}\ \mathbb{Z}

操作後

3-5=-2\ \text{in}\ \mathbb{Z},\quad -2\notin\mathbb{N}

條件：-2<0

規則：def_unfold · 依賴：S06, G1, G2

葉節點依據：def_unfold + order_basics

S06 給出 ℤ 中恰有一個解，依 G2，3−5 在 ℤ（以及 ℚ）中有定義且等於 −2。又 −2<0，依 G1 的 ℕ={n∈ℤ ∣ n≥0}，−2∉ℕ。這與 S05 一致：ℤ 中唯一的解不在 ℕ 中，所以 ℕ 中沒有解。同一組輸入，換了數系，判定就不同。



S08 · case_split操作前

q\in\mathbb{Z}\ \text{with}\ 5q=3\ ?

操作後

q\le 0\ \lor\ q\ge 1

條件：q\in\mathbb{Z}

規則：int_no_gap · 依賴：G1, G2

葉節點依據：int_no_gap + case_analysis

要判定 3÷5 在 ℤ 中是否有定義，需問有沒有整數 q 使 5q=3。依 int_no_gap（m=0），每個整數 q 都滿足 q≤0 或 q≥1；兩種情形涵蓋全部整數，分別在 S08.1、S08.2 處理。



S09 · implies操作前

q\le 0\Rightarrow 5q\neq 3,\quad q\ge 1\Rightarrow 5q\neq 3

操作後

\neg\exists q\in\mathbb{Z}:\ 5q=3;\ 3\div 5\ \text{undefined in}\ \mathbb{Z}\ \text{and in}\ \mathbb{N}

條件：無

規則：case_analysis · 依賴：S08, S08.1, S08.2, G1, G2

葉節點依據：case_analysis + quantifier_negation + def_unfold

兩種情形都得 5q≠3，依分情況論證，每個整數 q 都有 5q≠3，即 ℤ 中沒有解；依 G2，3÷5 在 ℤ 中沒有定義。因 ℕ⊂ℤ 且運算相同，ℕ 中的解也會是 ℤ 中的解，所以 3÷5 在 ℕ 中也沒有定義。ℤ 對除法不封閉。



S10 · equivalent操作前

5q=3,\ q\in\mathbb{Q}

操作後

q=3\cdot\tfrac{1}{5}=\tfrac{3}{5}

條件：5\neq 0

規則：L_div · 依賴：G1, G3

葉節點依據：eq_congruence + mul_inverse_nonzero + mul_assoc + mul_comm + mul_one + numeric_evaluation

在 ℚ 中依引理 L_div（a=3、b=5，條件 5≠0）：5q=3 ⇔ q=3·(1/5)=3/5。所以在 ℚ 中方程 5q=3 恰有一個解。



S11 · implies操作前

q=\tfrac{3}{5}\ \text{is the only solution in}\ \mathbb{Q}

操作後

3\div 5=\tfrac{3}{5}\ \text{in}\ \mathbb{Q},\quad 0<\tfrac{3}{5}<1,\ \tfrac{3}{5}\notin\mathbb{Z}

條件：無

規則：def_unfold · 依賴：S10, G2, int_no_gap

葉節點依據：def_unfold + int_no_gap + order_basics + numeric_evaluation

依 G2 與 S10，3÷5 在 ℚ 中有定義且等於 3/5。又 1/5>0（因 5>0），把 0<3<5 乘以 1/5 得 0<3/5<1；依 int_no_gap 沒有整數嚴格介於 0 與 1 之間，所以 3/5∉ℤ。這與 S09 一致：ℚ 中唯一的解不是整數。



S12 · implies操作前

q\in\mathbb{Q}

操作後

0\cdot q=0

條件：無

規則：mul_zero · 依賴：G1

葉節點依據：mul_zero + mul_comm

轉向除數為零。依 mul_zero，q·0=0；再依乘法交換律 0·q=q·0=0。這對每個 q∈ℚ 成立，因而對 ℤ、ℕ 中的 q 也成立。



S13 · implies操作前

\forall q\in\mathbb{Q}:\ 0\cdot q=0\neq 3

操作後

\neg\exists q\in\mathbb{Q}:\ 0\cdot q=3;\ 3\div 0\ \text{undefined in}\ \mathbb{Q},\mathbb{Z},\mathbb{N}

條件：無

規則：contradiction · 依賴：S12, G1, G2

葉節點依據：contradiction + mul_zero + numeric_evaluation

若有 q∈ℚ 使 0·q=3，則由 S12 得 3=0·q=0，與 3≠0 矛盾。所以沒有任何 q∈ℚ 滿足 0·q=3，依 G2，3÷0 在 ℚ 中沒有定義；ℤ、ℕ 中的解也會是 ℚ 中的解，所以 3÷0 在三個數系中都沒有定義。這是「沒有候選值」型的除零。



S14 · implies操作前

\forall q:\ 0\cdot q=0

操作後

0\cdot 0=0,\ 0\cdot 1=0,\ 0\neq 1;\ 0\div 0\ \text{undefined in}\ \mathbb{N},\mathbb{Z},\mathbb{Q}

條件：無

規則：def_unfold · 依賴：S12, G2

葉節點依據：def_unfold + mul_zero

由 S12，每個 q 都滿足 0·q=0，例如 q=0 與 q=1；兩者都在 ℕ（因而也在 ℤ、ℚ）中，而且 0≠1。所以在每個數系中，方程 0·q=0 的解都不只一個；G2 要求恰有一個，因此 0÷0 在三個數系中都沒有定義。這是「候選值太多」型的除零。



S15 · implies操作前

\text{verdicts of S02, S05, S07, S09, S11, S13, S14}

操作後

3+5=8,\ 3\cdot 5=15\ (\mathbb{N});\ 3-5=-2\ (\mathbb{Z});\ 3\div 5=\tfrac{3}{5}\ (\mathbb{Q});\ 3\div 0,\ 0\div 0\ \text{undefined}

條件：無

規則：and_intro_elim · 依賴：S02, S05, S07, S09, S11, S13, S14

葉節點依據：and_intro_elim

把各步結論合在一起：在 ℕ 中 3+5=8、3·5=15 有定義，3−5、3÷5 沒有定義；在 ℤ 中 3−5=−2 有定義，3÷5 仍沒有定義；在 ℚ 中 3÷5=3/5 有定義；3÷0 與 0÷0 在三個數系中都沒有定義。







## 局部子步與引理

S06.1 · equivalent操作前

b+c=a

操作後

(-b)+(b+c)=(-b)+a

條件：無

規則：eq_congruence · 依賴：eq_congruence, add_inverse

葉節點依據：eq_congruence + add_inverse

在 ℤ（或 ℚ）中每個 b 都有 −b；兩邊同時在左側加上 −b。反向是兩邊同加 b，再用 S06.2 的化簡。



S06.2 · equivalent操作前

(-b)+(b+c)=(-b)+a

操作後

c=a+(-b)

條件：無

規則：eq_replace · 依賴：S06.1

葉節點依據：add_assoc + add_comm + add_inverse + add_zero + eq_replace

化簡左邊：(−b)+(b+c)=((−b)+b)+c=0+c=c（加法結合律、反元素、交換律與單位元）；右邊依交換律 (−b)+a=a+(−b)。S06.1 與 S06.2 合起來證得引理 L_sub。



S08.1 · implies操作前

q\le 0

操作後

5q\le 0<3,\ \text{so}\ 5q\neq 3

條件：5>0

規則：order_basics · 依賴：S08

葉節點依據：order_basics + mul_zero

若 q<0，乘以正數 5 保持順序，得 5q<5·0=0；若 q=0，則 5q=0。所以 5q≤0<3，於是 5q≠3。



S08.2 · implies操作前

q\ge 1

操作後

5q\ge 5>3,\ \text{so}\ 5q\neq 3

條件：5>0

規則：order_basics · 依賴：S08

葉節點依據：order_basics + mul_one

若 q>1，乘以 5>0 得 5q>5·1=5；若 q=1，則 5q=5。所以 5q≥5>3，於是 5q≠3。



S10.1 · equivalent操作前

bq=a

操作後

\tfrac{1}{b}(bq)=\tfrac{1}{b}a

條件：b\neq 0

規則：mul_inverse_nonzero · 依賴：eq_congruence, mul_inverse_nonzero

葉節點依據：eq_congruence + mul_inverse_nonzero

因 b≠0，倒數 1/b 存在；兩邊同乘 1/b。反向是兩邊同乘 b，再用 S10.2 的化簡。若 b=0，1/b 不存在，這一步不能做。



S10.2 · equivalent操作前

\tfrac{1}{b}(bq)=\tfrac{1}{b}a

操作後

q=a\cdot\tfrac{1}{b}

條件：b\neq 0

規則：eq_replace · 依賴：S10.1

葉節點依據：mul_assoc + mul_comm + mul_one + mul_inverse_nonzero + eq_replace

化簡左邊：(1/b)(bq)=((1/b)b)q=1·q=q（乘法結合律、倒數、單位元）；右邊依交換律 (1/b)a=a·(1/b)。S10.1 與 S10.2 合起來證得引理 L_div。







## 逐步反向審查


- S15 · sufficient_goal_reduction · S02, S05, S07, S09, S11, S13, S14, and_intro_elim — 目標 G：對每個數系與每個運算給出判定。足夠條件 H：S02、S05、S07、S09、S11、S13、S14 的結論；H⇒G 只是把它們並列。H 由 G1 到 G3 正向證成，沒有把 G 當作前提。
- S14 · premise_audit · S12, G2, def_unfold — 兩個相異的解就足以推翻唯一性；不宣稱 0÷0 等於某個特定值。
- S13 · premise_audit · S12, contradiction, G2 — 矛盾只依賴 S12 對所有 q 成立與 3≠0；結論是「不存在」，不是「結果為 0」，也不是「結果為無窮大」。
- S12 · premise_audit · mul_zero, mul_comm — mul_zero 對所有 q 成立（理由見規則表）；這一步沒有用到任何關於 q 的額外假設。
- S11 · premise_audit · S10, G2, int_no_gap, order_basics — 需要 S10 的存在與唯一，以及 0<3/5<1；結論只說這個商在 ℚ 中有定義，不說 ℚ 中任何除法都有定義（見 S13、S14）。
- S10.2 · inverse_equivalence · mul_assoc, mul_comm, mul_one, mul_inverse_nonzero — 只把式子換成相等的式子，雙向成立；(1/b)b=1 需要 b≠0。
- S10.1 · inverse_equivalence · eq_congruence, mul_inverse_nonzero — 乘 1/b 與乘 b 互為反運算，前提正是 b≠0。
- S10 · inverse_equivalence · L_div, numeric_evaluation — 反向：代回 5·(3/5)=3。引理的條件 5≠0 成立，兩個方向都已證，所以解存在且唯一。
- S09 · premise_audit · S08, S08.1, S08.2, case_analysis, G2 — 需要兩個情形涵蓋全部整數（S08）；若只檢查了幾個 q，不能推出沒有解。
- S08.2 · premise_audit · order_basics, mul_one — 同 S08.1，用到 5>0；不宣稱反向。
- S08.1 · premise_audit · order_basics, mul_zero — 用到 5>0 才能保持不等號方向；只推出 5q≠3，不宣稱反向。
- S08 · premise_audit · G1, int_no_gap — 分情況需要兩支涵蓋所有整數；這依賴 q 是整數，對有理數 q（例如 3/5）不成立。
- S07 · premise_audit · S06, G1, G2, order_basics — 需要 S06 的存在與唯一，以及 ℕ 的定義；並不宣稱 ℤ 對所有運算都封閉（S09 的除法就不封閉）。
- S06.2 · inverse_equivalence · add_assoc, add_comm, add_inverse, add_zero — 只把式子換成相等的式子，等式的真假不變，雙向成立。
- S06.1 · inverse_equivalence · eq_congruence, add_inverse — 加 −b 與加 b 互為反運算，在 ℤ、ℚ 中沒有附加條件。在 ℕ 中 −b 一般不在 ℕ 內，這一步無法在 ℕ 中進行，這正是 S05 的情形。
- S06 · inverse_equivalence · L_sub, numeric_evaluation — 反向：代回 5+(−2)=3。引理的兩個方向都在子步證明，所以「是解」與「等於 −2」等價，這同時給出存在與唯一。
- S05 · premise_audit · S04, G2, def_unfold — 定義要求解存在且唯一；不存在就已足以判定沒有定義。此結論只對 ℕ 成立；ℤ 在 S06、S07 另行處理。
- S04 · premise_audit · S03, order_basics, quantifier_negation — 需要的是對 ℕ 中每個 c 都成立的不等式，而不只是試了幾個 c；S03 對任意 c 證成，所以結論涵蓋全部 c∈ℕ。
- S03 · premise_audit · G1, order_basics, add_zero — 只用到 c≥0 與加法保持順序；c 是任取的，沒有其他假設。反向（由 5+c≥5 推回 c∈ℕ）不需要，也未宣稱。
- S02 · premise_audit · G1, G3, nat_closed, numeric_evaluation — 需要 3,5∈ℕ 以及 ℕ 對加法、乘法封閉；封閉性只對這兩種運算宣稱，不延伸到減法與除法（見 S05、S09）。
- S01 · premise_audit · G1, G2, mko_arith — 此步只固定數系與定義，不推出新事實；之後每個結論都相對於某個明示的 S。





## 錯誤控制與反例

封閉性取決於數系MKO 指出常見誤解是以為四則運算在所有數系都無條件封閉。本稿顯示：ℕ 對加法與乘法封閉（S02），但 3−5 在 ℕ 中沒有定義（S05）；ℤ 補上了減法（S07），但 3÷5 在 ℤ 中仍沒有定義（S09）；ℚ 中 3÷5=3/5（S11），但除數為零仍然不行（S13、S14）。說「某運算有定義」時，必須同時說出數系。

除以零不是普通的除法MKO 的另一個誤解是把除以零當作普通除法結果。依 G2，a÷b 是 b·q=a 的唯一解。b=0 時 0·q 永遠是 0：若 a≠0（如 3÷0），沒有任何候選值（S13）；若 a=0（0÷0），每個數都是候選值（S14）。兩種情形都不給出結果。「3÷0=0」代回得 0·0=0≠3；「0÷0=1」雖然代回成立，但 q=0 也成立，唯一性不成立。

帶餘除法不是精確除法MKO 提到 3÷2 不是自然數的整除結果。同理，帶餘除法給出 3=5·0+3（商 0、餘 3），但這是另一個運算：G2 的 3÷5 要求 5q=3 恰好成立，而 5·0=0≠3。把帶餘除法的商 0 當作 3÷5 在 ℕ 中的值，等於換了運算而沒有說明。


- 在 ℕ 中 3−5=0 → reject — 代回得 5+0=5≠3；把負的差改寫成 0 的截斷減法是另一個運算，不是 G2 的減法。
- 3÷0=0 → reject — 代回得 0·0=0≠3；依 S13，任何 q 都有 0·q=0≠3，沒有候選值。
- 0÷0=1，因為任何數除以自己都等於 1 → reject — u÷u=1 需要 u≠0；0·q=0 對每個 q 成立，q=0 與 q=1 都是解，解不唯一（S14）。
- 6÷3=2 是整數，所以 ℤ 對除法封閉 → reject — 一個例子不能證明封閉性；3÷5 在 ℤ 中沒有定義（S09），一個反例就足以否定封閉。





## 結論與限制

在 ℕ 中，3+5=8 與 3·5=15 有定義（在 ℤ、ℚ 中是同樣的值）；3−5 與 3÷5 在 ℕ 中沒有定義。在 ℤ（以及 ℚ）中 3−5=−2，但 −2∉ℕ；3÷5 在 ℤ 中沒有定義，在 ℚ 中等於 3/5，而 3/5∉ℤ。3÷0 沒有任何候選值，0÷0 的候選值不唯一，兩者在 ℕ、ℤ、ℚ 中都沒有定義。


- 本稿把 ℕ、ℤ、ℚ 的運算與順序性質（nat_closed、int_no_gap、order_basics 等）當作前提，不在此建構這些數系。
- G2 是以唯一解定義差與商的一種常見約定；截斷減法、帶餘除法，或程式語言中對 a÷0 的特別約定，是不同的運算，需要各自的定義。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: ef166229ecdb3b0f44715ad7924ab80f5ce26775fb834d7df17af4dbc883ea69
- original source SHA-256: ef166229ecdb3b0f44715ad7924ab80f5ce26775fb834d7df17af4dbc883ea69
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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