排列與組合：以計數證明 P(n,k)=n!/(n−k)! 與 C(n,k)=n!/(k!(n−k)!)

目標與範圍

設 X 是恰有 n 個相異物件的集合，n、k 為自然數且 0≤k≤n，選取無放回、不重複。證明：從 X 有序選取 k 個的方法數 P(n,k)=n!/(n−k)!，無序選取 k 個的方法數 C(n,k)=n!/(k!(n−k)!)，且 k=0 時兩者都等於 1。最後以 X={a,b,c,d,e}、k=3 算出 P(5,3)=60 與 C(5,3)=10。

只在 MKO 的模型內工作：物件相異、無放回、不重複、0≤k≤n，排列區分順序、組合忽略順序。以有限集合的互斥聯集計數與對 k 的歸納證明兩個公式。不處理重複選取、不可區分物件、環形排列或附加限制（MKO 指出它們需要不同的計數模型）；不改動 canonical MKO 或英文 edition。

已知條件與符號

• finite_counting_basics
• nat_induction
• frac_rules
• numeric_evaluation

• G1 — X 是恰有 n 個相異元素的有限集合；n、k∈ℕ（ℕ 含 0），0≤k≤n；選取無放回且不可重複（MKO 假設 a1）。
• G2 — 有序選取 k 個是 X 中兩兩相異元素的 k 元組 (x_i)_{i=1}^{k}，所成集合記為 𝒫_k(X)，P(n,k)=|𝒫_k(X)|；無序選取 k 個是 X 的 k 元子集合，所成集合記為 𝒞_k(X)，C(n,k)=|𝒞_k(X)|。k=0 時空元組與空集合各計為一種選取（MKO 假設 a2）。
• G3 — 例子：X={a,b,c,d,e}（五個相異字母），k=3。

• X — 恰有 n 個相異物件的有限集合
• \mathcal{P}_k(X) — X 中 k 個兩兩相異元素的 k 元組（有序選取）所成的集合
• \mathcal{C}_k(X) — X 的 k 元子集合（無序選取）所成的集合
• P(n,k),\ C(n,k) — 上述兩個集合的元素個數
• \operatorname{set}(t) — 元組 t 的各項所成的集合
• t^\frown x — 在元組 t 後面接上一項 x
• \sigma — 忘記順序的映射 t↦set(t)
• m! — 階乘：0!=1，(m+1)!=(m+1)·m!

規則與來源

• finite_counting_basics · prerequisite — 有限計數：互斥有限集合 A、B 有 |A∪B|=|A|+|B|；|A×B|=|A|·|B|；有限集之間存在雙射 ⇔ 元素個數相同。
• nat_induction · prerequisite — 數學歸納原理：對從 n₀ 起的命題族 P(n)，若 P(n₀) 成立，且對每個 n≥n₀ 都有 P(n)⇒P(n+1)，則所有 n≥n₀ 都有 P(n)。
• frac_rules · prerequisite — 分數運算（分母皆非零）：a/c+b/c=(a+b)/c；(a/b)(c/d)=(ac)/(bd)；(a/b)/(c/d)=(ad)/(bc)（另需 c≠0）；a/b=(ak)/(bk)（k≠0）。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
• 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。
• set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
• 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。
• subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• injective_surjective_def · prerequisite — 單射：f(a)=f(a′) ⇒ a=a′。滿射：每個 b∈B 都有 a∈A 使 f(a)=b。雙射：既單又滿，此時有唯一反函數 f⁻¹ 使 f⁻¹∘f=id_A、f∘f⁻¹=id_B。
• eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
• eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
• forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
• imp_intro · prerequisite — →引入（釋放假設）：若在暫時假設 P 的作用域中推出 Q，則得到 P⇒Q；此後 P 不再可當作已知使用。
• function_def · prerequisite — 函數：f:A→B 對每個 a∈A 指定恰好一個 f(a)∈B。兩函數相等 ⇔ 定義域、對應域相同且對每個 a 都有相同值。
• image_preimage_def · prerequisite — 像與原像：f(S)={f(a) ∣ a∈S}；f⁻¹(T)={a∈A ∣ f(a)∈T}。原像記號不預設 f 有反函數。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
• mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
• mko_perm_comb · cited — 對自然數 n、k 且 0≤k≤n，由 n 個相異物件無放回選取 k 個的排列數為 P(n,k)=n!/(n−k)!，組合數為 C(n,k)=n!/(k!(n−k)!)；k=0 時兩者均為 1。 · mko-permutation-combination
• mko_factorial_def · cited — 函數 F:ℕ→ℕ 由 F(0)=1 與 F(m+1)=(m+1)F(m) 唯一遞迴決定；慣用記號為 m!。 · mko-factorial
• tuple_eq · prerequisite — 有限元組：兩個 k 元組相等當且僅當每個位置的項都相等；0 元組只有空元組 ()；對 k 元組 t 與物件 x，t⌢x 是前 k 項為 t、第 k+1 項為 x 的元組；每個 (k+1) 元組恰可唯一寫成 t⌢x，其中 t 是它的前 k 項、x 是它的最後一項。
• disjoint_union_count · prerequisite — 若有限集合是有限多個兩兩互斥的有限集合 B_j（j∈J，J 有限）的聯集，則其元素個數是 Σ_{j∈J}|B_j|；特別地，若每個 |B_j|=c，則為 |J|·c。這是 finite_counting_basics 的兩集合情形對集合個數歸納所得。
• L_fact_pos · lemma — 對每個自然數 m，m!≥1；特別地 m!≠0。
• L_complement_count · lemma — 若 Y 是有限集合且 A⊆Y，則 |Y∖A|=|Y|−|A|。
• L_same_size_subset · lemma — 若 A 是有限集合、B⊆A 且 |B|=|A|，則 B=A。

