Permutations and combinations: proving P(n,k)=n!/(n−k)! and C(n,k)=n!/(k!(n−k)!) by counting

Goal and scope

Let X be a set of exactly n distinct objects, with natural numbers n, k and 0≤k≤n, and selection without replacement and without repetition. Prove that the number of ordered selections of k objects from X is P(n,k)=n!/(n−k)!, that the number of unordered selections is C(n,k)=n!/(k!(n−k)!), and that both equal 1 when k=0. Finally compute P(5,3)=60 and C(5,3)=10 for X={a,b,c,d,e} and k=3.

Works only inside the MKO's model: distinct objects, no replacement, no repetition, 0≤k≤n, with permutations distinguishing order and combinations ignoring it. Both formulas are proved by counting disjoint unions of finite sets and by induction on k. Repeated selection, indistinguishable objects, circular arrangements and extra restrictions are not treated (the MKO says they need different counting models); the canonical MKO and its English edition are not changed.

Givens and symbols

• finite_counting_basics
• nat_induction
• frac_rules
• numeric_evaluation

• G1 — X is a finite set with exactly n distinct elements; n, k∈ℕ (ℕ contains 0) and 0≤k≤n; selection is without replacement and without repetition (MKO assumption a1).
• G2 — An ordered selection of k objects is a k-tuple (x_i)_{i=1}^{k} of pairwise distinct elements of X; their set is 𝒫_k(X) and P(n,k)=|𝒫_k(X)|. An unordered selection of k objects is a k-element subset of X; their set is 𝒞_k(X) and C(n,k)=|𝒞_k(X)|. For k=0 the empty tuple and the empty set each count as one selection (MKO assumption a2).
• G3 — Example: X={a,b,c,d,e} (five distinct letters), k=3.

• X — a finite set of exactly n distinct objects
• \mathcal{P}_k(X) — the set of k-tuples of pairwise distinct elements of X (ordered selections)
• \mathcal{C}_k(X) — the set of k-element subsets of X (unordered selections)
• P(n,k),\ C(n,k) — the numbers of elements of these two sets
• \operatorname{set}(t) — the set of entries of the tuple t
• t^\frown x — the tuple t followed by one more entry x
• \sigma — the order-forgetting map t↦set(t)
• m! — factorial: 0!=1, (m+1)!=(m+1)·m!

Rules and sources

• finite_counting_basics · prerequisite — Finite counting: for disjoint finite sets A, B, |A∪B|=|A|+|B|; |A×B|=|A|·|B|; there is a bijection between finite sets ⇔ they have the same number of elements.
• nat_induction · prerequisite — Principle of induction: for a family P(n) starting at n₀, if P(n₀) holds and P(n)⇒P(n+1) for every n≥n₀, then P(n) holds for every n≥n₀.
• frac_rules · prerequisite — Fraction rules (all denominators nonzero): a/c+b/c=(a+b)/c; (a/b)(c/d)=(ac)/(bd); (a/b)/(c/d)=(ad)/(bc) (also needing c≠0); a/b=(ak)/(bk) for k≠0.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable.
• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements.
• set_operations_def · prerequisite — Set operations: x∈A∪B ⇔ x∈A or x∈B; x∈A∩B ⇔ x∈A and x∈B; x∈A∖B ⇔ x∈A and x∉B; in a universe U, Aᶜ=U∖A.
• subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈B).
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• injective_surjective_def · prerequisite — Injective: f(a)=f(a′) ⇒ a=a′. Surjective: every b∈B has some a∈A with f(a)=b. Bijective: both; then there is a unique inverse f⁻¹ with f⁻¹∘f=id_A and f∘f⁻¹=id_B.
• eq_congruence · prerequisite — Congruence of equality: if u=v, applying the same defined operation f to both sides gives f(u)=f(v). Operating on one side only is not an instance of this rule.
• eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• imp_intro · prerequisite — →-introduction (discharging a hypothesis): if Q is derived inside a scope that temporarily assumes P, then P⇒Q follows, and P may no longer be used as known.
• function_def · prerequisite — Function: f:A→B assigns to each a∈A exactly one f(a)∈B. Two functions are equal ⇔ they have the same domain and codomain and agree at every a.
• image_preimage_def · prerequisite — Image and preimage: f(S)={f(a) ∣ a∈S}; f⁻¹(T)={a∈A ∣ f(a)∈T}. The preimage notation does not presuppose that f has an inverse.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds.
• mul_inverse_nonzero · prerequisite — Inverse of a nonzero number: in ℚ, ℝ or ℂ, if u≠0 there is 1/u with u·(1/u)=1, and v/u means v·(1/u). 0 has no inverse, so v/0 is undefined.
• mko_perm_comb · cited — For natural numbers n and k with 0≤k≤n, the number of ordered selections without replacement is P(n,k)=n!/(n−k)!, while the number of unordered selections is C(n,k)=n!/(k!(n−k)!). Both values are 1 when k=0. · mko-permutation-combination
• mko_factorial_def · cited — The function F:ℕ→ℕ is uniquely determined recursively by F(0)=1 and F(m+1)=(m+1)F(m); its customary notation is m!. · mko-factorial
• tuple_eq · prerequisite — Finite tuples: two k-tuples are equal exactly when their entries agree in every position; the only 0-tuple is the empty tuple (); for a k-tuple t and an object x, t⌢x is the tuple whose first k entries are those of t and whose entry k+1 is x; every (k+1)-tuple can be written as t⌢x in exactly one way, with t its first k entries and x its last entry.
• disjoint_union_count · prerequisite — If a finite set is the union of finitely many pairwise disjoint finite sets B_j (j∈J, J finite), its number of elements is Σ_{j∈J}|B_j|; in particular, if every |B_j|=c, it is |J|·c. This is the two-set case of finite_counting_basics iterated by induction on the number of sets.
• L_fact_pos · lemma — For every natural number m, m!≥1; in particular m!≠0.
• L_complement_count · lemma — If Y is a finite set and A⊆Y, then |Y∖A|=|Y|−|A|.
• L_same_size_subset · lemma — If A is a finite set, B⊆A and |B|=|A|, then B=A.

