Why does the fixed point theorem justify the existence of the factorial function?

Why is the fixed point theorem actually important here?

Well, let's think about why we believe that there is a function $f$ satisfying [recursive description of $!$]. It comes down to the following two (quite correct) beliefs:

• We can use the recursive description of $!$ to "deduce" what the value of $!$ should be on each specific natural number.

• We cannot use the recursive description of $!$ to deduce two contradictory things about $!$ (e.g. we can't use it to prove that $2!$ should be $7$).

With both claims in hand, we can then define $!$ by saying "$n!$ is the unique $m$ such that "$n!=m$" is implied by the recursive description." (In fact, only the second claim is needed to justify the existence of $!$ as a partial function.) But these claims need to be justified, and while in the case of the factorial function they are pretty obvious, $(i)$ the second claim is actually not as trivial to prove as one might hope and $(ii)$ certainly in general we want a theorem that lets us handle problems like these.

The fixed point theorem is basically a machine for getting around this issue: given a recursive description of a function, the fixed point theorem can (often) construct functions which actually satisfy that description in a precise, controlled way.

How we use it here (part $1$)

We can pass from the recursive description of the factorial function to a (perfectly good) definition of an operator on (partial) functions. The fixed point theorem shows that there is a fixed point, $f$, for this operator (once we've shown that this operator is in fact continuous); we then argue by induction that in fact this $f$ actually is the factorial function.

In detail:

From our self-referential "definition" of the factorial function, we can extract a perfectly good non-self-referential definition of an operator on partial functions $\mathcal{F}$: given a partial function $g:\mathbb{N}\rightarrow\mathbb{N}$, $\mathcal{F}(g)$ is the partial function given by

$$ \mathcal{F}(g):n\mapsto \left\{ \begin{array}{ll} 1 & \mbox{if } n = 0 \\ n * g(n-1) & \mbox{if } n > 0\mbox{ and } g(n-1)\downarrow\\ \uparrow & \mbox{if $n>0$ and $g(n-1)\uparrow$} \end{array} \right. $$

where "$\uparrow$" means "is undefined" and "$\downarrow$" means "is defined." (Note that I've written "$\mathcal{F}(g):n\mapsto...$" instead of "$\mathcal{F}(g)(n)=...$" for clarity, but there's no actual difference.) Intuitively, think of $\mathcal{F}$ as taking in a "partial computation" of $!$ - say, the first seventeen bits of the factorial function - and "going a bit further." The function we want is the "limit" of this process. This is exactly what the fixed point theorem says exists.

A quick example

Suppose $g$ is the partial function which sends $3$ to $7$, sends $10$ to $2$, sends $11$ to $11$, and is otherwise undefined. Then what partial function should $\mathcal{F}(g)$ be?

In no particular order:

• $\mathcal{F}(g)$ is certainly defined at $0$: by definition of $\mathcal{F}$, we'll always have $\mathcal{F}(g):0\mapsto 1$ regardless of what $g$ is.

• On the other hand, since $g(0)$ isn't defined, we know that $\mathcal{F}(g)(1)$ isn't defined.

• What about $11$? Well, $11>0$ and $g(11-1)$ is defined, so the second clause of the definition of $\mathcal{F}$ tells us that $$\mathcal{F}(g)(11)=11\cdot g(11-1)=11\cdot g(10)=11\cdot 2=22.$$ So $\mathcal{F}(g)(11)\downarrow =2$.

Exercise: Convince yourself that in fact the domain of $\mathcal{F}(g)$ is precisely $\{0,4,11,12\}$ and calculate the values of $\mathcal{F}(g)(4)$ and $\mathcal{F}(g)(12)$.

How we use it here (part $2$)

Having defined our operator $\mathcal{F}$, we now need to use it somehow.

Claim $1$: $\mathcal{F}$ is continuous.

The text you've quoted doesn't actually prove this, but it's not hard to check. If this is an issue, though, let me know and I'll add details.

With the continuity of $\mathcal{F}$ in hand, we can now invoke the fixed point theorem to get a function $f$ such that $$\mathcal{F}(f)=f.$$ In fact, the fixed point theorem gives us a least fixed point of $\mathcal{F}$, but we don't even need that in the current situation. We now show:

Claim $2$: This $f$ is in fact the factorial function. That is, we have $(i)$ $f$ is defined on all of $\mathbb{N}$, $(ii)$ $f(0)=1$, and $(iii)$ $f(n+1)=(n+1)f(n)$.

Parts $(i)$ and $(iii)$ are proved by induction: get a contradiction from looking at the putative first $n$ on which $f$ is undefined, and the putative first $n$ on which $f(n+1)\not=(n+1)f(n)$, respectively. Part $(ii)$ doesn't require any induction, and is just a quick observation.

Specifically, here's how we prove $(i)$ and $(ii)$ (I'll leave $(iii)$ as an exercise). The key point is that the equality $$\mathcal{F}(f)=f$$ (this is what it means for $f$ to be a fixed point of $\mathcal{F}$) lets us prove things about $f$ by proving them about $\mathcal{F}(f)$.

• To prove $(ii)$, we know by definition of $\mathcal{F}$ that $\mathcal{F}(g)(0)\downarrow=1$ for any partial function $g$. In particular, we have $$\mathcal{F}(f)(0)\downarrow=1.$$ But since $f$ is a fixed point for $\mathcal{F}$ we can turn this into $$f(0)\downarrow=1.$$

• To prove $(i)$, we've just shown that $f(0)$ is defined. Now suppose $f(n)$ is defined. By definition of $\mathcal{F}$, we know $\mathcal{F}(f)(n+1)$ is defined (namely, it's $(n+1)f(n)$). But again since $f$ is a fixed point of $\mathcal{F}$, this tells us that $f(n+1)$ is defined. So by induction, $f$ is total.

As the function $f$ is defined in terms of itself, you have a priori no guarantee that it is defined at all or uniquely defined.

Now the function $\mathcal F$ is such that it extends the known values of $f(n)$ (from a given subset of naturals) by applying the definition.

Then the fixed-point theorem guarantees that $\mathcal F$ has a fixed-point, which corresponds to $f$ defined over the whole of $\mathbb N$. Uniqueness of the fixed-point guarantees that $f$ is uniquely defined.