逐步主鏈

\text{ordered and unordered selections of }k\text{ objects from }X

P(n,k)=|\mathcal{P}_k(X)|,\quad C(n,k)=|\mathcal{C}_k(X)|

m!\ (m\in\mathbb{N})

m!\geq 1,\ \text{hence}\ m!\neq 0

\mathcal{P}_0(X)

\mathcal{P}_0(X)=\{()\},\quad |\mathcal{P}_0(X)|=1=\frac{n!}{(n-0)!}

\mathcal{P}_{k+1}(X)\quad(k+1\le n)

\mathcal{P}_{k+1}(X)=\bigcup_{t\in\mathcal{P}_k(X)}E(t),\quad E(t)=\{t^\frown x\mid x\in X\setminus\operatorname{set}(t)\},\ \text{pairwise disjoint}

E(t)\quad(t\in\mathcal{P}_k(X))

|E(t)|=n-k\geq 1

\mathcal{P}_{k+1}(X)=\bigcup_{t\in\mathcal{P}_k(X)}E(t)

|\mathcal{P}_{k+1}(X)|=|\mathcal{P}_k(X)|\cdot(n-k)

|\mathcal{P}_k(X)|=\frac{n!}{(n-k)!}

|\mathcal{P}_{k+1}(X)|=\frac{n!}{(n-(k+1))!}

Q(k):\ k\le n\Rightarrow|\mathcal{P}_k(X)|=\frac{n!}{(n-k)!}

P(n,k)=\frac{n!}{(n-k)!}\quad\text{for all}\ 0\le k\le n

t\in\mathcal{P}_k(X)

\sigma(t)=\operatorname{set}(t)\in\mathcal{C}_k(X)

\sigma^{-1}(\{A\})\quad(A\in\mathcal{C}_k(X))

\sigma^{-1}(\{A\})=\mathcal{P}_k(A)

|\sigma^{-1}(\{A\})|=|\mathcal{P}_k(A)|

|\sigma^{-1}(\{A\})|=\frac{k!}{(k-k)!}=\frac{k!}{0!}=k!

\mathcal{P}_k(X)=\bigcup_{A\in\mathcal{C}_k(X)}\sigma^{-1}(\{A\})

P(n,k)=C(n,k)\cdot k!

P(n,k)=C(n,k)\cdot k!

C(n,k)=\frac{P(n,k)}{k!}=\frac{n!}{k!\,(n-k)!}

k=0

P(n,0)=\frac{n!}{n!}=1,\quad C(n,0)=\frac{n!}{0!\,n!}=1,\quad \mathcal{C}_0(X)=\{\varnothing\}

n=5,\ k=3

P(5,3)=60,\quad C(5,3)=10,\quad 10\cdot 3!=60

局部子步與引理

0!

0!=1\geq 1

m!\geq 1

(m+1)!=(m+1)\,m!\geq m!\geq 1

u\in\mathcal{P}_{k+1}(X)

u=t^\frown x,\ t\in\mathcal{P}_k(X),\ x\in X\setminus\operatorname{set}(t)

t\in\mathcal{P}_k(X),\ x\in X\setminus\operatorname{set}(t)

t^\frown x\in\mathcal{P}_{k+1}(X)

t^\frown x=s^\frown y

t=s\ \land\ x=y

A\subseteq Y,\ Y\ \text{finite}

|Y\setminus A|=|Y|-|A|

t=(x_i)_{i=1}^{k}\in\mathcal{P}_k(X)

|\operatorname{set}(t)|=k,\quad |X\setminus\operatorname{set}(t)|=n-k

x\mapsto t^\frown x:\ X\setminus\operatorname{set}(t)\to E(t)

|E(t)|=|X\setminus\operatorname{set}(t)|=n-k

(n-k)!

(n-k)\cdot(n-k-1)!

