# 整數：判定成員、負號的意義與對負號的封閉性

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

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

derivation-mko-integer-01 · production-20261019-adopted-96



## 目標與範圍

在實數中，取 Z={0}∪N⁺∪{−n ∣ n∈N⁺}（N 依 OCME 慣例含 0，N⁺=N∖{0}，−n 是 n 的加法反元素）。證明 −7∈Z；說明十進位符號「3.0」表示整數 3；證明 −2.5∉Z；由加法反元素的唯一性證明 −(−a)=a，特別是 −(−4)=4；對所有 z∈Z 證明 −z∈Z；並以 5−8=5+(−8)=−3 分辨二元減法與一元負號。

只處理 MKO 建立的成員與符號邊界：Z 的三部分、負號作為加法反元素、對負號的封閉性。在 ℝ 中描述 Z（只用到加法公理與序），N 以「最小歸納集」刻畫並作為前提。不證明 Z 對加法、乘法封閉，也不處理序與整除（MKO 說這些需要各自的聲明）；不處理與 Lean Int 的語義對應；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- add_assoc
- add_comm
- add_zero
- add_inverse
- order_basics
- numeric_evaluation


- G1 — 在實數 ℝ 中討論（只用到加法公理與序）。N⊆ℝ 是 OCME 慣例下的自然數（含 0，MKO 假設 a1），它是 ℝ 中最小的歸納集：0∈N、x∈N ⇒ x+1∈N，且任何含 0 並對 x↦x+1 封閉的 T⊆ℝ 都包含 N。
- G2 — N⁺=N∖{0}；Z={0}∪N⁺∪{−n ∣ n∈N⁺}。
- G3 — −a 表示 a 的加法反元素（a+(−a)=0）；二元減法 a−b 定義為 a+(−b)。
- G4 — 要判定或計算的對象：−7、十進位符號「3.0」、−2.5、−(−4)、5−8。


- \mathbb{Z} — 整數集合
- N,\ N^{+} — 自然數（含 0）與正自然數 N∖{0}
- -a — a 的加法反元素（一元負號）
- a-b — 二元減法，定義為 a+(−b)
- T_3 — 歸納集 {0,1,2}∪{x ∣ x≥3}





## 規則與來源


- add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
- add_comm · prerequisite — 加法交換律：u+v=v+u。
- add_zero · prerequisite — 加法單位元：u+0=u。
- add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
- 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 — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- set_operations_def · prerequisite — 集合運算：x∈A∪B ⇔ x∈A 或 x∈B；x∈A∩B ⇔ x∈A 且 x∈B；x∈A∖B ⇔ x∈A 且 x∉B；在全集 U 中 Aᶜ=U∖A。
- exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
- power_laws · prerequisite — 整數指數律（底數非零或指數為正整數）：a^m·a^n=a^{m+n}，(a^m)^n=a^{mn}，(ab)^n=a^n b^n，a^0=1。
- eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。
- subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。
- de_morgan_logic · prerequisite — 邏輯的德摩根律：¬(P∧Q) ⇔ ¬P∨¬Q；¬(P∨Q) ⇔ ¬P∧¬Q。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。
- forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_int_def · cited — 整數集合 Z 包含 0、每個正自然數及其負數；符號 n∈Z 表示 n 是整數。 · mko-integer
- nat_least_inductive · prerequisite — N 是 ℝ 中最小的歸納集：0∈N，x∈N ⇒ x+1∈N；若 T⊆ℝ 含 0 且對 x↦x+1 封閉，則 N⊆T。
- positional_def · prerequisite — 十進位小數符號：整數部分各位數 d_i 表示 Σ d_i 10^i，小數點後第 j 位數 e_j 表示 e_j 10^{−j}，兩者相加；例如「3.0」表示 3·10⁰+0·10⁻¹。
- L_N_T3 · lemma — 令 T₃={0,1,2}∪{x∈ℝ ∣ x≥3}，則 N⊆T₃。
- L_inv_unique · lemma — 對實數 a、x、y：若 a+x=0 且 a+y=0，則 x=y（加法反元素唯一）。





## 逐步主鏈

S01 · definition操作前

z\in\mathbb{Z}

操作後

z=0\ \lor\ z\in N^{+}\ \lor\ \exists n\in N^{+}:\ z=-n

條件：無

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

葉節點依據：mko_int_def + def_unfold + set_operations_def

依 MKO，Z 由三部分組成：0、正自然數、正自然數的負數。所以判定 z∈Z，就是判定三個析取項中是否至少一個成立。這裡 −n 是 n 的加法反元素，不是「減掉 n」這個動作（G3）。



S02 · implies操作前

7=0+1+1+1+1+1+1+1

操作後

7\in N^{+},\ -7\in\mathbb{Z}

條件：無

規則：exists_intro · 依賴：S01, G1

