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

目標與範圍

取 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)。

逐步主鏈

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)

3,5\in\mathbb{N}

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

c\in\mathbb{N}

5+c\ge 5

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

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

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

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

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

c=3+(-5)=-2

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

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

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

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

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}

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

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

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}

q\in\mathbb{Q}

0\cdot q=0

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

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

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

局部子步與引理

b+c=a

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

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

c=a+(-b)

q\le 0

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

q\ge 1

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

bq=a

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

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

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

逐步反向審查

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