\frac{n!\,(n-k)}{(n-k)\cdot(n-k-1)!}

\frac{n!}{(n-k-1)!}=\frac{n!}{(n-(k+1))!}

t\in\mathcal{P}_k(X),\ \sigma(t)=A

t\in\mathcal{P}_k(A)

B\subseteq A,\ |B|=|A|,\ A\ \text{finite}

B=A

t\in\mathcal{P}_k(A)

t\in\mathcal{P}_k(X)\ \land\ \sigma(t)=A

逐步反向審查

• S15 · premise_audit · G3, S08, S13, numeric_evaluation — 這是一般公式的一個實例，可獨立重算（N1 至 N6、N9、N10）；它不能取代 S03 到 S13 的一般證明。
• S14 · premise_audit · S08, S13, forall_elim, mko_factorial_def — 需要 0!=1 與 n!≠0；若誤把 0! 當 0，C(n,0) 會變成除以零。
• S13 · inverse_equivalence · mul_inverse_nonzero, S02, frac_rules — 乘 1/k! 與乘 k! 互為反運算，前提 k!≠0；代入 S08 是等值代換，雙向成立。
• S12 · premise_audit · S09, S11, disjoint_union_count, function_def — 需要每個纖維大小都是 k!；若物件不可區分，不同選取的排序數可能不同，就不能寫成乘積。
• S11 · premise_audit · S08, S10, forall_elim, mko_factorial_def — 代入 S08 需要 A 的元素相異且 |A|=k；所用的是已證的一般結論，不是對某個例子的再計算。
• S10.3 · premise_audit · S05.2, S10.2, L_same_size_subset, set_extensionality — 關鍵是 set(t) 已有 |A| 個元素，因此不可能是 A 的真子集合；這依賴 A 有限。
• S10.2 · premise_audit · S05.1, set_extensionality, set_operations_def — 需要 A 有限；對無限集合，真子集合可以與原集合之間有雙射（例如偶數與 ℕ），這個引理就不成立。
• S10.1 · premise_audit · S09, image_preimage_def — 只用 set(t) 的定義；反向包含在 S10.3。
• S10 · premise_audit · S09, set_extensionality, image_preimage_def — 集合相等需要兩個方向的包含，在下列子步中逐一證明；只證一個方向不夠。
• S09 · premise_audit · G2, S05.2, function_def — 需要每個 t 的像確實在 𝒞_k(X) 中，這依賴各項兩兩相異。若有重複項，set(t) 的元素少於 k 個，σ 就不落在 𝒞_k(X)。
• S08 · sufficient_goal_reduction · S03, S07, nat_induction, forall_intro — 目標 G：0≤k≤n 時 P(n,k)=n!/(n−k)!。足夠條件 H：Q(0) 且對每個 k 有 Q(k)⇒Q(k+1)；H⇒G 由歸納原理。H 由 S03 與 S07 正向證成，沒有把 G 當作前提。
• S07.2 · inverse_equivalence · frac_rules, S02 — 約分與擴分互為反運算，前提是公因子 n−k 非零；若 n−k=0，約分不合法。
• S07.1 · inverse_equivalence · mko_factorial_def, eq_replace — 兩邊是同一個數的兩種寫法，可以雙向代換；條件是 n−k≥1，若 n−k=0，(n−k−1)! 沒有定義。
• S07 · premise_audit · S06, S02, frac_rules — 需要歸納假設、k+1≤n（使 n−k−1 是自然數）與分母非零（S02）；本步只由 k 推到 k+1。
• S06 · premise_audit · S04, S04.3, S05, disjoint_union_count — 需要互斥（否則重複計數）與每類大小相同（否則和不能寫成乘積）；兩者分別由 S04.3 與 S05 提供。
• S05.3 · premise_audit · S04.3, S05.2, injective_surjective_def, finite_counting_basics — 單射與滿射兩者都需要；只有其一不足以推出元素個數相等。
• S05.2 · premise_audit · G2, finite_counting_basics, injective_surjective_def, S05.1 — 「兩兩相異」保證單射；若有重複項，set(t) 會少於 k 個元素。
• S05.1 · premise_audit · finite_counting_basics, set_operations_def, eq_congruence — 需要 A⊆Y；若 A 不是 Y 的子集合，Y=A∪(Y∖A) 不成立，公式也會錯。
• S05 · premise_audit · L_complement_count, G1, finite_counting_basics — 需要 E(t) 的大小不依賴 t；若後續可選數隨前面的選擇改變，就不能直接相乘。
• S04.3 · premise_audit · tuple_eq — 只用元組相等的逐位條件；結論同時用於各類互斥（S06）與 S05.3 的單射。
• S04.2 · premise_audit · tuple_eq, set_operations_def, set_extensionality — 需要 x∉set(t)；這正是 E(t) 的定義要求 x 取自 X∖set(t) 的原因。
• S04.1 · premise_audit · G2, tuple_eq, set_operations_def — 用到 u 的各項兩兩相異；若允許重複，x 可能落在 set(t) 中，這個包含就不成立。
• S04 · premise_audit · G2, tuple_eq, set_extensionality — 集合相等需要兩個方向的包含，互斥另需證明；三者都在後面的子步中證成，只證一個方向不夠。
• S03 · premise_audit · tuple_eq, S02 — 需要「0 元組唯一」與 n!≠0；本步不依賴 X 的具體元素，n=0 時也成立。
• S02.2 · premise_audit · mko_factorial_def, order_basics, nat_induction — 需要歸納假設 m!≥1 與 m≥0；結論只由 m 推到 m+1，不宣稱反向。
• S02.1 · premise_audit · mko_factorial_def — 只用定義的第一條，不需其他前提。
• S02 · premise_audit · L_fact_pos, mko_factorial_def — 只需階乘的遞迴定義與歸納法；不宣稱反向（由 m!≥1 推回遞迴式）。
• S01 · premise_audit · G1, G2, def_intro, mko_perm_comb — 此步只命名，不推出新事實。它依賴物件相異（否則「兩兩相異」無從判定）與無放回（元組中不重複）；若改為可重複選取，𝒫_k(X) 的定義就不同，後面的證明也不適用。

