# 自然數：以最小歸納集判定成員，並分辨數與數字符號

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

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

derivation-mko-natural-number-01 · production-20261019-adopted-96



## 目標與範圍

依 OCME 慣例（0∈N），把 MKO 的「0 以及由 0 經有限次後繼所得的數」讀成「實數中包含 0 且對 x↦x+1 封閉的最小集合」。據此證明 0∈N、3∈N；說明二進位符號「11」與十進位符號「3」表示同一個自然數；證明 −1∉N 與 1/2∉N；並與「自然數從 1 開始」的慣例 N⁺=N∖{0} 比較最小元素。

在實數 ℝ 中討論（只用到加法與序的性質），以便判定 −1、1/2 這類數是否屬於 N；這是 N 在 ℝ 中的刻畫，不是 N 的基礎建構（在 OCME 的建構鏈中 ℝ 反而由 ℚ、ℤ、N 建成）。不處理 Peano 公理、與 Lean Nat 的語義橋，也不證明「最小歸納集」與「有限次後繼」兩種說法的等價；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- order_basics
- subset_def
- set_operations_def
- numeric_evaluation


- G1 — 討論的數都是實數；後繼運算是 S(x)=x+1。n 表示任意一個待判定是否屬於 N 的數（MKO 假設 a2）。
- G2 — MKO 的形式讀法：子集 T⊆ℝ 稱為歸納集，若 0∈T，且對每個 x∈T 都有 x+1∈T。N 定義為 ℝ 的所有歸納子集的交集，即包含 0 且對後繼封閉的最小集合。依本條目慣例，N 包含 0（MKO 假設 a1）。
- G3 — 位值記數：以 b 為底、由右至左數字依序為 d₀、d₁ 等直到 d_k 的數字符號，表示的數是 Σ_{i=0}^{k} d_i b^i。
- G4 — 要判定的數：0、3、−1、1/2；數字符號：十進位「3」、二進位「11」。


- N — OCME 慣例下的自然數集合（含 0）
- N^{+} — N∖{0}，從 1 開始的慣例
- S(x)=x+1 — 後繼
- T_1,\ T_2 — 兩個用來排除非自然數的歸納集
- \bigcap — 集合族的交集





## 規則與來源


- 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。
- subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。
- 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。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
- add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
- modus_ponens · prerequisite — 肯定前件：由 P 與 P⇒Q 得 Q。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- power_laws · prerequisite — 整數指數律（底數非零或指數為正整數）：a^m·a^n=a^{m+n}，(a^m)^n=a^{mn}，(ab)^n=a^n b^n，a^0=1。
- add_zero · prerequisite — 加法單位元：u+0=u。
- contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_nat_def · cited — 在本條目的慣例中，自然數集合 N 包含 0，並包含 0 經有限次後繼所得的 1、2、3 等數。 · mko-natural-number
- inductive_def · prerequisite — 歸納集：T⊆ℝ 若 0∈T 且對每個 x∈T 都有 x+1∈T，則稱 T 為歸納集。
- nat_as_intersection · prerequisite — N=⋂{T⊆ℝ ∣ T 是歸納集}：x∈N 當且僅當 x 屬於每一個歸納集。
- big_intersection_def · prerequisite — 集合族的交集：對非空集合族 𝓕，x∈⋂𝓕 ⇔ 對每個 T∈𝓕 都有 x∈T；因此對每個 T∈𝓕 都有 ⋂𝓕⊆T。
- positional_def · prerequisite — 位值記數：以 b 為底、數字由右至左為 d₀、d₁ 等到 d_k 的符號表示 Σ_{i=0}^{k} d_i b^i。
- L_N_inductive · lemma — N 本身是歸納集：0∈N，且對每個 x∈N 都有 x+1∈N。





## 逐步主鏈

S01 · definition操作前

N

操作後

N=\bigcap\{T\subseteq\mathbb{R}\mid 0\in T,\ \forall x\in T:\ x+1\in T\}

條件：無

規則：nat_as_intersection · 依賴：G1, G2, mko_nat_def

葉節點依據：nat_as_intersection + inductive_def + big_intersection_def

MKO 說 N 包含 0 與由 0 經有限次後繼得到的數。若把「有限次」直接當定義會循環（必須先知道什麼是有限，也就是自然數），所以採 G2 的讀法：N 是所有歸納集的交集。這個集合族不空，因為 ℝ 本身是歸納集（0∈ℝ，x∈ℝ ⇒ x+1∈ℝ），所以交集有定義且 N⊆ℝ。



S02 · implies操作前

N=\bigcap\{T\ \text{inductive}\}

操作後

0\in N,\ \forall x\in N:\ x+1\in N

條件：無