葉節點依據：exists_intro + nat_least_inductive + set_operations_def + numeric_evaluation

7 由 0 經七次後繼得到（N1），G1 的封閉性連用七次給出 7∈N；7≠0，故 7∈N⁺。取 n=7，則 −7=−n，第三個析取項成立，依 ∃引入 −7∈Z。



S03 · implies操作前

\text{decimal numeral }3.0

操作後

3\cdot10^0+0\cdot10^{-1}=3\in N^{+}\subseteq\mathbb{Z}

條件：無

規則：positional_def · 依賴：S01, G4, positional_def

葉節點依據：positional_def + power_laws + numeric_evaluation + set_operations_def

十進位符號「3.0」表示 3·10⁰+0·10⁻¹=3。3 由 0 經三次後繼得到，3∈N 且 3≠0，所以 3∈N⁺，第二個析取項成立，3∈Z。符號中的小數點不改變數值；判定整數看的是數，不是符號的外觀。



S04 · equivalent操作前

-2.5\in\mathbb{Z}

操作後

-2.5=0\ \lor\ -2.5\in N^{+}\ \lor\ \exists n\in N^{+}:\ -2.5=-n

條件：無

規則：def_unfold · 依賴：S01, G4

葉節點依據：def_unfold + mko_int_def

對 −2.5（即 −5/2，N3）展開 S01 的成員條件。要證 −2.5∉Z，三個析取項都必須排除。



S05 · equivalent操作前

-2.5=-n

操作後

n=2.5

條件：無

規則：eq_congruence · 依賴：G3, eq_congruence

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

兩邊同加 n+2.5：左邊 −2.5+(n+2.5)=n，右邊 −n+(n+2.5)=2.5（加法交換、結合與反元素），得 n=2.5。反向：n=2.5 時，兩邊同取加法反元素得 −n=−2.5。所以「−2.5 等於某個 −n」恰好等於「n=2.5」。



S06 · implies操作前

T_3=\{0,1,2\}\cup\{x\in\mathbb{R}\mid x\ge 3\}

操作後

N\subseteq T_3

條件：無

規則：L_N_T3 · 依賴：G1, L_N_T3

葉節點依據：L_N_T3

依引理 L_N_T3，每個自然數要不是 0、1、2，就是 ≥3。所以 2 與 3 之間沒有自然數，而且每個自然數都 ≥0。引理在 S06.1、S06.2 證明。



S07 · implies操作前

N\subseteq T_3

操作後

2.5\notin N,\ -2.5\notin N

條件：無

規則：contrapositive · 依賴：S06, G4

葉節點依據：contrapositive + subset_def + order_basics + numeric_evaluation

2.5 不等於 0、1、2，且 2.5<3，所以 2.5∉T₃；−2.5<0，而 T₃ 的元素都 ≥0，所以 −2.5∉T₃。因 N⊆T₃，依逆否 2.5∉N、−2.5∉N。



S08 · implies操作前

\text{the three disjuncts of S04}

操作後

-2.5\notin\mathbb{Z}

條件：無

規則：de_morgan_logic · 依賴：S04, S05, S07

葉節點依據：de_morgan_logic + set_operations_def + quantifier_negation

第一項：−2.5≠0。第二項：−2.5∉N，所以也不在 N⁺⊆N 中。第三項：依 S05，它等於「2.5∈N⁺」，但 2.5∉N（S07）。三項都不成立，依德摩根律析取為假，依 S04 的等價 −2.5∉Z。



S09 · implies操作前

(-a)+a=0,\ (-a)+(-(-a))=0

操作後

-(-a)=a\quad(a\in\mathbb{R})

條件：無

規則：L_inv_unique · 依賴：G3, L_inv_unique

葉節點依據：L_inv_unique + add_comm + add_inverse + forall_intro

對任意實數 a：依加法交換律 (−a)+a=a+(−a)=0，所以 a 是 −a 的一個加法反元素；依定義 −(−a) 也是 −a 的加法反元素。依引理 L_inv_unique（取 L_inv_unique 中的 a 為 −a），−(−a)=a。a 是任意的，所以對所有實數成立。引理在 S09.1、S09.2 證明。



S10 · implies操作前

-(-4)

操作後

4\in N^{+}\subseteq\mathbb{Z}

條件：無

規則：forall_elim · 依賴：S09, S01

葉節點依據：forall_elim + numeric_evaluation + set_operations_def

在 S09 中取 a=4：−(−4)=4。驗算 (−4)+4=0（N8）。4 由 0 經四次後繼得到且 4≠0，所以 4∈N⁺⊆Z；−4 本身也是整數（第三部分，n=4）。



S11 · implies操作前

z\in\mathbb{Z}

操作後

-z\in\mathbb{Z}

條件：無

規則：case_analysis · 依賴：S01, S09

