The fixed point lemma is profound because it reveals a
surprisingly deep capacity in mathematics for
self-reference: when a statement $A$ is equivalent to
$F(A)$, it effectively asserts "$F$ holds of me". How
shocking it is to find that self-reference, the stuff of paradox
and nonsense, is fundamentally embedded in our beautiful
number theory! The fixed point lemma shows that every
elementary property $F$ admits a statement of arithmetic
asserting "this statement has property $F$".
Such self-reference, of course, is precisely how Goedel
proved the Incompleteness Theorem, by forming the famous
"this statement is not provable" assertion, obtaining it
simply as a fixed point $A$ asserting "$A$ is not
provable". Once you have this statement, it is easy to see
that it must be true but unprovable: it cannot be provable,
since otherwise we will have proved something false, and
therefore it is both true and unprovable.
But I have shared your apprehension at the proof of the
fixed point lemma, which although short and simple, can
nevertheless appear mysteriously impenetrable, like an
ancient mystical rune that we have memorized. We can verify
it step-by-step, but where did it come from?
So let me try to explain how one could derive this
argument, or at least arrive at it by small steps.
We want to find a statement $A$ that is equivalent to
$F(A)$. Thus, $A$ has the property that it absorbs
applications of $F$, since $A$ is equivalent to $F(A)$.
In particular, $A$ is also equivalent to $F(F(A))$, and we
could continue, arriving at one solution attempt, taking $A$ as the
infinitary expression $F(F(F(\cdots)))$. This works in a
naive formal way, since adding one more $F$ doesn't change
the form of the statement, which makes $A$ formally the
same as $F(A)$, exactly as desired. But of course it
doesn't count as a solution, since it isn't a well formed
finite expression.
What we need to do instead is to capture in a single
statement the idea that adding one more $F$ doesn't change
$A$. The statement $A$ is equivalent to the assertion that
$F$ holds when substituted at $A$ itself. Introducing an
auxiliary variable $v$ to represent the possibilities, we
consider the assertion $H(v)$ that asserts that $v$ is as
desired, namely, that $F$ holds of the statement $v$ codes,
when substituted at $v$.
(This last part, about substituting v at v, is what allows
one substitution to self-expand into two, and then three
and so on, capturing with just one substitution
the infinitary fixed point effect mentioned above.)
Namely, if $n$ is the code of $H(v)$, then we perform the
one substitution, obtaining the statement $H(n)$, which
asserts exactly that $F$ holds of the statement $n$ codes
when substituted at $n$. But since $n$ codes $H(v)$, this
means that $H(n)$ asserts that $F(H(n))$, and we have the
desired fixed point. We could have kept expanding to $F(F(H(n)))$, but we've already caught our tail.
So that's it. But let me mention some other things. First, it is interesting to consider whether all fixed points of
$F$ are equivalent to each other. This is true after all
when $F$ is tautological, for example, since any fixed
point will also be logically valid. Similarly, Goedel's "I
am not provable" statements are all equivalent to the
assertion that the theory is consistent, and this is how
one can prove the Second incompleteness theorem. But are
fixed points for a given $F$ always equivalent? The answer
is no. Fix any statements $A$ and $B$, and let $F(v)$ be
the statement, "if $v=[A]$, then $A$, otherwise $B$". Note
that $F([A])$ is equivalent to $A$ and $F([B])$ is
equivalent to $B$, so they are both fixed points.
Lastly, I would like to mention that essentially the same
argument for the fixed point lemma has been used to prove
other fixed point theorems in logic. For example, the
Recursion
Theorem
asserts that for any computable function $f$, acting on
programs, there is a program $e$ such that $e$ and $f(e)$
compute exactly the same function.
One can prove this in a very similar way to the fixed point
lemma. Namely, define H(v,x)={f({v}(v))}(x), where {e}(x)
means the output of program e on input x. Note that H is
running program v on itself, and then applying f, just as
the H in your argument. Now, let s be the function that on
input v, produces a program to compute H(v,x), so that
{s(v)}(x)=H(v,x). Let d be the program computing s, and let
e=s(d). Putting this together, we have
- {e}(x) = {s(d)}(x)= H(d,x) = {f({d}(d))}(x)
= {f(s(d))}(x) = {f(e)}(x).
So program e and f(e) compute the same function.
