# 階乘：遞迴定義的唯一性、乘積形式與 5! 的計算 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-factorial/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-factorial-01 · production-20261019-adopted-96 ## 目標與範圍 只用 F(0)=1 與 F(n+1)=(n+1)F(n)（n∈ℕ，ℕ 含 0）：(1) 證明滿足這兩條的函數 ℕ→ℕ 只有一個；(2) 證明對所有 n 有 F(n)=∏_{k=1}^{n} k（空乘積為 1），所以 n>0 時 n! 是從 1 到 n 所有整數的乘積；(3) 證明每個 F(n)≥1，特別是 0!=1≠0；(4) 由遞迴逐步算出 5!=120。 在 MKO 的範圍內：自然數含 0（假設 a1），以遞迴定義的函數 F。F 的存在取自 MKO 的陳述（遞迴定理不在本稿證明）；本稿證明唯一性、乘積形式與正性。不證明「n! 計數 n 元集合的排列」（MKO 指出那是另需證明的定理）；不改動 canonical MKO 或英文 edition。 ## 已知條件與符號 - nat_induction - function_def - eq_replace - mul_comm - order_basics - numeric_evaluation - G1 — ℕ 包含 0；n 是自然數（MKO 假設 a1）。 - G2 — F:ℕ→ℕ 滿足 F(0)=1，且對每個 n∈ℕ 有 F(n+1)=(n+1)F(n)；記 n!=F(n)。這樣的 F 存在，取自 MKO 的陳述。 - F,\ n! — 階乘函數及其記號 n!=F(n) - G — 任一滿足同樣兩條等式的函數 - \mathbb{N} — 含 0 的自然數 - \prod_{k=1}^{n} k — 1 到 n 的整數乘積，n=0 時為 1 - P(n) — 乘積 ∏_{k=1}^{n} k 作為 n 的函數 ## 規則與來源 - nat_induction · prerequisite — 數學歸納原理：對從 n₀ 起的命題族 P(n)，若 P(n₀) 成立，且對每個 n≥n₀ 都有 P(n)⇒P(n+1)，則所有 n≥n₀ 都有 P(n)。 - function_def · prerequisite — 函數：f:A→B 對每個 a∈A 指定恰好一個 f(a)∈B。兩函數相等 ⇔ 定義域、對應域相同且對每個 a 都有相同值。 - eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。 - mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。 - order_basics · prerequisite — 實數的序：任兩數恰有 uv 之一；u0 推出 uwvw。 - numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。 - def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。 - def_intro · 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) 成立。 - forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。 - mul_one · prerequisite — 乘法單位元：1·u=u。 - and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。 - mko_factorial_def · cited — 函數 F:ℕ→ℕ 由 F(0)=1 與 F(n+1)=(n+1)F(n) 唯一遞迴決定；慣用記號為 n!。 · mko-factorial - prod_def · prerequisite — 有限乘積：∏_{k=1}^{0} a_k=1（空乘積），且 ∏_{k=1}^{n+1} a_k=(∏_{k=1}^{n} a_k)·a_{n+1}。 - nat_closure · prerequisite — 自然數的和與積仍是自然數；對每個 n∈ℕ 有 n+1≥1>0。 - L_pos · lemma — 對每個 n∈ℕ，F(n)≥1。 ## 逐步主鏈 S01 · definition操作前 n! 操作後 F(0)=1,\ \ F(n+1)=(n+1)F(n)\ \ (n\in\mathbb{N}) 條件：0\in\mathbb{N} 規則：mko_factorial_def · 依賴：G1, G2, mko_factorial_def 葉節點依據：mko_factorial_def + def_unfold 依 MKO，n! 就是 F(n)，而 F 只由兩條等式決定：起點 F(0)=1，以及「下一個值 = 新的因數 n+1 乘上前一個值」。本稿之後只使用這兩條等式，不使用任何事先記住的公式。 S02 · definition操作前 G:\mathbb{N}\to\mathbb{N},\ G(0)=1,\ G(n+1)=(n+1)G(n) 操作後 Q(n):\ G(n)=F(n) 條件：無 規則：def_intro · 依賴：S01 葉節點依據：def_intro 為了證明唯一性，任取一個函數 G:ℕ→ℕ，只假設它滿足同樣的兩條等式。對每個 n，把「G(n)=F(n)」這個命題取名為 Q(n)，目標是證明所有 n 都有 Q(n)。 S03 · induction_base操作前 G(0),\ F(0) 操作後 G(0)=1=F(0) 條件：無 規則：eq_refl_symm_trans · 依賴：S01, S02 葉節點依據：eq_refl_symm_trans 歸納基礎：G(0)=1（G 的假設），F(0)=1（定義），依等號的對稱與傳遞得 G(0)=F(0)，即 Q(0)。 S04 · induction_step操作前 G(n)=F(n) 操作後 G(n+1)=F(n+1) 條件：n\in\mathbb{N}\ \text{arbitrary} 規則：eq_replace · 依賴：S01, S02 葉節點依據：eq_replace + eq_refl_symm_trans + forall_elim 設某個 n 有 G(n)=F(n)。則 G(n+1)=(n+1)G(n)（G 的遞迴）=(n+1)F(n)（以歸納假設作等值代換）=F(n+1)（F 的遞迴）。所以 Q(n)⇒Q(n+1)。 S05 · implies操作前 Q(0),\ \ Q(n)\Rightarrow Q(n+1) 操作後 G=F\ \text{for every such}\ G 條件：n_0=0 規則：nat_induction · 依賴：S03, S04, nat_induction, function_def 葉節點依據：nat_induction + function_def + forall_intro 依歸納原理（n₀=0），所有 n∈ℕ 都有 G(n)=F(n)。G 與 F 定義域都是 ℕ、對應域都是 ℕ，且每點的值相同，依 function_def 得 G=F。因 G 是任意取的，依全稱推廣：滿足這兩條等式的函數至多一個。這就是 MKO 中「唯一」的內容。 S06 · definition操作前 P(n)=\prod_{k=1}^{n} k 操作後 P:\mathbb{N}\to\mathbb{N} 條件：無 規則：prod_def · 依賴：prod_def, nat_closure 葉節點依據：prod_def + nat_closure + nat_induction 取 a_k=k，令 P(n)=∏_{k=1}^{n} k。P(n) 是自然數：P(0)=1∈ℕ，且若 P(n)∈ℕ，則 P(n+1)=P(n)·(n+1)∈ℕ（nat_closure），依歸納原理對所有 n 成立。所以 P 是 ℕ→ℕ 的函數。 S07 · equivalent操作前 P(0)=\prod_{k=1}^{0} k 操作後 P(0)=1 條件：無 規則：prod_def · 依賴：S06 葉節點依據：prod_def + def_unfold 沒有任何因數的乘積是 1（空乘積），這是 prod_def 的第一條；所以 P 的起始值與 F(0)=1 相同。 S08 · equivalent操作前 P(n+1)=P(n)\cdot(n+1) 操作後 P(n+1)=(n+1)P(n) 條件：無 規則：mul_comm · 依賴：S06 葉節點依據：prod_def + mul_comm prod_def 的第二條給出 P(n+1)=P(n)·(n+1)；依乘法交換律改寫成 (n+1)P(n)，與 F 的遞迴形式完全相同。 S09 · theorem_application操作前 P(0)=1,\ \ P(n+1)=(n+1)P(n) 操作後 F(n)=\prod_{k=1}^{n} k\ \text{for every}\ n\in\mathbb{N} 條件：P:\mathbb{N}\to\mathbb{N} 規則：forall_elim · 依賴：S05, S06, S07, S08 葉節點依據：forall_elim + function_def + def_unfold P 是 ℕ→ℕ 的函數（S06），且滿足 F 的兩條等式（S07、S08）。S05 對每個這樣的函數成立，取 G=P 得 P=F，即 n!=∏_{k=1}^{n} k。n>0 時，這是從 1 到 n 所有整數的乘積，例如 5!=1·2·3·4·5。 S10 · theorem_application操作前 F(n) 操作後 F(n)\geq 1\ \text{for every}\ n\in\mathbb{N};\ \text{in particular}\ 0!=1\neq 0 條件：無 規則：L_pos · 依賴：S01, L_pos 葉節點依據：nat_induction + order_basics 依引理 L_pos，每個階乘至少是 1，所以沒有任何 n! 等於 0；特別是 0!=1。引理在子步 S10.1、S10.2 以歸納法證明。 S11 · implies操作前 F(0)=1 操作後 F(1)=1,\ F(2)=2,\ F(3)=6 條件：無 規則：forall_elim · 依賴：S01 葉節點依據：forall_elim + eq_replace + numeric_evaluation 依遞迴逐步代入：n=0 得 F(1)=1·F(0)=1；n=1 得 F(2)=2·F(1)=2；n=2 得 F(3)=3·F(2)=6。每一步乘上的是新因數 n+1，不是 n。 S12 · implies操作前 F(3)=6 操作後 F(4)=24,\ F(5)=120 條件：無 規則：forall_elim · 依賴：S01, S11 葉節點依據：forall_elim + eq_replace + numeric_evaluation 繼續代入：n=3 得 F(4)=4·F(3)=4·6=24；n=4 得 F(5)=5·F(4)=5·24=120。所以 5!=120。 S13 · implies操作前 \prod_{k=1}^{5} k 操作後 1\cdot 2\cdot 3\cdot 4\cdot 5=120=F(5) 條件：無 規則：prod_def · 依賴：S09, S12 葉節點依據：prod_def + numeric_evaluation 交叉核對：依 prod_def 展開 ∏_{k=1}^{5} k=1·2·3·4·5=120，與 S12 由遞迴得到的 F(5)=120 一致，符合 S09。 S14 · implies操作前 S05,\ S09,\ S10,\ S12 操作後 \text{goals (1) to (4) established} 條件：無 規則：and_intro_elim · 依賴：S05, S09, S10, S12 葉節點依據：and_intro_elim 四個目標分別由 S05（唯一性）、S09（乘積形式）、S10（F(n)≥1，0!=1）與 S12（5!=120）證成。 ## 局部子步與引理 S10.1 · induction_base操作前 F(0)=1 操作後 F(0)\geq 1 條件：無 規則：order_basics · 依賴：S01 葉節點依據：order_basics + def_unfold F(0)=1，而 1≥1（相等情形），所以基礎成立。 S10.2 · induction_step操作前 F(n)\geq 1 操作後 F(n+1)=(n+1)F(n)\geq 1 條件：n+1>0 規則：order_basics · 依賴：S01, nat_closure, order_basics 葉節點依據：order_basics + nat_closure + mul_one 設 F(n)≥1。因 n+1>0，兩邊同乘 n+1 保持方向：(n+1)F(n)≥(n+1)·1=n+1；又 n+1≥1，依傳遞得 F(n+1)=(n+1)F(n)≥1。S10.1 與 S10.2 依歸納原理證得引理 L_pos。 ## 逐步反向審查 - S14 · sufficient_goal_reduction · S05, S09, S10, S12, and_intro_elim — 目標 G：(1) 到 (4) 同時成立。足夠條件 H：S05、S09、S10、S12 各自成立；H⇒G 由合取引入。H 由定義與歸納正向證成，沒有把 G 當作前提。 - S13 · premise_audit · S09, S12, prod_def — 這只是 n=5 的一致性核對；S09 的一般結論來自唯一性，不來自這個例子。 - S12 · premise_audit · S11, forall_elim, numeric_evaluation — 精確整數乘法（N4、N5），沒有使用浮點近似。 - S11 · premise_audit · S01, forall_elim, numeric_evaluation — 每個值都依賴前一個值，必須按順序計算；乘法可獨立重算（N1 到 N3）。 - S10.2 · premise_audit · nat_closure, order_basics, nat_induction — 乘以 n+1 保持不等號方向需要 n+1>0；若乘的是可能為 0 的數（例如錯誤遞迴 n·F(n) 在 n=0），結論就會失敗。 - S10.1 · premise_audit · S01, order_basics — 只用到定義的起始值。 - S10 · premise_audit · L_pos — 結論只宣稱 F(n)≥1，不宣稱更強的下界。 - S09 · premise_audit · S05, S06, S07, S08, forall_elim — 套用唯一性需要 P 滿足同樣的起始值與同樣的遞迴，兩者分別由 S07、S08 提供。不是靠核對幾個 n 得到的。 - S08 · inverse_equivalence · mul_comm — 交換律是恆等式，兩種寫法表示同一個數，雙向成立。 - S07 · inverse_equivalence · prod_def — 兩邊依定義是同一個數，等式雙向成立。 - S06 · premise_audit · prod_def, nat_closure, nat_induction — 要套用 S05，P 必須是 ℕ→ℕ 的函數；這一步確認了對應域。 - S05 · premise_audit · S03, S04, nat_induction, function_def, forall_intro — 需要基礎 S03 與歸納步 S04 兩者；只檢查前幾個 n 不能代替歸納步。此步只證唯一性，存在性來自 MKO。 - S04 · premise_audit · S01, S02, eq_replace — 只用到同一個 n 的歸納假設與兩條遞迴；n 是任意的，沒有加條件。不宣稱反向（由 Q(n+1) 推回 Q(n)）。 - S03 · premise_audit · S01, S02, eq_refl_symm_trans — 需要兩個函數的起始值相同；若 G(0)=0，基礎就不成立（見錯誤控制一）。 - S02 · premise_audit · S01, def_intro — 對 G 不加任何其他假設，這是 S05 能對所有這樣的 G 下結論（全稱推廣）的前提。 - S01 · premise_audit · G1, G2, mko_factorial_def — 此步只寫出定義，不推出新事實。F 的存在是 MKO 提供的前提；唯一性在 S02 到 S05 證明。 ## 錯誤控制與反例 0! 是 1，不是 0MKO 指出常見誤解是把 0! 當成 0。F(0)=1 是定義的一部分。若把起點改成 H(0)=0 而保留 H(n+1)=(n+1)H(n)，則依歸納每個 H(n) 都是 0（H(n+1)=(n+1)·0=0），整個函數塌成 0，5! 會變成 0 而不是 120。空乘積為 1 的慣例（S07）也與 F(0)=1 一致。 n! 不是「n 倍」MKO 指出另一個誤解是把 n! 當成 n 倍。遞迴每一步都乘上新的因數 n+1，所以 n! 累積了從 1 到 n 的所有因數：3!=6 不是 3，5!=120 不是 5，也不是 5·5=25。另一個常見的差一錯誤是寫成 H(n+1)=n·H(n)：此時 H(1)=0·H(0)=0，之後全為 0。 用精確整數，不用浮點近似MKO 提醒不可用超出安全範圍的浮點值冒充精確結果。23!=25852016738884976640000=2¹⁹·49308808782358125，其奇數部分大於 2⁵³=9007199254740992。IEEE 754 binary64 的有效數具有 53 位元精度，一個正整數（在指數範圍內）可精確表示當且僅當它的奇數部分小於 2⁵³，所以 binary64 無法精確表示 23!。本稿的計算全部用精確整數乘法。 - 0!=0 → reject — 定義給出 F(0)=1；且 S10 證明每個 F(n)≥1。 - 把遞迴寫成 H(n+1)=n·H(n)、H(0)=1，定義的是同一個階乘 → reject — H(1)=0·1=0，但 F(1)=1。 - 對 n=0 到 5 核對 F(n)=∏_{k=1}^{n} k 成立，就證明了所有 n 都成立 → reject — 有限檢查只涵蓋那些 n；一般結論來自 S05 的唯一性（歸納法）。 - 以 binary64 浮點計算得到的 23! 就是精確值 → reject — 23! 的奇數部分大於 2⁵³，binary64 無法精確表示。 ## 結論與限制 由 F(0)=1 與 F(n+1)=(n+1)F(n) 決定的函數只有一個；它等於乘積 ∏_{k=1}^{n} k（n=0 時為空乘積 1），每個值都至少為 1，所以 0!=1 而不是 0；逐步代入得 1!=1、2!=2、3!=6、4!=24、5!=120。 - F 的存在（遞迴定理）取自 MKO 的陳述，本稿未證明；本稿證明的是唯一性與由此推出的性質。 - N8、N9 是以 Python 標準函式 factorial 對 n=0 到 30 的有限核對，只支持這些 n，論證不依賴它們。 - 錯誤控制三關於 binary64 的敘述依據 IEEE 754 binary64 格式有 53 位元有效數精度這一事實，本稿未核對標準原文。 ## 驗證及來源綁定 15 個本稿宣告算術檢查；只支持所列算式。 - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: 20f46251e6543f0cb88df555a6522f263111c7e35fd4a025a2b6b776eb0bc6c5 - original source SHA-256: 20f46251e6543f0cb88df555a6522f263111c7e35fd4a025a2b6b776eb0bc6c5 - Lean: NOT_RUN · independent AI: NOT_MEASURED [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-factorial-01.json)