葉節點依據：case_analysis + L_inv_unique + forall_intro + exists_intro

依 S01 分三種情況。(i) z=0：0+0=0，所以 0 是 0 的反元素，依唯一性 −0=0∈Z。(ii) z∈N⁺：取 n=z，−z 屬於第三部分。(iii) z=−n（n∈N⁺）：依 S09，−z=−(−n)=n∈N⁺⊆Z。三種情況涵蓋 Z 的全部元素，所以對每個整數 z，−z∈Z。這是對任意 z 的證明，不是由幾個例子歸納。



S12 · implies操作前

5-8=5+(-8)

操作後

5+(-8)=-3

條件：無

規則：L_inv_unique · 依賴：G3, L_inv_unique

葉節點依據：L_inv_unique + add_comm + add_assoc + add_inverse + numeric_evaluation

依 G3，二元減法 5−8 定義為 5+(−8)。計算 3+(5+(−8))=(3+5)+(−8)=8+(−8)=0（結合律與反元素），又 3+(−3)=0；依引理 L_inv_unique（a=3），5+(−8)=−3。這裡出現兩種「−」：5−8 中的是二元運算（減法），−3 中的是一元記號（3 的反元素）；運算的結果是 −3 這個數，而 −3∈Z（3∈N⁺）。



S13 · implies操作前

\text{S02, S03, S08, S10, S11, S12}

操作後

-7,\ 3,\ 4,\ -3\in\mathbb{Z};\ -2.5\notin\mathbb{Z};\ \forall z\in\mathbb{Z}:\ -z\in\mathbb{Z}

條件：無

規則：and_intro_elim · 依賴：S02, S03, S08, S10, S11, S12

葉節點依據：and_intro_elim

−7、3（寫成 3.0）、−(−4)=4、5−8=−3 都是整數；−2.5 不是；而且 Z 對負號封閉。







## 局部子步與引理

S06.1 · implies操作前

0\in T_3;\ x\in\{0,1,2\}

操作後

x+1\in\{1,2,3\}\subseteq T_3

條件：無

規則：case_analysis · 依賴：G1, nat_least_inductive

葉節點依據：case_analysis + numeric_evaluation + order_basics

0∈T₃。x=0、1、2 時，x+1 分別是 1、2、3；1、2 在 {0,1,2} 中，3≥3，所以都在 T₃ 中。



S06.2 · implies操作前

x\ge 3

操作後

x+1\ge 4\ge 3;\ T_3\ \text{inductive},\ N\subseteq T_3

條件：無

規則：nat_least_inductive · 依賴：S06.1, nat_least_inductive

葉節點依據：nat_least_inductive + case_analysis + order_basics

x≥3 時 x+1≥4≥3，所以 x+1∈T₃。T₃ 的元素不是在 {0,1,2} 中就是 ≥3，兩種情況（S06.1 與此處）涵蓋全部，所以 T₃ 對 x↦x+1 封閉；加上 0∈T₃，T₃ 是歸納集。依 G1 的最小性，N⊆T₃。S06.1 與 S06.2 合起來證得引理 L_N_T3。



S09.1 · implies操作前

a+x=0,\ a+y=0

操作後

x=x+0=x+(a+y)=(x+a)+y

條件：無

規則：add_assoc · 依賴：add_zero, add_assoc

葉節點依據：add_zero + eq_replace + add_assoc

x=x+0（加法單位元）=x+(a+y)（以假設 0=a+y 代換）=(x+a)+y（結合律）。



S09.2 · implies操作前

(x+a)+y

操作後

y,\ \text{hence}\ x=y

條件：無

規則：add_comm · 依賴：S09.1, add_comm

葉節點依據：add_comm + eq_replace + add_zero + eq_refl_symm_trans

(x+a)+y=(a+x)+y（交換律）=0+y（以假設 a+x=0 代換）=y。與 S09.1 串接得 x=y。S09.1 與 S09.2 合起來證得引理 L_inv_unique。







## 逐步反向審查