錯誤控制與反例

先判斷順序、相異與放回

MKO 指出的常見誤解是不先判斷條件就套公式。從 {a,b,c,d,e} 選 3 個：若區分順序且不可重複（例如分別選會長、副會長、秘書），用 P(5,3)=60；若只看選了誰（三人小組），用 C(5,3)=10；若可重複（三位字母密碼，字母可重複使用），每位都有 5 種，共 5³=125，P 與 C 都不適用。本稿每一步都依賴「相異」與「無放回」：S04.1 需要 x 不在 t 中，S05.2 需要各項兩兩相異。

除以 k! 需要每個子集合恰有 k! 種排序

S12 能寫成 C(n,k)·k! 是因為每個纖維的大小都是 k!（S11），而這依賴物件相異。若物件不可區分，例如字母 A、A、B 排成三個位置，不同的結果只有 AAB、ABA、BAA 三種，不是 3!=6；把 3! 當成排列數就多算了一倍。這類情況需要另外的計數模型（MKO para2）。

0!=1 與空選取

k=0 時有序與無序選取都只有一種：空元組與空集合（S03、S14）。若把 0! 誤當 0，C(n,0)=n!/(0!·n!) 會變成除以零；若認為「什麼都不選不算一種」，C(5,0) 會被誤算成 0。

• 從 {a,b,c,d,e} 中可重複地組成三位字母密碼，共有 P(5,3)=60 種 → reject — 可重複時每位都有 5 種，共 5³=125；P(5,3) 只計各項兩兩相異的有序選取。
• 從 5 人中選出會長與秘書（兩個不同職位）的方法數是 C(5,2)=10 → reject — 職位區分順序：甲任會長、乙任秘書與乙任會長、甲任秘書不同，應為 P(5,2)=20=10·2!。
• 字母 A、A、B 的不同排列共有 3!=6 種 → reject — 物件不相異，實際只有 AAB、ABA、BAA 三種；這超出本 MKO 的相異物件模型。
• C(5,0)=0，因為什麼都沒有選 → reject — 空選取計為一種：5!/(0!·5!)=1，且 𝒞_0(X)={∅}。

結論與限制

對 n 個相異物件、0≤k≤n、無放回不重複的選取：有序選取數 P(n,k)=n!/(n−k)!（第 i 次可選 n−i+1 個，S06 至 S08），無序選取數 C(n,k)=n!/(k!(n−k)!)（每個 k 元子集合恰有 k! 種排序，S11 至 S13），k=0 時兩者都是 1。例：P(5,3)=60，C(5,3)=10。

• disjoint_union_count 是 finite_counting_basics 兩集合情形對集合個數的歸納推廣，本稿把它當作前置規則，沒有寫出該歸納。
• N11、N12 只是 n 從 3 到 25 的有限點核對，用來交叉檢查公式的寫法；一般結論依賴 S08 與 S13 的證明，不依賴這些核對。
• 可重複選取、不可區分物件與環形排列的計數不在本稿範圍；負面對照中的數字只用來說明公式不適用。

驗證及來源綁定

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 87cb2ae2d23efddad0cb4a3c6cf56e3e9661d77e4fa32202b282969bac1604f2
• original source SHA-256: 87cb2ae2d23efddad0cb4a3c6cf56e3e9661d77e4fa32202b282969bac1604f2
• Lean: NOT_RUN · independent AI: NOT_MEASURED

同源完整 JSON（含公式、AST、反控制與修訂記錄）