# 自然數

自然數是用於計數與離散次序的基本數；本條目採用包含 0 的慣例。

mko-natural-number · concept · v0.10.0



## 數學敘述

在本條目的慣例中，自然數集合 N 包含 0，並包含 0 經有限次後繼所得的 1、2、3 等數。





## 代表公式（精確 TeX）

n\in N





## 成立條件


- 本條目的符號 N 明定包含 0。
- n 表示任意一個待判定是否屬於 N 的數。





## 符號作用域


- n — 自然數候選
- N — 自然數集合
- ∈ — 隸屬關係





## 直觀、定義與常見誤解

自然數提供計數與排列離散次序的基本語言。0 表示沒有對象的數量；從任一自然數取後繼，可得到下一個自然數。

不同數學傳統對 0 是否屬於自然數有不同慣例。為了和 Lean 的 Nat 及本庫後續物件一致，本條目固定採 N 包含 0；閱讀外部資料時仍應先確認該資料的定義。

自然數本身與書寫它的數字符號不同。例如十進位符號 2、二進位符號 10 可以表示同一個自然數。

常見誤解是以為所有教材對自然數是否包含 0 都有相同約定，或把數字的書寫方式與數本身混為一談。





## 已採用的推導導讀

[自然數：以最小歸納集判定成員，並分辨數與數字符號](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-natural-number-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識







## 驗證界線

本條目是概念候選稿；研究來源不是 OCME Evidence，尚未建立計算檢查或 Lean 形式證明。

not_formalized

這不表示內容錯誤；只表示尚未登錄可重播的計算或形式證據。





## 下一個義務

建立 OCME 的 N、0 與後繼到 Lean Nat 的明確語義橋，驗證後再產生內容位址化 Evidence。





## 同源結構化資料

本頁與互動版共用同一個物件與既有語言 edition；未新增證明或人工審定。

[原始 MKO JSON](https://ocme.evemisslab.com/data/mko/natural-number.json) · [純文字 Markdown](https://ocme.evemisslab.com/zh-Hant/mko/mko-natural-number/index.md)