規則：L_N_inductive · 依賴：S01, L_N_inductive

葉節點依據：L_N_inductive

依引理 L_N_inductive，N 本身含 0 並對後繼封閉；這兩點正是 MKO 文字中的「包含 0」與「自然數的後繼仍是自然數」。0∈N 也就是 OCME 的慣例（假設 a1）。引理在 S02.1、S02.2 證明。



S03 · implies操作前

T\subseteq\mathbb{R}\ \text{inductive}

操作後

N\subseteq T

條件：無

規則：big_intersection_def · 依賴：S01, big_intersection_def

葉節點依據：big_intersection_def + subset_def + forall_elim

交集包含於族中的每一個集合：若 x∈N，x 屬於每個歸納集，特別屬於 T。這就是本稿用的歸納原理：要證每個自然數都在某個集合 T 中，只需證明 T 是歸納集。與 S02 合看，N 是最小的歸納集。



S04 · equivalent操作前

3

操作後

((0+1)+1)+1

條件：無

規則：numeric_evaluation · 依賴：G4

葉節點依據：numeric_evaluation + add_assoc

把 3 寫成從 0 出發的三次後繼：0+1=1，1+1=2，2+1=3，所以 3=S(S(S(0)))。



S05 · implies操作前

0\in N

操作後

1\in N,\ 2\in N,\ 3\in N

條件：無

規則：L_N_inductive · 依賴：S02, S04

葉節點依據：L_N_inductive + modus_ponens + eq_replace

由 0∈N 與後繼封閉（S02）連用三次：0∈N ⇒ 1∈N ⇒ 2∈N ⇒ 3∈N。這正是 MKO 所說「經有限次（這裡是三次）後繼所得」。



S06 · equivalent操作前

\text{binary numeral }11,\ \text{decimal numeral }3

操作後

1\cdot2^1+1\cdot2^0=3=3\cdot10^0

條件：無

規則：positional_def · 依賴：G3, S05

葉節點依據：positional_def + power_laws + numeric_evaluation

依位值記數，二進位符號「11」表示 1·2¹+1·2⁰=2+1=3，十進位符號「3」表示 3·10⁰=3。兩個不同的符號表示同一個數 3，而 3∈N（S05）。是否屬於 N 是數的性質，不是符號的性質。



S07 · implies操作前

T_1=\{x\in\mathbb{R}\mid x\ge 0\}

操作後

T_1\ \text{inductive}

條件：無

規則：inductive_def · 依賴：G1, inductive_def

葉節點依據：inductive_def + order_basics + add_zero

0≥0，所以 0∈T₁。若 x≥0，則 x+1≥0+1=1>0（序的加法性質與 0<1），所以 x+1∈T₁。兩條都成立，T₁ 是歸納集。



S08 · implies操作前

T_1\ \text{inductive}

操作後

N\subseteq T_1:\ \forall n\in N,\ n\ge 0

條件：無

規則：big_intersection_def · 依賴：S03, S07, S02

葉節點依據：big_intersection_def + subset_def + order_basics

依 S03 的歸納原理，N⊆T₁：每個自然數都 ≥0。配合 0∈N（S02），0 是 N 的最小元素。



S09 · implies操作前

-1<0

操作後

-1\notin N

條件：無

規則：contrapositive · 依賴：S08, G4

葉節點依據：contrapositive + subset_def + order_basics

−1<0，所以 −1∉T₁；因 N⊆T₁，依包含關係的逆否（x∈N ⇒ x∈T₁ 等價於 x∉T₁ ⇒ x∉N），−1∉N。注意 −1+1=0∈N 並不使 −1 成為自然數：後繼封閉只往前推，不往回推。



S10 · implies操作前

T_2=\{0\}\cup\{x\in\mathbb{R}\mid x\ge 1\}

操作後

T_2\ \text{inductive}

條件：無

規則：inductive_def · 依賴：G1, inductive_def

葉節點依據：inductive_def + case_analysis + set_operations_def

要排除 1/2，T₁ 太粗（1/2∈T₁），需要更細的歸納集 T₂。T₂ 含 0；對後繼的封閉性分兩種情況在 S10.1、S10.2 證明，因 T₂ 的元素只有 x=0 與 x≥1 兩類。



S11 · implies操作前

T_2\ \text{inductive}

操作後

N\subseteq T_2

條件：無

規則：big_intersection_def · 依賴：S03, S10, S10.2

葉節點依據：big_intersection_def + subset_def

依歸納原理 S03，N⊆T₂：每個自然數要不是 0，就是 ≥1。所以 0 與 1 之間沒有自然數。



S12 · implies操作前

\tfrac{1}{2}\neq 0,\ \tfrac{1}{2}<1

操作後

