Factorial: uniqueness of the recursive definition, the product form and computing 5!

Goal and scope

Using only F(0)=1 and F(n+1)=(n+1)F(n) (n∈ℕ, with 0∈ℕ): (1) prove that at most one function ℕ→ℕ satisfies these two equations; (2) prove F(n)=∏_{k=1}^{n} k for every n (the empty product being 1), so that for n>0, n! is the product of all integers from 1 to n; (3) prove F(n)≥1 for every n, in particular 0!=1≠0; (4) compute 5!=120 step by step from the recursion.

Inside the MKO's scope: natural numbers including 0 (assumption a1) and the recursively defined function F. Existence of F is taken from the MKO statement (the recursion theorem is not proved here); this guide proves uniqueness, the product form and positivity. It does not prove that n! counts the permutations of an n-element set (the MKO says that is a separate theorem), and it does not change the canonical MKO or its English edition.

Givens and symbols

• nat_induction
• function_def
• eq_replace
• mul_comm
• order_basics
• numeric_evaluation

• G1 — ℕ includes 0, and n is a natural number (MKO assumption a1).
• G2 — F:ℕ→ℕ satisfies F(0)=1 and F(n+1)=(n+1)F(n) for every n∈ℕ; write n!=F(n). That such an F exists is taken from the MKO statement.

• F,\ n! — the factorial function and its notation n!=F(n)
• G — any function satisfying the same two equations
• \mathbb{N} — the natural numbers, including 0
• \prod_{k=1}^{n} k — the product of the integers from 1 to n, equal to 1 when n=0
• P(n) — the product ∏_{k=1}^{n} k as a function of n

Rules and sources

• 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₀.
• 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.
• 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.
• mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
• 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.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• 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.
• 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.
• eq_refl_symm_trans · prerequisite — Properties of equality: u=u; if u=v then v=u; if u=v and v=w then u=w.
• forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds.
• 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.
• mul_one · prerequisite — Multiplicative identity: 1·u=u.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_factorial_def · cited — The function F:ℕ→ℕ is uniquely determined recursively by F(0)=1 and F(n+1)=(n+1)F(n). Its customary notation is n!. · mko-factorial
• prod_def · prerequisite — Finite products: ∏_{k=1}^{0} a_k=1 (the empty product) and ∏_{k=1}^{n+1} a_k=(∏_{k=1}^{n} a_k)·a_{n+1}.
• nat_closure · prerequisite — Sums and products of natural numbers are natural numbers; for every n∈ℕ, n+1≥1>0.
• L_pos · lemma — For every n∈ℕ, F(n)≥1.

Main derivation

n!

F(0)=1,\ \ F(n+1)=(n+1)F(n)\ \ (n\in\mathbb{N})

G:\mathbb{N}\to\mathbb{N},\ G(0)=1,\ G(n+1)=(n+1)G(n)

Q(n):\ G(n)=F(n)

G(0),\ F(0)

G(0)=1=F(0)

G(n)=F(n)

G(n+1)=F(n+1)

Q(0),\ \ Q(n)\Rightarrow Q(n+1)

G=F\ \text{for every such}\ G

P(n)=\prod_{k=1}^{n} k

P:\mathbb{N}\to\mathbb{N}

P(0)=\prod_{k=1}^{0} k

P(0)=1

P(n+1)=P(n)\cdot(n+1)

P(n+1)=(n+1)P(n)

P(0)=1,\ \ P(n+1)=(n+1)P(n)

F(n)=\prod_{k=1}^{n} k\ \text{for every}\ n\in\mathbb{N}

F(n)

F(n)\geq 1\ \text{for every}\ n\in\mathbb{N};\ \text{in particular}\ 0!=1\neq 0

F(0)=1

F(1)=1,\ F(2)=2,\ F(3)=6

F(3)=6

F(4)=24,\ F(5)=120

\prod_{k=1}^{5} k

1\cdot 2\cdot 3\cdot 4\cdot 5=120=F(5)

S05,\ S09,\ S10,\ S12

\text{goals (1) to (4) established}

Substeps and lemmas

F(0)=1

F(0)\geq 1

F(n)\geq 1

F(n+1)=(n+1)F(n)\geq 1

Reverse audits

