The factorial $n!$ and the falling factorial $n^{\underset{‾}{k}}$, defined by recursion in $\mathbb{N}$

The factorial. By the recursion theorem (The recursion theorem) applied to the set $\mathbb{N}\times \mathbb{N}$, the starting element $(0,1)$ and the function $f(k,v)=(\sigma (k),v\cdot \sigma (k))$, and by the same induction on the first coordinate as in Finite sums and finite products of natural numbers, ${\sum }_{k<n}{a}_k$ and ${\prod }_{k<n}{a}_k$ in $\mathbb{N}$, there is a unique $F:\mathbb{N}\to \mathbb{N}$ with

$F(0)=1,F(\sigma (n))=F(n)\cdot \sigma (n)(n\in \mathbb{N})\mathrm{.}$

We write $n!:=F(n)$. Thus $0!=1$, $1!=0!\cdot 1=1$, $2!=1!\cdot 2=2$, $3!=6$, $4!=24$, $5!=120$, $6!=720$.

$0!=1$ is the base clause of this recursion, not a convention imported from elsewhere. Nothing about empty products is presupposed; the agreement with the empty product is proved below, in clause (a), rather than assumed.

Truncated difference. Throughout, $n-k$ is the operation fixed in Finite sums and finite products of natural numbers, ${\sum }_{k<n}{a}_k$ and ${\prod }_{k<n}{a}_k$ in $\mathbb{N}$: the unique $j$ with $k+j=n$ when $k\le n$, and $0$ when $n<k$.

The falling factorial. For $n\in \mathbb{N}$ define $n^{\underset{‾}{k}}$ by recursion on $k$, by the recursion theorem applied to $\mathbb{N}\times \mathbb{N}$ with starting element $(0,1)$ and $f(k,v)=(\sigma (k),v\cdot (n-k))$:

$n^{\underset{‾}{0}}=1,n^{\underset{‾}{\sigma (k)}}=n^{\underset{‾}{k}}\cdot (n-k)\mathrm{.}$

So $n^{\underset{‾}{1}}=1\cdot (n-0)=n$ and $n^{\underset{‾}{2}}=n(n-1)$, and for $k\le n$ the value is the product $n(n-1)\cdots (n-k+1)$ of the $k$ topmost factors.

Four facts, proved here because the page uses each of them.

(a) The factorial is the product of the first $n$ positive naturals. $n!={\prod }_{j<n}\sigma (j)={\prod }_{j<n}(j+1)$, the $\mathbb{N}$-valued product of Finite sums and finite products of natural numbers, ${\sum }_{k<n}{a}_k$ and ${\prod }_{k<n}{a}_k$ in $\mathbb{N}$. Induction (The principle of mathematical induction): at $n=0$ both sides are $1$, the empty product and the base clause agreeing; and ${\prod }_{j<\sigma (n)}\sigma (j)=({\prod }_{j<n}\sigma (j))\cdot \sigma (n)=n!\cdot \sigma (n)=\sigma (n)!$. So the empty-product reading and the base-clause reading are the same reading, and neither was assumed.

(b) $n!\mathrm{\ne }0$, and $\iota (n!)={\prod }_{j<n}^{\mathbb{R}}\iota (j+1)$. For the first, $0!=1\mathrm{\ne }0$ (The von Neumann naturals form a Peano system) and $\sigma (n)!=n!\cdot \sigma (n)$ is a product of two nonzero naturals, which is nonzero: if $xy=0$ with $y\mathrm{\ne }0$ then $xy=0\cdot y$ (Zero and one under multiplication) and cancellation gives $x=0$ (Cancellation for multiplication by a nonzero factor). So $n!\mathrm{\ne }0$ for every $n$ by induction. For the second, apply the bridge clause 6 of that lemma to clause (a) above. This is what makes the factorial of this page and the real-valued product ${\prod }_{j<n}(j+1)$ used elsewhere in the library one object seen twice, rather than two unrelated notions.

(c) $n^{\underset{‾}{k}}\cdot (n-k)!=n!$ for $k\le n$. Induction on $k$, for all $n$ at once. At $k=0$ this reads $1\cdot n!=n!$. Assume it at $k$ and let $\sigma (k)\le n$; then $k\le n$, and writing $d:=n-k$ we have $k+d=n$ and $d\mathrm{\ne }0$, since $k+0=k\mathrm{\ne }n$; so $d=\sigma (e)$ for a unique $e$ (Every nonzero natural number is a successor), and $\sigma (k)+e=n$, that is $e=n-\sigma (k)$ (Addition is cancellative). Therefore $n^{\underset{‾}{\sigma (k)}}\cdot (n-\sigma (k))!=n^{\underset{‾}{k}}\cdot (n-k)\cdot e!=n^{\underset{‾}{k}}\cdot (e!\cdot \sigma (e))=n^{\underset{‾}{k}}\cdot \sigma (e)!=n^{\underset{‾}{k}}\cdot (n-k)!=n!$, using commutativity and associativity of multiplication (Multiplication is associative, Multiplication is commutative) and the recursion clause for the factorial.

(d) Boundary values. $n^{\underset{‾}{0}}=1$ for every $n$, by the base clause; $n^{\underset{‾}{n}}=n!$, since clause (c) at $k=n$ gives $n^{\underset{‾}{n}}\cdot 0!=n!$ and $0!=1$; and $n^{\underset{‾}{k}}=0$ whenever $k>n$. For the last, $n-n=0$ gives $n^{\underset{‾}{\sigma (n)}}=n^{\underset{‾}{n}}\cdot 0=0$, the clause $x\cdot 0=0$ being definitional (Multiplication of natural numbers), and if $n^{\underset{‾}{k}}=0$ then $n^{\underset{‾}{\sigma (k)}}=0$ as well, so $n^{\underset{‾}{k}}=0$ for every $k\ge \sigma (n)$ by induction.

• Why $0!=1$ is not imported. The empty-product convention of an arbitrary monoid is fixed in The product $g_0{g}_1\cdots g_{n-1}$ of a finite list in a monoid, by recursion, with the empty product ($n=0$) equal to the identity ↗, which comes later in the reading order, so citing it here would be a dependency pointing the wrong way. Taking $0!=1$ as the base clause of the factorial's own recursion costs nothing and owes nothing, and clause (a) then records the agreement.

• The library's other factorial. For every real $x$, $x^k\mathrm{/}k!\to 0$ ↗, later in the reading order, works with a real-valued factorial defined as the product ${\prod }_{j<n}(j+1)$ in $\mathbb{R}$. Clause (b) says that this is exactly $\iota (n!)$, so the two agree and no second notion has been created. That pointer is orientation only.

• Check every clause at $k=0$ and at $k=n$. The falling factorial is defined by two regimes, one for $k\le n$ and one beyond, and the recursion above covers both because the truncated difference is $0$ past the end. The two values that get used constantly are $n^{\underset{‾}{0}}=1$ and $n^{\underset{‾}{n}}=n!$, and both are clause (d).