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

目標與範圍

在實數中，取 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（加法反元素唯一）。

逐步主鏈

z\in\mathbb{Z}

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

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

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

\text{decimal numeral }3.0

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

-2.5\in\mathbb{Z}

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

-2.5=-n

n=2.5

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

N\subseteq T_3

N\subseteq T_3

2.5\notin N,\ -2.5\notin N

\text{the three disjuncts of S04}

-2.5\notin\mathbb{Z}

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

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

-(-4)

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

z\in\mathbb{Z}

-z\in\mathbb{Z}

5-8=5+(-8)

5+(-8)=-3

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

局部子步與引理

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

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

x\ge 3

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

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

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

(x+a)+y

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

逐步反向審查

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