• S14 · sufficient_goal_reduction · S05, S09, S10, S12, and_intro_elim — Goal G: (1) to (4) together. Sufficient condition H: S05, S09, S10 and S12 each hold; H⇒G by conjunction introduction. H is proved forwards from the definition and induction; G is never used as a premise.
• S13 · premise_audit · S09, S12, prod_def — This is a consistency check at n=5 only; the general statement of S09 comes from uniqueness, not from this example.
• S12 · premise_audit · S11, forall_elim, numeric_evaluation — Exact integer multiplication (N4, N5), with no floating-point approximation.
• S11 · premise_audit · S01, forall_elim, numeric_evaluation — Each value depends on the previous one and must be computed in order; the products can be recomputed independently (N1 to N3).
• S10.2 · premise_audit · nat_closure, order_basics, nat_induction — Multiplying by n+1 keeps the inequality only because n+1>0; multiplying by a factor that can be 0 (such as the wrong recursion n·F(n) at n=0) breaks the conclusion.
• S10.1 · premise_audit · S01, order_basics — Only the defined starting value is used.
• S10 · premise_audit · L_pos — The conclusion claims only F(n)≥1, not any stronger lower bound.
• S09 · premise_audit · S05, S06, S07, S08, forall_elim — Applying uniqueness needs P to have the same starting value and the same recursion, supplied by S07 and S08. It is not obtained by checking a few values of n.
• S08 · inverse_equivalence · mul_comm — Commutativity is an identity; both forms name the same number, so the step is two-way.
• S07 · inverse_equivalence · prod_def — Both sides are the same number by definition, so the equation holds both ways.
• S06 · premise_audit · prod_def, nat_closure, nat_induction — To apply S05, P must be a function ℕ→ℕ; this step confirms its codomain.
• S05 · premise_audit · S03, S04, nat_induction, function_def, forall_intro — Both the base case S03 and the step S04 are needed; checking the first few n cannot replace the induction step. This proves uniqueness only; existence comes from the MKO.
• S04 · premise_audit · S01, S02, eq_replace — Only the induction hypothesis for the same n and the two recursions are used; n is arbitrary with no extra condition. The converse, Q(n+1)⇒Q(n), is not claimed.
• S03 · premise_audit · S01, S02, eq_refl_symm_trans — It needs the two starting values to agree; if G(0)=0 the base case fails (see error control 1).
• S02 · premise_audit · S01, def_intro — No other assumption is placed on G; that is what allows S05 to conclude for every such G (generalization).
• S01 · premise_audit · G1, G2, mko_factorial_def — This step only states the definition and derives no new fact. Existence of F is a premise supplied by the MKO; uniqueness is proved in S02 to S05.

Error controls and negative controls

0! is 1, not 0

The MKO notes the common mistake of taking 0! to be 0. F(0)=1 is part of the definition. If the start were changed to H(0)=0 while keeping H(n+1)=(n+1)H(n), induction would give H(n)=0 for every n (H(n+1)=(n+1)·0=0): the whole function collapses to 0 and 5! would be 0 instead of 120. The convention that the empty product is 1 (S07) agrees with F(0)=1.

n! is not 'n times'

The MKO also notes the mistake of reading n! as 'n times'. Each step of the recursion multiplies by the new factor n+1, so n! accumulates every factor from 1 to n: 3!=6, not 3, and 5!=120, not 5 and not 5·5=25. A related off-by-one error writes H(n+1)=n·H(n); then H(1)=0·H(0)=0 and every later value is 0.

Use exact integers, not floating-point approximations

The MKO warns against passing off floating-point values outside the safe range as exact results. 23!=25852016738884976640000=2¹⁹·49308808782358125, whose odd part exceeds 2⁵³=9007199254740992. IEEE 754 binary64 has a 53-bit significand, and a positive integer within the exponent range is exactly representable if and only if its odd part is below 2⁵³, so binary64 cannot represent 23! exactly. Every computation in this guide uses exact integer multiplication.

• 0!=0 → reject — The definition gives F(0)=1, and S10 proves F(n)≥1 for every n.
• Writing the recursion as H(n+1)=n·H(n) with H(0)=1 defines the same factorial → reject — H(1)=0·1=0, whereas F(1)=1.
• Checking F(n)=∏_{k=1}^{n} k for n=0 to 5 proves it for every n → reject — A finite check covers only those n; the general statement comes from the uniqueness of S05 (induction).
• The value of 23! computed in binary64 floating point is exact → reject — The odd part of 23! exceeds 2⁵³, so binary64 cannot represent it exactly.

Result and limitations

Exactly one function is determined by F(0)=1 and F(n+1)=(n+1)F(n) (given its existence); it equals the product ∏_{k=1}^{n} k (the empty product 1 when n=0), every value is at least 1, so 0!=1 and not 0; step-by-step substitution gives 1!=1, 2!=2, 3!=6, 4!=24 and 5!=120.

• Existence of F (the recursion theorem) is taken from the MKO statement and is not proved here; this guide proves uniqueness and the properties that follow from it.
• N8 and N9 are finite checks with the standard factorial function for n=0 to 30; they support only those n, and the argument does not depend on them.
• The statement about binary64 in error control 3 rests on the fact that the IEEE 754 binary64 format has a 53-bit significand; the text of the standard was not checked here.

Verification and source binding

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

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

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