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

目標與範圍

依 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。

逐步主鏈

N

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

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

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

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

N\subseteq T

3

((0+1)+1)+1

0\in N

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

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

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

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

T_1\ \text{inductive}

T_1\ \text{inductive}

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

-1<0

-1\notin N

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

T_2\ \text{inductive}

T_2\ \text{inductive}

N\subseteq T_2

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

\tfrac{1}{2}\notin N

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

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

\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

局部子步與引理

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

0\in N

x\in N

x+1\in N

x=0

x+1=1\in T_2

x\ge 1

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

逐步反向審查

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