Main derivation

\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

Substeps and lemmas

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

Reverse audits

• S15 · premise_audit · G3, S08, S13, numeric_evaluation — This is one instance of the general formulas and can be recomputed independently (N1 to N6, N9, N10); it cannot replace the general proof in S03 to S13.
• S14 · premise_audit · S08, S13, forall_elim, mko_factorial_def — It needs 0!=1 and n!≠0; taking 0! to be 0 would make C(n,0) a division by zero.
• S13 · inverse_equivalence · mul_inverse_nonzero, S02, frac_rules — Multiplying by 1/k! and by k! undo each other, given k!≠0; substituting S08 replaces equals by equals, so the step is two-way.
• S12 · premise_audit · S09, S11, disjoint_union_count, function_def — It needs every fibre to have exactly k! elements; with indistinguishable objects the numbers of orderings could differ and the count would not be a product.
• S11 · premise_audit · S08, S10, forall_elim, mko_factorial_def — Substituting into S08 needs the elements of A to be distinct and |A|=k; what is used is the general result already proved, not a recomputation for one example.
• S10.3 · premise_audit · S05.2, S10.2, L_same_size_subset, set_extensionality — The key point is that set(t) already has |A| elements and so cannot be a proper subset of A; this relies on A being finite.
• S10.2 · premise_audit · S05.1, set_extensionality, set_operations_def — It needs A to be finite; for infinite sets a proper subset can be in bijection with the whole set (for example the even numbers and ℕ), and the lemma fails.
• S10.1 · premise_audit · S09, image_preimage_def — Uses only the definition of set(t); the reverse inclusion is S10.3.
• S10 · premise_audit · S09, set_extensionality, image_preimage_def — Set equality needs both inclusions, which are proved in the sub-steps below; one inclusion alone would not suffice.
• S09 · premise_audit · G2, S05.2, function_def — It needs the image of each t to lie in 𝒞_k(X), which rests on the entries being pairwise distinct. With a repeated entry set(t) would have fewer than k elements and σ would not land in 𝒞_k(X).
• S08 · sufficient_goal_reduction · S03, S07, nat_induction, forall_intro — Goal G: P(n,k)=n!/(n−k)! for 0≤k≤n. Sufficient condition H: Q(0) and Q(k)⇒Q(k+1) for every k; H⇒G by the induction principle. H is proved forwards in S03 and S07; G is never used as a premise.
• S07.2 · inverse_equivalence · frac_rules, S02 — Cancelling and expanding by a common factor undo each other, provided the factor n−k is nonzero; with n−k=0 the cancellation would be invalid.
• S07.1 · inverse_equivalence · mko_factorial_def, eq_replace — Both sides name the same number and may replace each other in either direction; the condition is n−k≥1, since for n−k=0 the factorial (n−k−1)! is undefined.
• S07 · premise_audit · S06, S02, frac_rules — It needs the induction hypothesis, k+1≤n (so that n−k−1 is a natural number) and nonzero denominators (S02); it goes from k to k+1 only.
• S06 · premise_audit · S04, S04.3, S05, disjoint_union_count — It needs disjointness (otherwise elements are counted twice) and equal class sizes (otherwise the sum is not a product); S04.3 and S05 supply them.
• S05.3 · premise_audit · S04.3, S05.2, injective_surjective_def, finite_counting_basics — Both injectivity and surjectivity are needed; either alone would not give equal sizes.
• S05.2 · premise_audit · G2, finite_counting_basics, injective_surjective_def, S05.1 — Pairwise distinctness gives injectivity; with a repeated entry set(t) would have fewer than k elements.
• S05.1 · premise_audit · finite_counting_basics, set_operations_def, eq_congruence — It needs A⊆Y; if A is not a subset of Y, Y=A∪(Y∖A) fails and so does the formula.
• S05 · premise_audit · L_complement_count, G1, finite_counting_basics — It needs the size of E(t) not to depend on t; if the number of later options changed with earlier choices, one could not simply multiply.
• S04.3 · premise_audit · tuple_eq — Uses only the positionwise equality of tuples; the conclusion serves both the disjointness of the classes (S06) and the injectivity in S05.3.
• S04.2 · premise_audit · tuple_eq, set_operations_def, set_extensionality — It needs x∉set(t), which is exactly why E(t) takes x from X∖set(t).
• S04.1 · premise_audit · G2, tuple_eq, set_operations_def — It uses that the entries of u are pairwise distinct; if repetition were allowed, x could lie in set(t) and this inclusion would fail.
• S04 · premise_audit · G2, tuple_eq, set_extensionality — Set equality needs both inclusions, and disjointness needs its own proof; all three are proved in the sub-steps that follow, and one inclusion alone would not suffice.
• S03 · premise_audit · tuple_eq, S02 — It needs the uniqueness of the 0-tuple and n!≠0; it does not depend on the particular elements of X and holds for n=0 as well.
• S02.2 · premise_audit · mko_factorial_def, order_basics, nat_induction — It needs the hypothesis m!≥1 and m≥0; the conclusion goes from m to m+1 only, and no converse is claimed.
• S02.1 · premise_audit · mko_factorial_def — Uses only the first clause of the definition; nothing else is needed.
• S02 · premise_audit · L_fact_pos, mko_factorial_def — Only the recursive definition of factorial and induction are needed; no converse (recovering the recursion from m!≥1) is claimed.
• S01 · premise_audit · G1, G2, def_intro, mko_perm_comb — This step only introduces names and derives no new fact. It relies on the objects being distinct (otherwise pairwise distinctness cannot be judged) and on selection without replacement (no repeated entry); if repetition were allowed, 𝒫_k(X) would be defined differently and the proof below would not apply.