- S13 · sufficient_goal_reduction · S02, S03, S08, S09, S10, S11, S12 — 目標是 goal 所列各項。足夠條件 H：S02、S03、S08、S10、S11、S12 各自成立；H 推出目標只用合取。普遍敘述（S09、S11）由任意元素的論證得到，沒有把目標當作前提。
- S12 · premise_audit · L_inv_unique, add_assoc, add_inverse, numeric_evaluation — 套用唯一性需要兩個等式 3+x=0 與 3+y=0，x=5+(−8)、y=−3；兩者都已驗證（N9、N11）。
- S11 · premise_audit · S01, S09, case_analysis, L_inv_unique, forall_intro — 三種情況必須對應 S01 的三個析取項，缺一不可。
- S10 · premise_audit · S09, forall_elim — 這是一般結論的特例；反過來，這個例子不能證明一般結論。
- S09.2 · premise_audit · add_comm, eq_replace, add_zero, eq_refl_symm_trans — 兩個假設 a+x=0、a+y=0 各用一次；等號傳遞把兩段串起來。
- S09.1 · premise_audit · add_zero, eq_replace, add_assoc — 用到假設 a+y=0 作一次代換。
- S09 · premise_audit · L_inv_unique, add_comm, forall_intro — 結論依賴反元素唯一；它不是背誦「負負得正」，而是唯一性的推論。
- S08 · premise_audit · S04, S05, S07, de_morgan_logic — 三項都須排除；只說「−2.5 是負數」不夠，因為 −7 也是負數卻是整數。
- S07 · premise_audit · S06, contrapositive, subset_def, order_basics — 逆否與包含關係等價；不宣稱 T₃ 的每個元素都是自然數。
- S06.2 · premise_audit · S06.1, nat_least_inductive, case_analysis, order_basics — 最小性只要求 T₃ 含 0 且對後繼封閉；不需要 T₃⊆N（事實上 3.5∈T₃ 不是自然數）。
- S06.1 · premise_audit · case_analysis, numeric_evaluation — 三個情況逐一檢查。
- S06 · premise_audit · L_N_T3 — 此步只引用引理；證明在子步。
- S05 · inverse_equivalence · eq_congruence, add_inverse, add_comm, add_assoc — 兩個方向都是對等式兩邊做同一個有定義的運算。
- S04 · inverse_equivalence · S01, def_unfold — 定義展開，雙向成立。
- S03 · premise_audit · positional_def, S01, numeric_evaluation — 需要的是符號所表示的數；只看外觀（有沒有小數點）不能判定。
- S02 · premise_audit · S01, exists_intro, nat_least_inductive — 只需找到一個 n∈N⁺；不需要也不宣稱唯一性。
- S01 · premise_audit · mko_int_def, G2, G3, def_unfold — 此步只展開定義；三部分涵蓋 MKO 所列的全部成員。





## 錯誤控制與反例

負號不是減法本身MKO 指出的誤解之一是把負號當成減法操作本身。−3 是一個數：3 的加法反元素，滿足 3+(−3)=0；5−8 是一個運算，定義為 5+(−8)，它的值才是 −3（S12）。−(−4)=4 也不是背誦的規則，而是反元素唯一性的結果（S09）。

小數點不決定是否為整數MKO 指出的另一誤解與帶小數點的寫法有關。「3.0」帶有小數點，表示的卻是整數 3（S03）；「−2.5」表示的數不是整數（S08）。判定看的是符號所表示的數，以及它是否落在 Z 的三部分之一，不看寫法。

例子不能推出普遍代數律MKO 提醒不要由幾個例子推得全部整數代數律。驗算 −(−4)=4、−(−7)=7（N12）不證明 −(−z)=z 對所有 z 成立；S09 對任意實數 a 證明，S11 以分情況證明對負號的封閉性。至於 Z 對加法、乘法的封閉性，本稿沒有證明，需要各自的聲明。


- −2.5 是整數，因為它是負數，而整數包含負數 → reject — Z 中的負數只能是正自然數的負數；2.5 不是自然數（S07），所以 −2.5∉Z（S08）。
- 3.0 不是整數，因為它寫有小數點 → reject — 「3.0」表示 3，而 3∈N⁺⊆Z（S03）。
- −3 表示「從某數減去 3」這個運算 → reject — −3 是滿足 3+(−3)=0 的數；5−8 才是運算 5+(−8)，其值為 −3（S12）。
- 因為 −(−4)=4、−(−7)=7，所以 −(−z)=z 已對所有整數證明 → reject — 有限個例子不能證明普遍命題；一般證明在 S09（反元素唯一性）。





## 結論與限制

依 Z={0}∪N⁺∪{−n ∣ n∈N⁺}：−7∈Z；「3.0」表示 3∈Z；因 N⊆{0,1,2}∪{x ∣ x≥3}，2.5 與 −2.5 都不是自然數，所以 −2.5∉Z。加法反元素唯一，故 −(−a)=a，特別是 −(−4)=4；對每個 z∈Z 都有 −z∈Z。5−8 是運算 5+(−8)，其值是數 −3∈Z。


- Z 對加法、乘法的封閉性，以及序與整除的性質需要各自的聲明，本稿不證明（MKO 說明）。
- nat_least_inductive 是前提（自然數 MKO 的形式讀法）；在 OCME 的建構鏈中 ℝ 由 ℚ、ℤ、N 建成，本稿只把 ℝ 當作討論成員問題的環境。
- 與 Lean Int 的構造、自然數嵌入與負數的語義對應（MKO formal next）未在此處理。





## 驗證及來源綁定

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


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

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