\tfrac{1}{2}\notin N

條件：無

規則：contrapositive · 依賴：S11, G4

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

1/2≠0，且 1/2<1，所以 1/2∉T₂；因 N⊆T₂，依逆否 1/2∉N。這不能靠列出 0、1、2、3 再觀察 1/2 不在其中來證：列出有限個元素永遠列不完 N，必須用歸納集的論證。



S13 · definition操作前

N^{+}=N\setminus\{0\}

操作後

0\notin N^{+},\ 3\in N^{+},\ \min N^{+}=1,\ \min N=0

條件：無

規則：set_operations_def · 依賴：S02, S05, S08, S11

葉節點依據：set_operations_def + def_intro + order_basics

有些教材所說的自然數是 N⁺=N∖{0}（從 1 開始）。依集合差的定義 0∉N⁺；3∈N 且 3≠0，所以 3∈N⁺。由 N⊆T₂，N⁺ 的元素都 ≥1，而 1∈N（S05），所以 N⁺ 的最小元素是 1；在 OCME 的 N 中最小元素是 0（S08）。同一句「最小的自然數」在兩個慣例下答案不同。



S14 · implies操作前

\text{S05, S06, S09, S12, S13}

操作後

0,3\in N;\ 11_{2}=3_{10};\ -1,\tfrac{1}{2}\notin N;\ \min N=0,\ \min N^{+}=1

條件：無

規則：and_intro_elim · 依賴：S05, S06, S09, S12, S13

葉節點依據：and_intro_elim

在 OCME 慣例下 0、3 是自然數；「11」（二進位）與「3」（十進位）是同一個自然數的兩種寫法；−1 與 1/2 不是自然數；N 的最小元素是 0，而 N⁺ 慣例下是 1。







## 局部子步與引理

S02.1 · implies操作前

T\ \text{inductive}\Rightarrow 0\in T

操作後

0\in N

條件：無

規則：big_intersection_def · 依賴：S01, big_intersection_def

葉節點依據：inductive_def + big_intersection_def + forall_intro

每個歸納集都含 0（歸納集定義的第一條），所以 0 屬於族中每一個集合；依交集的定義，0∈N。



S02.2 · implies操作前

x\in N

操作後

x+1\in N

條件：無

規則：big_intersection_def · 依賴：S01, big_intersection_def

葉節點依據：forall_elim + forall_intro + inductive_def + big_intersection_def

設 x∈N，任取一個歸納集 T。因 x 屬於每個歸納集，x∈T；T 對後繼封閉，所以 x+1∈T。T 是任意取的（沒有額外假設），所以 x+1 屬於每個歸納集，即 x+1∈N。S02.1 與 S02.2 合起來證得引理 L_N_inductive。



S10.1 · implies操作前

x=0

操作後

x+1=1\in T_2

條件：無

規則：order_basics · 依賴：S10

葉節點依據：order_basics + add_zero + set_operations_def

x=0 時 x+1=1，而 1≥1，所以 1∈T₂。



S10.2 · implies操作前

x\ge 1

操作後

x+1\ge 2\ge 1,\ x+1\in T_2

條件：無

規則：order_basics · 依賴：S10, S10.1

葉節點依據：order_basics + case_analysis

x≥1 時 x+1≥1+1=2≥1，所以 x+1∈T₂。兩種情況涵蓋 T₂ 的全部元素，依分情況論證 T₂ 對後繼封閉；加上 0∈T₂，T₂ 是歸納集。







## 逐步反向審查