Error controls and negative controls

Decide order, distinctness and replacement first

The common error named in the MKO is to apply a formula before checking the conditions. Choosing 3 from {a,b,c,d,e}: if order matters and there is no repetition (president, vice-president and secretary), use P(5,3)=60; if only who is chosen matters (a three-person committee), use C(5,3)=10; if repetition is allowed (a three-letter code whose letters may repeat), each position has 5 options, giving 5³=125, and neither P nor C applies. Every step here relies on distinctness and no replacement: S04.1 needs x not in t, and S05.2 needs the entries to be pairwise distinct.

Dividing by k! needs exactly k! orderings for every subset

S12 can be written as C(n,k)·k! because every fibre has exactly k! elements (S11), and that rests on the objects being distinct. With indistinguishable objects, for example the letters A, A, B in three positions, there are only three different results, AAB, ABA and BAA, not 3!=6; taking 3! as the count doubles it. Such cases need a different counting model (MKO para2).

0!=1 and the empty selection

For k=0 there is exactly one ordered and one unordered selection: the empty tuple and the empty set (S03, S14). Taking 0! to be 0 would make C(n,0)=n!/(0!·n!) a division by zero; thinking that choosing nothing does not count would wrongly give C(5,0)=0.

• Three-letter codes from {a,b,c,d,e} with repetition allowed number P(5,3)=60 → reject — With repetition each position has 5 options, giving 5³=125; P(5,3) counts only ordered selections with pairwise distinct entries.
• The number of ways to choose a president and a secretary (two different posts) from 5 people is C(5,2)=10 → reject — The posts distinguish order: A as president with B as secretary differs from B as president with A as secretary, so the count is P(5,2)=20=10·2!.
• The letters A, A, B have 3!=6 different arrangements → reject — The objects are not distinct; there are only AAB, ABA and BAA, three arrangements, and this lies outside the MKO's model of distinct objects.
• C(5,0)=0 because nothing is chosen → reject — The empty selection counts as one: 5!/(0!·5!)=1, and 𝒞_0(X)={∅}.

Result and limitations

For selections from n distinct objects with 0≤k≤n, without replacement or repetition: the number of ordered selections is P(n,k)=n!/(n−k)! (choice number i has n−i+1 options, S06 to S08), the number of unordered selections is C(n,k)=n!/(k!(n−k)!) (each k-element subset has exactly k! orderings, S11 to S13), and both equal 1 when k=0. Example: P(5,3)=60 and C(5,3)=10.

• disjoint_union_count is the two-set case of finite_counting_basics extended by induction on the number of sets; this guide takes it as a prerequisite and does not write out that induction.
• N11 and N12 are finite checks for n from 3 to 25 only, used to cross-check how the formulas are written; the general result rests on the proofs in S08 and S13, not on these checks.
• Counting with repetition, with indistinguishable objects or around a circle is outside this guide; the numbers in the negative controls only show that the formulas do not apply.

Verification and source binding

16 declared checks for this guide; only the listed expressions are covered.

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

Same-source full JSON (formulas, ASTs, controls and revision log)