- S14 · sufficient_goal_reduction · S03, S05, S06, S09, S12, S13 — 目標是 goal 所列各項。足夠條件 H：S05、S06、S09、S12、S13 各自成立；H 推出目標只用合取。排除 −1、1/2 的部分依賴 S03 的歸納原理與兩個歸納集，沒有把目標當作前提。
- S13 · premise_audit · set_operations_def, S11, S08, S05 — 兩個最小元素的結論各自需要「下界」與「下界本身屬於集合」兩件事。
- S12 · premise_audit · S11, contrapositive, set_operations_def — 1/2 必須同時不等於 0 且不 ≥1，才不在 T₂ 的兩個部分之中。
- S11 · premise_audit · S03, S10.2 — 只需 T₂ 是歸納集；不宣稱 T₂⊆N。
- S10.2 · premise_audit · order_basics, case_analysis, S10.1 — 用到序的加法性質 u<v ⇒ u+w<v+w（等號情況同理）；兩種情況合起來才得到封閉性。
- S10.1 · premise_audit · order_basics, add_zero — 直接計算，沒有附加條件。
- S10 · premise_audit · inductive_def, case_analysis, set_operations_def — x∈T₂ 只有兩種可能，兩種情況都必須處理，否則封閉性未證完。
- S09 · premise_audit · S08, contrapositive, subset_def — 逆否命題與原命題等價；不宣稱逆命題（x∈T₁ ⇒ x∈N），事實上 1/2∈T₁ 卻不是自然數。
- S08 · premise_audit · S03, S07, S02 — 只用到 T₁ 是歸納集；「最小元素」還需要 0 本身在 N 中。
- S07 · premise_audit · inductive_def, order_basics — 需要 0<1；若「後繼」是 x↦x−1，T₁ 就不再封閉。
- S06 · inverse_equivalence · positional_def, numeric_evaluation — 兩個求值都是精確計算（N2、N3），等式雙向成立。
- S05 · premise_audit · S02, S04, modus_ponens — 每一步都是肯定前件；反向（由 3∈N 推回 2∈N）並未宣稱，也不需要。
- S04 · inverse_equivalence · numeric_evaluation — 精確整數運算，雙向成立（N1）。
- S03 · premise_audit · big_intersection_def, subset_def, forall_elim — 只需要 T 是歸納集；不需要也不宣稱 T⊆N。
- S02.2 · premise_audit · inductive_def, big_intersection_def, forall_intro, forall_elim — T 必須是任意的；若只對某一個歸納集驗證，不能推出 x+1 屬於交集。
- S02.1 · premise_audit · inductive_def, big_intersection_def — 需要「每一個」歸納集都含 0；只找到一個含 0 的集合不夠。
- S02 · premise_audit · L_N_inductive, S01 — 此步只引用引理；兩個部分各自在子步證明。
- S01 · premise_audit · G2, nat_as_intersection, mko_nat_def, big_intersection_def — 此步只採用定義；它與 MKO 文字讀法的等價列為開放項目，不在此證明。





## 錯誤控制與反例

0 是否屬於自然數取決於慣例MKO 指出的誤解是以為所有教材對自然數是否包含 0 都相同。OCME 固定 0∈N（與 Lean 的 Nat 一致），但有些教材的自然數從 1 開始（本稿的 N⁺）。同一句「最小的自然數」在 OCME 是 0，在 N⁺ 慣例是 1（S13）。閱讀外部資料時要先確認它的定義。

數與數字符號MKO 的另一個誤解是把數字的書寫方式與數本身混為一談。字串「10」在十進位表示十（1·10+0=10，N12），在二進位表示二（1·2+0=2，N11）；「11」（二進位）與「3」（十進位）表示同一個數，二進位「110」與十進位「6」也表示同一個數（N13）。是否屬於 N 是數的性質，判定前要先確定符號用哪一個底。

排除一個數需要歸納集，不是列舉要證 1/2∉N，不能列出 0、1、2、3 後說「1/2 不在表上」：表永遠是有限的，N 不是。也不能說「1/2 不是由 0 經有限次後繼得到」而不加證明，那正是要證的事。正確做法是找一個歸納集 T₂ 不含 1/2（S10 到 S12）。同理，−1+1=0∈N 不推出 −1∈N，因為封閉性只往前推。


- 所有教材都把 0 算作自然數 → reject — 慣例不同；許多教材的自然數從 1 開始（N⁺），MKO 明確提醒要先確認定義。
- 字串「10」永遠表示十 → reject — 在二進位中「10」表示 1·2+0=2（N11）。
- 1/2 是自然數，因為它可由 0 加上 1/2 得到 → reject — 後繼只允許加 1；T₂ 是不含 1/2 的歸納集，所以 1/2∉N（S12）。
- −1 是自然數，因為 −1+1=0∈N → reject — 封閉性是 x∈N ⇒ x+1∈N，不是反向；N⊆{x ∣ x≥0} 排除 −1（S09）。





## 結論與限制

把 N 讀成實數中含 0 且對 x↦x+1 封閉的最小集合：0∈N，3=S(S(S(0)))∈N；二進位「11」與十進位「3」都表示 3；因 N⊆{x ∣ x≥0}，−1∉N；因 N⊆{0}∪{x ∣ x≥1}，1/2∉N。OCME 的 N 最小元素是 0，而 N⁺=N∖{0} 的最小元素是 1。


- 本稿採用「最小歸納集」作為 MKO「由 0 經有限次後繼所得」的形式讀法；兩種說法等價的證明，以及與 Peano 公理或 Lean Nat 的語義橋（MKO formal next），未在此處理。
- 本稿把 ℝ 當作討論成員問題的環境有序域；在 OCME 的建構鏈中 ℝ 由 ℚ、ℤ、N 建成，所以這是 N 在 ℝ 中的刻畫，不是 N 的基礎定義。





## 驗證及來源綁定

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


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

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